[Haskell-cafe] Transforming a ADT to a GADT

[Sean Leather]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120914/fcc342cb/attachment.htm>