On Fri, Sep 14, 2012 at 12:45 PM, Florian Lorenzen wrote:<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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></blockquote><div><br></div><div>It's not pretty, but it should still be safe...</div><div><br></div><div><div><font face="courier new, monospace">import Control.Applicative</font></div><div><font face="courier new, monospace">import Unsafe.Coerce</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">tcInt :: Exp -> Maybe (Term Int)</font></div><div><font face="courier new, monospace">tcInt (Lit i) = pure (TLit i)</font></div>
<div><font face="courier new, monospace">tcInt (Succ e) = TSucc <$> tcInt e</font></div><div><font face="courier new, monospace">tcInt (If c e1 e2) = TIf <$> tcBool c <*> tcInt e1 <*> tcInt e2</font></div>
<div><font face="courier new, monospace">tcInt _ = empty</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">tcBool :: Exp -> Maybe (Term Bool)</font></div>
<div><font face="courier new, monospace">tcBool (IsZero e) = TIsZero <$> tcInt e</font></div><div><font face="courier new, monospace">tcBool (If c e1 e2) = TIf <$> tcBool c <*> tcBool e1 <*> tcBool e2</font></div>
<div><font face="courier new, monospace">tcBool _ = empty</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">typecheck :: Exp -> Maybe (Term t)</font></div>
<div><font face="courier new, monospace">typecheck e = forget <$> tcInt e <|> forget <$> tcBool e</font></div><div><font face="courier new, monospace"> where</font></div><div><font face="courier new, monospace"> forget :: Term a -> Term b</font></div>
<div><font face="courier new, monospace"> forget = unsafeCoerce</font></div></div><div><br></div><div>Regards,</div><div>Sean</div></div>