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>" _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe