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