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 < florian.loren...@tu-berlin.de> wrote: > -----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.loren...@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----- > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe