[Haskell-cafe] Transforming a ADT to a GADT

[Erik Hesselink]

On Fri, Sep 14, 2012 at 2:01 PM, Sean Leather <leather at 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