[Haskell-cafe] Transforming a ADT to a GADT

[Florian Lorenzen]

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