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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe