On Fri, Sep 14, 2012 at 2:01 PM, Sean Leather <leat...@cs.uu.nl> 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
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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
