Dear Florian,
On Fri, Sep 14, 2012 at 6:45 AM, Florian Lorenzen
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