Greg Buchholz has posed an interesting problem of writing a typechecker. Given untyped terms of the form
data Expr = ELit Int | EInc Expr | EIsZ Expr ....
we are to compute typed terms:
data Term a where Lit :: Int -> Term Int Inc :: Term Int -> Term Int IsZ :: Term Int -> Term Bool
That is, we need to write a function
typecheck :: Expr -> Term a
Actually, Greg Buchholz posed a simpler example, of a function my_read
my_read :: Expr -> Term a
Although it has the same signature, the intent is different. When the user writes "my_read exp", the user is supposed to *specify* the type of the desired result. Just as when we write "read 1", we are supposed to specify the type of the expected value: Int, Integer, etc. The function typecheck has a different intent: it *computes* the result type. It is indeed the typechecker: given the expression, we compute its type -- or report a failure if the expression is ill-typed. That is, the result *type* "Term a" is a function of the *value* Expr. Thus is truly a problem of dependent types. And Haskell is up to it: Haskell is genuinely a dependently typed language. We show the solution that uses no GADTs and no representation types. We retain however the eval function in the previous message that uses GADT. Our solution uses type classes. It seems to some the type-checking rules stated as instances of the TypeCheck class take a particular natural form. Indeed:
-- given term e, compute its type t class TypeCheck e t | e -> t where typecheck :: e -> Term t
instance TypeCheck FLit Int where typecheck (FLit x) = Lit x
instance TypeCheck e Int => TypeCheck (FInc e) Int where typecheck (FInc e) = Inc (typecheck e)
instance TypeCheck e Int => TypeCheck (FIsZ e) Bool where typecheck (FIsZ e) = IsZ (typecheck e)
instance (TypeCheck e1 Bool, TypeCheck e2 t, TypeCheck e3 t) => TypeCheck (FIf e1 e2 e3) t where typecheck (FIf e1 e2 e3) = If (typecheck e1) (typecheck e2)(typecheck e3)
instance (TypeCheck e1 t1, TypeCheck e2 t2) => TypeCheck (FPair e1 e2) (t1,t2) where typecheck (FPair e1 e2) = Pair (typecheck e1) (typecheck e2)
instance TypeCheck e (t1,t2) => TypeCheck (FFst e) t1 where typecheck (FFst e) = Fst (typecheck e)
instance TypeCheck e (t1,t2) => TypeCheck (FSnd e) t2 where typecheck (FSnd e) = Snd (typecheck e)
In the paper, the IsZ rule would have been written as |- e : int --------------- |- IsZ e : bool (We don't need the environment Gamma as our language has no variables). I submit the typeclass notation takes less space. The typechecking rules above operate on `lifted' terms: FLit, FInc, etc:
newtype FLit = FLit Int newtype FInc e = FInc e newtype FIsZ e = FIsZ e
rather than the original terms Exp. The conversion is straightforward, via Template Haskell:
type F = Q TH.Exp parse :: Expr -> F parse (ELit x) = [e| FLit $(litE . integerL . fromIntegral $ x) |] parse (EInc x) = [e| FInc $(parse x) |] parse (EIsZ x) = [e| FIsZ $(parse x) |]
The only inconvenience of using the Template Haskell is the necessity of splitting the whole code into two modules. we can then write:
e1 = "EIf (ELit 1) (ELit 2) (ELit 3)" e2 = "(EIf (EIsZ (ELit 0)) " ++ " (EInc (ELit 1)) " ++ " (EFst (EPair (ELit 42) " ++ " (ELit 43))))"
t1' = $(parse . read $ e1) t2' = $(parse . read $ e2)
*G> :t t1' t1' :: FIf FLit FLit FLit *G> :t t2' t2' :: FIf (FIsZ FLit) (FInc FLit) (FFst (FPair FLit FLit))
-- Causes the typechecking error: cannot match Int against the Bool -- tt1 = typecheck t1' tt2 = typecheck t2'
*G> :t tt2 tt2 :: Term Int Obviously, e1 is ill-formed and so cannot be typechecked. The term e2 is well-typed, and the typechecker has figured out its type, which is Term Int. There was no need for any type annotation. The term tt2 can then be evaluated. The code: file GP.hs {-# OPTIONS -fglasgow-exts #-} module GP where import Language.Haskell.TH hiding (Exp) import qualified Language.Haskell.TH as TH (Exp) import Language.Haskell.TH.Ppr -- untyped terms, at Level 0 data Expr = ELit Int | EInc Expr | EIsZ Expr | EPair Expr Expr | EIf Expr Expr Expr | EFst Expr | ESnd Expr deriving (Read,Show) -- Untyped terms, at Level 1 type F = Q TH.Exp newtype FLit = FLit Int newtype FInc e = FInc e newtype FIsZ e = FIsZ e data FPair e1 e2 = FPair e1 e2 data FIf e1 e2 e3 = FIf e1 e2 e3 newtype FFst e = FFst e newtype FSnd e = FSnd e parse :: Expr -> F parse (ELit x) = [e| FLit $(litE . integerL . fromIntegral $ x) |] parse (EInc x) = [e| FInc $(parse x) |] parse (EIsZ x) = [e| FIsZ $(parse x) |] parse (EFst x) = [e| FFst $(parse x) |] parse (ESnd x) = [e| FSnd $(parse x) |] parse (EPair x y) = [e| FPair $(parse x) $(parse y) |] parse (EIf x y z) = [e| FIf $(parse x) $(parse y) $(parse z) |] show_code cde = runQ cde >>= putStrLn . pprint t0 = show_code . parse . read $ "EInc (EInc (ELit 1))" -- ill-typed expression e1 = "EIf (ELit 1) (ELit 2) (ELit 3)" e2 = "(EIf (EIsZ (ELit 0)) " ++ " (EInc (ELit 1)) " ++ " (EFst (EPair (ELit 42) " ++ " (ELit 43))))" t1 = show_code . parse . read $ e1 File g2.hs {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} module G where import GP -- Typed terms data Term a where Lit :: Int -> Term Int Inc :: Term Int -> Term Int IsZ :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a Pair :: Term a -> Term b -> Term (a,b) Fst :: Term (a,b) -> Term a Snd :: Term (a,b) -> Term b -- Typed evaluator [elided] -- Figure out the type of the expression e -- The type-checking rules are written in the natural notation [see the TypeCheck class and instances above. Elided to save space] t0' = $(parse . read $ "EInc (EInc (ELit 1))") t1' = $(parse . read $ e1) t2' = $(parse . read $ e2) tt0 = typecheck t0' -- Causes the typechecking error: cannot match Int against the Bool -- tt1 = typecheck t1' tt2 = typecheck t2' ttt0 = eval tt0 ttt2 = eval tt2