[Haskell-cafe] Transforming a ADT to a GADT
Florian Lorenzen
florian.lorenzen at tu-berlin.de
Fri Sep 14 12:45:19 CEST 2012
-----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 at 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-----
More information about the Haskell-Cafe
mailing list