[Haskell-cafe] Transforming a ADT to a GADT

[Tsuyoshi Ito]

Dear Florian,

On Fri, Sep 14, 2012 at 6:45 AM, Florian Lorenzen
<florian.lorenzen at tu-berlin.de> wrote:
> 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.

If you can add “deriving Typeable” to Term and you are fine with a
less general type

    typecheck :: Typeable t => Exp -> Maybe (Term t)

then you can use Data.Typeable.cast.

-----

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}

module ADTToGADT where

import Control.Applicative
import Data.Typeable

data Exp
  = Lit Int
  | Succ Exp
  | IsZero Exp
  | If Exp Exp Exp

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
  deriving Typeable

typecheck :: Typeable t => Exp -> Maybe (Term t)
typecheck (Lit i) = cast $ TLit i
typecheck (Succ e) = castTerm $ TSucc <$> typecheck e
typecheck (IsZero e)   = castTerm $ TIsZero <$> typecheck e
typecheck (If c e1 e2)  = TIf <$> typecheck c <*> typecheck e1 <*> typecheck e2

castTerm :: (Typeable a, Typeable b) => Maybe (Term a) -> Maybe (Term b)
castTerm Nothing = Nothing
castTerm (Just t) = cast t

-----

Best regards,
  Tsuyoshi