Re: [Haskell-cafe] Transforming a ADT to a GADT

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 José, it occurs to me that with this solution, I always have to prescribe the type as in

tc (Succ (Lit 5)) :: Maybe (Term Int)

Otherwise, I obtain the message Ambiguous type variable `a0' in the constraint: (Tc a0) arising from a use of `tc' But as Oleg already pointed out, I want to have a value `Just term :: Maybe (Term t)' if the input is well-typed for some type which I don't know. Best regards, Florian On 09/16/2012 01:45 PM, José Pedro Magalhães wrote:

Hi Florian,

Will this do?

class Tc a where tc :: Exp -> Maybe (Term a)

instance Tc Int where tc (Lit i) = return (TLit i) tc (Succ i) = tc i >>= return . TSucc tc (IsZero i) = Nothing tc e = tcIf e

instance Tc Bool where tc (Lit i) = Nothing tc (Succ i) = Nothing tc (IsZero i) = tc i >>= return . TIsZero tc e = tcIf e

tcIf :: (Tc a) => Exp -> Maybe (Term a) tcIf (If c e1 e2) = do c' <- tc c e1' <- tc e1 e2' <- tc e2 return (TIf c' e1' e2')

Cheers, Pedro

On Fri, Sep 14, 2012 at 11:45 AM, Florian Lorenzen mailto:florian.lorenzen@tu-berlin.de> wrote:

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

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

- -- 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/ iEYEARECAAYFAlBW24UACgkQvjzICpVvX7bWZACfVWRiNrJVl/ue5sk/AFsAK36m zeUAniWoGahDymxAqkBK6JWQ5jNzDR6f =FRcI -----END PGP SIGNATURE-----