-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Hello cafe, I have a question wrt. to GADTs and type families in GHC (7.6.1). I'd like to transform a value of an ADT to a GADT. Suppose I have the simple expression language
data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp
and the GADT
data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int -> Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term ty -> Term ty -> Term ty
that encodes the typing rules. Now, I'd like to have a function
typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...>
that returns the GADT value corresponding to `exp' if `exp' is type correct. I found a solution at http://okmij.org/ftp/tagless-final/TypecheckedDSLTH.hs but this has as type (slightly adapted)
typecheck :: Exp -> Maybe TypedTerm
with
data TypedTerm = forall ty. (Typ ty) (Term ty) > data Typ ty = TInt Int | TBool Bool
That is, the GADT value is hidden inside the existential and cannot be unpacked. Therefore, I cannot write a type preserving transformation function like
transform :: Term t -> Term t
that gets the result of the `typecheck' function as input. The solution mentioned above uses Template Haskell to extract the `Term t' type from the existential package and argues that type errors cannot occur during splicing. Is there a possibility to avoid the existential and hence Template Haskell? Of course, the result type of typecheck depends on the type and type correctness of its input. My idea was to express this dependency by parameterizing `Exp' and using a type family `ExpType' like:
typecheck :: Exp e -> Maybe (Term (ExpType e)) > typecheck (ELit i) = Just (TLit i) > typecheck (ESucc exp1) = case typecheck exp1 of > Nothing -> Nothing > Just t -> Just (TSucc t) > <...>
with
data TEXP = L | S TEXP | IZ TEXP | I TEXP TEXP TEXP -- datakind >
data Exp (e::TEXP) where > ELit :: Int -> Exp L > ESucc :: Exp e1 -> Exp (S e1) > EIsZero :: Exp e1 -> Exp (IZ e1) > EIf :: Exp e1 -> Exp e2 -> Exp e3 -> Exp (I e1 e2 e3)
It seems to me that `ExpType' then would be a reification of the type checker for `Exp' at the type level. But I did not know how to define it. Does it make sense at all? Is it possible in GHC? All the examples on the net I looked at either start with the GADT right away or use Template Haskell at some point. So, perhaps this `typecheck' function is not possible to write in GHC Haskell. I very much appreciate any hints and explanations on this. Best regards, Florian - -- Florian Lorenzen Technische Universität Berlin Fakultät IV - Elektrotechnik und Informatik Übersetzerbau und Programmiersprachen Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin Tel.: +49 (30) 314-24618 E-Mail: florian.lorenzen@tu-berlin.de WWW: http://www.user.tu-berlin.de/florenz/ -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.11 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://www.enigmail.net/ iEYEARECAAYFAlBTCr8ACgkQvjzICpVvX7ZfTgCeOPflPtaEW/w1McjYWheaRaqq oUQAnRXSrGP3se+3oiI3nnd+B/rK8yx8 =X1hR -----END PGP SIGNATURE-----