-----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.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/ iEYEARECAAYFAlBTH10ACgkQvjzICpVvX7ZIVACdEPtbEHbVeQcdgzQTanVkpeKq 8QsAn3b774JsVyMMVc1lIN2rFlTVheQD =zgOc -----END PGP SIGNATURE----- _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
