On Fri, Sep 14, 2012 at 2:01 PM, 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
I don't think this is safe. What will happen if you evaluate typecheck (Lit 1) :: Maybe (Term Bool) In general, I think you have to work inside an existential. So you hide the type of the parsed Term inside an existential. If you want to apply functions to this Term, you unpack, call the function, and repack. I don't think there's a way around this, since the type parameter to Term _is_ existential. You know there is some type, but you don't know what it is. If you make it polymorphic, the _called_ can choose it, which is the opposite of what you want. Erik