[Haskell-cafe] Typechecker to GADT: the full implementation of a typed DSL

[oleg at pobox.com]

Pasqualino 'Titto' Assini wrote:
> I am trying to write an interpreter for a little functional language but I am
> finding very problematic to dynamically create a typed representations of the
> language terms.
>
> > The problem is to write a function that converts between Exp and Term
> > t as in:
> >
> > > test :: Term Double
> > > test = typecheck $ EApp (EPrim "inc") (EDouble 10.0)


The specification leaves out a few important details. The typechecker can't
be a total function: what happens when typechecking this code?
	EApp (EDouble 10.0) (EPrim "inc") 

The error has to be reported somehow, and it is important to know how.
There are basically two choices. One is to keep the above interface

> test :: Term Double
> test = typecheck $ EApp (EPrim "inc") (EDouble 10.0)

which means using Template Haskell and means letting TH reporting
type errors (with no hope of catching them). The second choice is
`typing dynamic typing'. Which means we can't write a typechecker with
the signature "Exp -> Term t". Rather, we have to write 
	typecheck :: Exp -> (forall t. Typ t -> Term t -> w) -> Maybe w
or, equivalently, using an existential
	data MostlyStatic = forall t. MostlyStatic (Typ t, Term t)
	typecheck :: Exp -> Maybe MostlyStatic

Although both MostlyStatic and Exp are `untyped', the latter is
`deeply' untyped, whereas the former is only untyped at the
surface. In the case of MostlyStatic, the term is built out of typed
components, and the type is erased only at the end.

These choices aren't contradictory: using TH, we can convert
MostlyStatic to the proper Haskell term. Because the term has already
been typechecked, we are guaranteed the absence of errors during such
a conversion. 

For today, perhaps the implementation of the second choice will be
sufficient. This is the complete representation of a typed DSL given
in the untyped AST form. We typecheck a term. We either report a
type error, or evaluate the typed term and then report result, if can be
shown. We also show the inferred type of the result.

Examples. Let's assume the following terms (not all of them well-typed)

te1 = EApp (EPrim "inc") (EDouble 10.0)
te2 = EApp (EDouble 10.0) (EPrim "inc")
te3 = EApp (EApp (EPrim "+") 
	     (EApp (EPrim "inc") (EDouble 10.0)))
           (EApp (EPrim "inc") (EDouble 20.0))
            
te4 = EApp (EPrim "rev") te3
te5 = EApp (EPrim "rev") (EApp (EPrim "show") te3)


*Eval> teval te1
"type Double, value 11.0"
*Eval> teval te2
"Type error: Trying to apply not-a-function: Double"
*Eval> teval te3
"type Double, value 32.0"
*Eval> teval te4
"Type error: incompatible type of the application: (String->String) and Double"
*Eval> teval te5
"type String, value 0.23"


The complete code follows

{-# OPTIONS -fglasgow-exts #-}

-- Typechecker to GADT
-- Implementing a typed DSL with the typed evaluator and the 
-- the typechecker from untyped terms to typed ones

module Eval where

-- Untyped terms (what I get from my parser):

data Exp =  EDouble Double | 
            EString String | 
            EPrim String | 
            EApp Exp Exp deriving (Show)

-- Typed terms:

data Term a where
  Num :: Double -> Term Double
  Str :: String -> Term String
  App :: Term (a->b) -> Term a -> Term b
  Fun :: (a->b) -> Term (a->b)


-- Typed evaluator

eval :: Term a -> a
eval (Num x) = x
eval (Str x) = x
eval (Fun x ) = x
eval (App e1 e2) = (eval e1) (eval e2)


-- Types and type comparison

data Typ a where
    TDouble :: Typ Double
    TString :: Typ String
    TFun    :: Typ a -> Typ b -> Typ (a->b)

data EQ a b where
    Refl :: EQ a a

-- checking that two types are the same. If so, give the witness

eqt :: Typ a -> Typ b -> Maybe (EQ a b)
eqt TDouble TDouble = Just $ Refl
eqt TString TString = Just $ Refl
eqt (TFun ta1 tb1) (TFun ta2 tb2) = eqt' (eqt ta1 ta2) (eqt tb1 tb2)
 where
   eqt' :: (Maybe (EQ ta1 ta2)) -> Maybe (EQ tb1 tb2) -> 
           Maybe (EQ (ta1 -> tb1) (ta2 -> tb2))
   eqt' (Just Refl) (Just Refl) = Just Refl
   eqt' _ _ = Nothing
eqt _ _ = Nothing

instance Show (Typ a) where
    show TDouble = "Double"
    show TString = "String"
    show (TFun ta tb) = "(" ++ show ta ++ "->" ++ show tb ++ ")"


-- Type checking
data MostlyStatic = forall t. MostlyStatic (Typ t, Term t)

-- Typing environment
type Gamma = [(String,MostlyStatic)]


-- Initial environment (the types of primitives)

env0 = [("rev", MostlyStatic (TFun TString TString,
                              Fun (reverse::String->String))),
        -- sorry, no polymorphism!
        ("show", MostlyStatic (TFun TDouble TString,
                               Fun (show::Double->String))),
        ("inc",  MostlyStatic (TFun TDouble TDouble,
                               Fun ((+ (1.0::Double))))),
        ("+",    MostlyStatic (TFun TDouble (TFun TDouble TDouble),
                               Fun ((+)::Double->Double->Double)))
       ]

typecheck :: Gamma -> Exp -> Either String MostlyStatic
  -- literals
typecheck _ (EDouble x) = Right $ MostlyStatic (TDouble, Num x)
typecheck _ (EString x) = Right $ MostlyStatic (TString, Str x)
typecheck env (EPrim x) = maybe err Right $ lookup x env
  where err = Left $ "unknown primitive " ++ x
typecheck env (EApp e1 e2) =
  case (typecheck env e1, typecheck env e2) of
    (Right e1, Right e2) -> typechecka e1 e2
    (Left err, Right _)  -> Left err
    (Right _,  Left err) -> Left err
    (Left e1,  Left e2) ->  Left (e1 ++ " and " ++ e2)


-- typecheck the application

typechecka (MostlyStatic ((TFun ta tb),e1)) (MostlyStatic (t2,e2)) =
  typechecka' (eqt ta t2) tb e1 e2
 where
  typechecka' :: Maybe (EQ ta t2) -> Typ tb -> Term (ta->tb) -> Term t2 ->
                 Either String MostlyStatic
  typechecka' (Just Refl) tb e1 e2 = Right $ MostlyStatic (tb,App e1 e2)
  typechecka' _ tb e1 e2 = 
     Left $ unwords ["incompatible type of the application:",
                     show (TFun ta tb), "and", show t2]

typechecka (MostlyStatic (t1,e1)) _ = 
    Left $ "Trying to apply not-a-function: " ++ show t1



-- tests

te1 = EApp (EPrim "inc") (EDouble 10.0)
te2 = EApp (EDouble 10.0) (EPrim "inc")
te3 = EApp (EApp (EPrim "+") 
             (EApp (EPrim "inc") (EDouble 10.0)))
           (EApp (EPrim "inc") (EDouble 20.0))
            
te4 = EApp (EPrim "rev") te3
te5 = EApp (EPrim "rev") (EApp (EPrim "show") te3)


-- typecheck-and-eval

teval :: Exp  -> String
teval exp = either (terror) (ev) (typecheck env0 exp)
 where
  terror err = "Type error: " ++ err
  ev (MostlyStatic (t,e)) = "type " ++ show t ++ ", value " ++
       (tryshow (eqt t TString) (eqt t TDouble) (eval e))
  tryshow :: Maybe (EQ t String) -> Maybe (EQ t Double) -> t -> String
  tryshow (Just Refl) _ t = t
  tryshow _ (Just Refl) t = show t
  tryshow _ _ _ = "<fun>"