[Haskell-cafe] Transforming a ADT to a GADT

Florian Lorenzen florian.lorenzen at tu-berlin.de
Fri Sep 14 12:45:19 CEST 2012

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

I found a solution at
http://okmij.org/ftp/tagless-final/TypecheckedDSLTH.hs but this has as
type (slightly adapted)

> typecheck :: Exp -> Maybe TypedTerm


> 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

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) > <...>


> 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 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/
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://www.enigmail.net/


More information about the Haskell-Cafe mailing list