Hi Florian,<br><br>Will this do?<br><br><span style="font-family:courier new,monospace">class Tc a where<br> tc :: Exp -> Maybe (Term a)<br><br>instance Tc Int where<br> tc (Lit i) = return (TLit i)<br> tc (Succ i) = tc i >>= return . TSucc<br>
tc (IsZero i) = Nothing<br> tc e = tcIf e<br><br>instance Tc Bool where<br> tc (Lit i) = Nothing<br> tc (Succ i) = Nothing<br> tc (IsZero i) = tc i >>= return . TIsZero<br> tc e = tcIf e<br>
<br>tcIf :: (Tc a) => Exp -> Maybe (Term a)<br>tcIf (If c e1 e2) = do c' <- tc c<br> e1' <- tc e1<br> e2' <- tc e2<br> return (TIf c' e1' e2')</span><br>
<br><br>Cheers,<br>Pedro<br><br><div class="gmail_quote">On Fri, Sep 14, 2012 at 11:45 AM, Florian Lorenzen <span dir="ltr"><<a href="mailto:florian.lorenzen@tu-berlin.de" target="_blank">florian.lorenzen@tu-berlin.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">-----BEGIN PGP SIGNED MESSAGE-----<br>
Hash: SHA1<br>
<br>
Hello cafe,<br>
<br>
I have a question wrt. to GADTs and type families in GHC (7.6.1).<br>
<br>
I'd like to transform a value of an ADT to a GADT. Suppose I have the<br>
simple expression language<br>
<br>
> data Exp = Lit Int > | Succ Exp > | IsZero Exp > | If Exp Exp Exp<br>
<br>
and the GADT<br>
<br>
> data Term t where > TLit :: Int -> Term Int > TSucc :: Term Int -><br>
Term Int > TIsZero :: Term Int -> Term Bool > TIf :: Term Bool -> Term<br>
ty -> Term ty -> Term ty<br>
<br>
that encodes the typing rules.<br>
<br>
Now, I'd like to have a function<br>
<br>
> typecheck :: Exp -> Maybe (Term t) > typecheck exp = <...><br>
<br>
that returns the GADT value corresponding to `exp' if `exp' is type<br>
correct.<br>
<br>
I found a solution at<br>
<a href="http://okmij.org/ftp/tagless-final/TypecheckedDSLTH.hs" target="_blank">http://okmij.org/ftp/tagless-final/TypecheckedDSLTH.hs</a> but this has as<br>
type (slightly adapted)<br>
<br>
> typecheck :: Exp -> Maybe TypedTerm<br>
<br>
with<br>
<br>
> data TypedTerm = forall ty. (Typ ty) (Term ty) > data Typ ty =<br>
> TInt<br>
Int | TBool Bool<br>
<br>
That is, the GADT value is hidden inside the existential and cannot be<br>
unpacked. Therefore, I cannot write a type preserving transformation<br>
function like<br>
<br>
> transform :: Term t -> Term t<br>
<br>
that gets the result of the `typecheck' function as input.<br>
<br>
The solution mentioned above uses Template Haskell to extract the<br>
`Term t' type from the existential package and argues that type errors<br>
cannot occur during splicing.<br>
<br>
Is there a possibility to avoid the existential and hence Template<br>
Haskell?<br>
<br>
Of course, the result type of typecheck depends on the type and type<br>
correctness of its input.<br>
<br>
My idea was to express this dependency by parameterizing `Exp' and<br>
using a type family `ExpType' like:<br>
<br>
> typecheck :: Exp e -> Maybe (Term (ExpType e)) > typecheck (ELit<br>
> i)<br>
= Just (TLit i) > typecheck (ESucc exp1) = case typecheck exp1 of ><br>
Nothing -> Nothing > Just t -> Just (TSucc t) > <...><br>
<br>
with<br>
<br>
> data TEXP = L | S TEXP | IZ TEXP | I TEXP TEXP TEXP -- datakind ><br>
> ><br>
data Exp (e::TEXP) where > ELit :: Int -> Exp L > ESucc :: Exp e1 -><br>
Exp (S e1) > EIsZero :: Exp e1 -> Exp (IZ e1) > EIf :: Exp e1 -> Exp<br>
e2 -> Exp e3 -> Exp (I e1 e2 e3)<br>
<br>
It seems to me that `ExpType' then would be a reification of the type<br>
checker for `Exp' at the type level. But I did not know how to define<br>
it. Does it make sense at all? Is it possible in GHC?<br>
<br>
All the examples on the net I looked at either start with the GADT<br>
right away or use Template Haskell at some point. So, perhaps this<br>
`typecheck' function is not possible to write in GHC Haskell.<br>
<br>
I very much appreciate any hints and explanations on this.<br>
<br>
Best regards,<br>
<br>
Florian<br>
<br>
<br>
<br>
- --<br>
Florian Lorenzen<br>
<br>
Technische Universität Berlin<br>
Fakultät IV - Elektrotechnik und Informatik<br>
Übersetzerbau und Programmiersprachen<br>
<br>
Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin<br>
<br>
Tel.: +49 (30) 314-24618<br>
E-Mail: <a href="mailto:florian.lorenzen@tu-berlin.de">florian.lorenzen@tu-berlin.de</a><br>
WWW: <a href="http://www.user.tu-berlin.de/florenz/" target="_blank">http://www.user.tu-berlin.de/florenz/</a><br>
-----BEGIN PGP SIGNATURE-----<br>
Version: GnuPG v1.4.11 (GNU/Linux)<br>
Comment: Using GnuPG with Mozilla - <a href="http://www.enigmail.net/" target="_blank">http://www.enigmail.net/</a><br>
<br>
iEYEARECAAYFAlBTCr8ACgkQvjzICpVvX7ZfTgCeOPflPtaEW/w1McjYWheaRaqq<br>
oUQAnRXSrGP3se+3oiI3nnd+B/rK8yx8<br>
=X1hR<br>
-----END PGP SIGNATURE-----<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br>