Open jmchapman opened 10 months ago
For example, say I want to have abstract syntax à la Emil Axelsson (2012). This construction needs generalized algebraic types for storing arity information on the type level. But indexed types must be erased by agda2hs
, so what looks like a generalized algebraic type in Agda will become a plain sum type in Haskell. This then would allow me to construct in Haskell values that would have been illegal in Agda and should be illegal if I were writing abstract syntax in Haskell with generalized algebraic types to begin with.
For example, the following translation of Emil's NUM
to Agda:
data NUM : (@0 a : Signature) → Set₁ where
Num : Int → NUM (Full Int)
Add : NUM (Argument Int :→ Argument Int :→ Full Int)
Mul : NUM (Argument Int :→ Argument Int :→ Full Int)
{-# COMPILE AGDA2HS NUM #-}
— Loses all the arity data when compiled to Haskell with agda2hs
:
data NUM = Num Int
| Add
| Mul
Instead, it would be fantastic if it would become something like this:
data NUM (a :: Signature) where
Num :: Int -> NUM (Full Int)
Add :: NUM (Argument Int :→ Argument Int :→ Full Int)
Mul :: NUM (Argument Int :→ Argument Int :→ Full Int)
Is this realistic?
Add support for GADTs