Hi Florian,<br><br>Will this do?<br><br><span style="font-family:courier new,monospace">class Tc a where<br>† tc :: Exp -&gt; Maybe (Term a)<br><br>instance Tc Int where<br>† tc (Lit i) † † †= return (TLit i)<br>† tc (Succ i) † † = tc i &gt;&gt;= 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 &gt;&gt;= return . TIsZero<br>† tc e † † † † † †= tcIf e<br>

<br>tcIf :: (Tc a) =&gt; Exp -&gt; Maybe (Term a)<br>tcIf (If c e1 e2) = do c&#39; &lt;- tc c<br>† † † † † † † † † † † †e1&#39; &lt;- tc e1<br>† † † † † † † † † † † †e2&#39; &lt;- tc e2<br>† † † † † † † † † † † †return (TIf c&#39; e1&#39; e2&#39;)</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">&lt;<a href="mailto:florian.lorenzen@tu-berlin.de" target="_blank">florian.lorenzen@tu-berlin.de</a>&gt;</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&#39;d like to transform a value of an ADT to a GADT. Suppose I have the<br>
simple expression language<br>
<br>
&gt; data Exp = Lit Int &gt; | Succ Exp &gt; | IsZero Exp &gt; | If Exp Exp Exp<br>
<br>
and the GADT<br>
<br>
&gt; data Term t where &gt; TLit :: Int -&gt; Term Int &gt; TSucc :: Term Int -&gt;<br>
Term Int &gt; TIsZero :: Term Int -&gt; Term Bool &gt; TIf :: Term Bool -&gt; Term<br>
ty -&gt; Term ty -&gt; Term ty<br>
<br>
that encodes the typing rules.<br>
<br>
Now, I&#39;d like to have a function<br>
<br>
&gt; typecheck :: Exp -&gt; Maybe (Term t) &gt; typecheck exp = &lt;...&gt;<br>
<br>
that returns the GADT value corresponding to `exp&#39; if `exp&#39; 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>
&gt; typecheck :: Exp -&gt; Maybe TypedTerm<br>
<br>
with<br>
<br>
&gt; data TypedTerm = forall ty. (Typ ty) (Term ty) &gt; data Typ ty =<br>
&gt; 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>
&gt; transform :: Term t -&gt; Term t<br>
<br>
that gets the result of the `typecheck&#39; function as input.<br>
<br>
The solution mentioned above uses Template Haskell to extract the<br>
`Term t&#39; 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&#39; and<br>
using a type family `ExpType&#39; like:<br>
<br>
&gt; typecheck :: Exp e -&gt; Maybe (Term (ExpType e)) &gt; typecheck (ELit<br>
&gt; i)<br>
= Just (TLit i) &gt; typecheck (ESucc exp1) = case typecheck exp1 of &gt;<br>
Nothing -&gt; Nothing &gt; Just t -&gt; Just (TSucc t) &gt; &lt;...&gt;<br>
<br>
with<br>
<br>
&gt; data TEXP = L | S TEXP | IZ TEXP | I TEXP TEXP TEXP -- datakind &gt;<br>
&gt; &gt;<br>
data Exp (e::TEXP) where &gt; ELit :: Int -&gt; Exp L &gt; ESucc :: Exp e1 -&gt;<br>
Exp (S e1) &gt; EIsZero :: Exp e1 -&gt; Exp (IZ e1) &gt; EIf :: Exp e1 -&gt; Exp<br>
e2 -&gt; Exp e3 -&gt; Exp (I e1 e2 e3)<br>
<br>
It seems to me that `ExpType&#39; then would be a reification of the type<br>
checker for `Exp&#39; 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&#39; 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>