Oleg, thank you so much for taking the time to provide the example code and the explanation, it really helps. My mental typechecker seems to diverge on the "data EQ a b where Refl :: EQ a a" bit so I am now reading the "typing dynamic typing" paper, hoping for further enlightment. If you don't mind, I would have a question regarding the usage of Template Haskell to convert the AST to a typed term. I have found this paper by Louis-Julien Guillemette and Stefan Monnier : http://www.iro.umontreal.ca/~monnier/tct.pdf The code that I could extract from the paper (there doesn't seem to be a code distribution) follows. I don't see however how this could possibly be used to implement an interpreter, certainly the AST must be known at compile time, or am I missing something? Thanks again, titto

{-# OPTIONS -fglasgow-exts -fth #-} module HOASEval where import Language.Haskell.TH

type VarId = String

data AST = Fvar VarId | Flam VarId AST | Fapp AST AST

lift :: AST -> ExpQ lift (Fvar x) = varE (mkName x) lift (Flam x b) = [| Lam $(lam1E (varP (mkName x)) (lift b)) |] lift (Fapp a b) = [| App $(lift a) $(lift b) |]

data Term t where Num :: Int -> Term Int Prim :: PrimOp -> Term Int -> Term Int -> Term Int If0 :: Term Int -> Term t -> Term t -> Term t Lam :: (Term s -> Term t) -> Term (s -> t) App :: Term (s -> t) -> Term s -> Term t

data PrimOp = Add | Sub | Mult

e0 = Flam "x" (Fvar "x")

eval ast = $(lift ast)

test = eval e0

On Thursday 04 October 2007 07:02:32 oleg@pobox.com wrote:

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>"