[Haskell-cafe] Transforming a ADT to a GADT

[Florian Lorenzen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear Sean,

thanks for your solution. It in the documentation of unsafeCoerce it
says: "It [unsafeCoerce] is generally used when you want to write a
program that you know is well-typed, but where Haskell's type system
is not expressive enough to prove that it is well typed."

May I conclude that the (GHC) Haskell type system is not powerful
enough to type such a typecheck function?

Best regards,

Florian

On 09/14/2012 02:01 PM, Sean Leather wrote:
> On Fri, Sep 14, 2012 at 12:45 PM, Florian Lorenzen wrote:
> 
> 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.
> 
> 
> It's not pretty, but it should still be safe...
> 
> import Control.Applicative import Unsafe.Coerce
> 
> tcInt :: Exp -> Maybe (Term Int) tcInt (Lit i)       = pure (TLit
> i) tcInt (Succ e)      = TSucc <$> tcInt e tcInt (If c e1 e2)  =
> TIf <$> tcBool c <*> tcInt e1 <*> tcInt e2 tcInt _             =
> empty
> 
> tcBool :: Exp -> Maybe (Term Bool) tcBool (IsZero e)   = TIsZero
> <$> tcInt e tcBool (If c e1 e2) = TIf <$> tcBool c <*> tcBool e1
> <*> tcBool e2 tcBool _            = empty
> 
> typecheck :: Exp -> Maybe (Term t) typecheck e = forget <$> tcInt e
> <|> forget <$> tcBool e where forget :: Term a -> Term b forget =
> unsafeCoerce
> 
> Regards, Sean

- -- 
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 at 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/

iEYEARECAAYFAlBTH10ACgkQvjzICpVvX7ZIVACdEPtbEHbVeQcdgzQTanVkpeKq
8QsAn3b774JsVyMMVc1lIN2rFlTVheQD
=zgOc
-----END PGP SIGNATURE-----