liboleg 0.1.0.3 → 0.1.1

raw patch · 11 files changed

+2460/−4 lines, 11 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Language/TEval/EvalN.hs +150/−0
• Language/TEval/EvalTaglessF.hs +230/−0
• Language/TEval/EvalTaglessI.hs +265/−0
• Language/TEval/TEvalNC.hs +123/−0
• Language/TEval/TEvalNR.hs +135/−0
• Language/TEval/TInfLetI.hs +322/−0
• Language/TEval/TInfLetP.hs +411/−0
• Language/TEval/TInfT.hs +219/−0
• Language/TEval/TInfTEnv.hs +289/−0
• Language/TEval/TInfTM.hs +301/−0
• liboleg.cabal +15/−4

@@ -0,0 +1,150 @@+-- |+-- Untyped (nominal) lambda-calculus with integers and the conditional+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--+--+--    [The Abstract of the lecture notes]+--    We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic+--     semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type+--     checking, deals with approximations like int. A type system is sound if it correctly approximates+--     the dynamic behavior and predicts its outcome: if the static semantics predicts that a term has+--     the type int, the dynamic evaluation of the term, if it terminates, will yield an integer.+-- +--     As object language, we use simply-typed and let-polymorphic lambda calculi with integers and+--     integer operations as constants. We use Haskell as a metalanguage in which to write evaluators,+--     type checkers, type reconstructors and inferencers for the object language.+-- +--     We explore the deep relation between parametric polymorphism and `inlining'. Polymorphic type+--     checking then is an optimization allowing us to type check a polymorphic term at the place of its+--     definition rather than at the places of its use.+-- +--     Joint work with Chung-chieh Shan.+-- +-- Version+--     The current version is 1.1, July 2008.+-- References+--     lecture.pdf [199K]+-- ++module Language.TEval.EvalN where++data Term = V VarName+          | L VarName Term+          | A Term Term+          | I Int+          | Term :+ Term                -- addition+          | IFZ Term Term Term          -- if zero+            deriving (Show, Eq)++infixl 9 `A`+type VarName = String++-- | Environment: associating values with `free' variables+type Env = [(VarName, Value)]++env0 :: Env+env0 = []++lkup :: Env -> VarName -> Value+lkup env x = maybe err id $ lookup x env + where err = error $ "Unbound variable " ++ x++ext :: Env -> (VarName,Value) -> Env+ext env xt = xt : env++data Value = VI Int | VC (Value -> Value)+instance Show Value where+    show (VI n) = "VI " ++ show n+    show (VC _) = "<function>"++-- | Denotational semantics. Why? How to make it operational?+eval :: Env -> Term -> Value+eval env (V x)   = lkup env x+eval env (L x e) = VC (\v -> eval (ext env (x,v)) e)+eval env (A e1 e2) = +    let v1 = eval env e1+        v2 = eval env e2+    in case v1 of+       VC f  -> f v2+       v     -> error $ "Trying to apply a non-function: " ++ show v++eval env (I n) = VI n                   -- already a value+eval env (e1 :+ e2) =+    let v1 = eval env e1+        v2 = eval env e2+    in case (v1,v2) of+       (VI n1, VI n2) -> VI (n1+n2)+       vs     -> error $ "Trying to add non-integers: " ++ show vs+eval env (IFZ e1 e2 e3) =+    let v1 = eval env e1+    in case v1 of+       VI 0 -> eval env e2+       VI _ -> eval env e3+       v    -> error $ "Trying to compare a non-integer to 0: " ++ show v++(vx,vy) = (V "x",V "y")++term1 = L "x" (IFZ vx (I 1) (vx :+ (I 2)))++test11 = eval env0 term1+test12 = eval env0 (term1 `A` (I 2))    -- VI 4+test13 = eval env0 (term1 `A` (I 0))    -- VI 1+test14 = eval env0 (term1 `A` vx)       -- Exception: Unbound variable x++term2 = L "x" (L "y" (vx :+ vy))++test21 = eval env0 term2+test22 = eval env0 (term2 `A` (I 1))+test23 = eval env0 (term2 `A` (I 1) `A` (I 2)) -- VI 3++-- | Hidden problems+term3 = L "x" (IFZ vx (I 1) vy)++test31 = eval env0 term3+test32 = eval env0 (term3 `A` (I 0))    -- VI 1+test33 = eval env0 (term3 `A` (I 1))    -- Exception: Unbound variable y++term4 = L "x" (IFZ vx (I 1) (vx `A` (I 1)))+test41 = eval env0 term4+test42 = eval env0 (term4 `A` (I 0))    -- VI 1+test43 = eval env0 (term4 `A` (I 1))    -- applying a non-function+++term6  = (L "x" (I 1)) `A` vy+test61 = eval env0 term6                -- regarding CBN vs CBV...+++-- (x+1)*y = x*y + y++-- | why is this cheating? Try showing the term+tmul1 = L "x" (L "y" +          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy)))++testm1 = eval env0 (tmul1 `A` (I 2) `A` (I 3))++-- | termY f === f (termY f)+-- or: termY f x === f (termY f) x++termY = L "f" (delta `A` (L "y" (L "x" (vf `A` (delta `A` vy) `A` vx))))+ where delta = L "y" (vy `A` vy)+       vf = V "f"++tmul = termY `A` (L "self" (L "x" (L "y" +          (IFZ vx (I 0)+            (((V "self") `A` (vx :+ (I (-1))) `A` vy) :+ vy)))))++testm2 = eval env0 (tmul `A` (I 2) `A` (I 3)) -- VI 6++-- | The following is the implementation of a few exercises. Don't show them++termfib = termY `A` (L "self" (L "n"+     (IFZ vn (I 1)+       (IFZ (pred vn) (I 1)+        ((self `A` (pred vn)) :+ (self `A` (pred (pred vn))))))))+ where (vn,self) = (V "n", V "self")+       pred x = x :+ (I (-1))           -- This is an _abbreviation_++testfib = map (\n -> eval env0 (termfib `A` (I n))) [0..7]+-- [VI 1,VI 1,VI 2,VI 3,VI 5,VI 8,VI 13,VI 21]

@@ -0,0 +1,230 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+  -- Haskell' Committee seems to have agreed to remove the restriction++-- | Tagless Typed lambda-calculus with integers and the conditional+-- in the higher-order abstract syntax.+-- Haskell itself ensures the object terms are well-typed.+-- Here we use the tagless final approach.+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.EvalTaglessF where++class Symantics repr where+  l    :: (repr t1 -> repr t2) -> repr (t1->t2)+  a    :: repr (t1->t2) -> repr t1 -> repr t2+  i    :: Int -> repr Int+  (+:) :: repr Int -> repr Int -> repr Int              -- addition+  ifz  :: repr Int -> repr t -> repr t -> repr t        -- if zero+  fix  :: repr ((a->b) -> (a->b)) -> repr (a->b)+  -- Let :: repr t1 -> (repr t1 -> repr t) -> repr t++-- compared to EvalTaglessI, everything is in lower-case now++-- | Since we rely on the metalanguage for typechecking and hence+-- type generalization, we have to use `let' of the metalanguage.+infixl 9 `a`+++-- | It is quite challenging to show terms. Yet, in contrast to the GADT-based+-- approach (EvalTaglessI.hs), we are able to do that, without+-- extending our language with auxiliary syntactic forms.+-- Incidentally, showing of terms is just another way of _evaluating_+-- them, to strings.+--+type VarCount = Int                     -- to build the names of variables+newtype S t = S (VarCount -> (String,VarCount))+evals (S t) = t++instance Symantics S where+    l f      = S $ \c0 ->+                   let vname = "v" ++ show c0+                       c1 = succ c0+                       (s,c2) = evals (f (S $ \c -> (vname,c))) c1+                   in ("(\\" ++ vname ++ "-> " ++ s ++ ")",c2)+    a e1 e2  = S $ \c0 ->+                   let (s1,c1) = evals e1 c0+                       (s2,c2) = evals e2 c1+                   in ("(" ++ s1 ++ " " ++ s2 ++ ")",c2)+    i n      = S $ \c -> (show n,c)+    e1 +:e2  = S $ \c0 ->+                   let (s1,c1) = evals e1 c0+                       (s2,c2) = evals e2 c1+                   in ("(" ++ s1 ++ " + " ++ s2 ++ ")",c2)+    ifz e1 e2 e3 = S $ \c0 ->+                   let (s1,c1) = evals e1 c0+                       (s2,c2) = evals e2 c1+                       (s3,c3) = evals e3 c2+                   in ("(ifz " ++ s1 ++ " " ++ s2 ++ " " ++ s3 ++")",c3)+    fix e = S $ \c0 ->+                   let (s1,c1) = evals e c0+                   in ("(fix " ++ s1 ++ ")",c1)++tshow t = fst $ evals t 0++-- | We no longer need variables or the environment and we do+-- normalization by evaluation.++-- | Denotational semantics. Why?+newtype D t = D t                       -- This is not a tag. Why?+evald:: D t -> t+evald (D t) = t++instance Symantics D where+    l f      = D $ \x -> evald (f (D x))+    a e1 e2  = D $ (evald e1) (evald e2)+    i n      = D $ n+    e1 +: e2 = D $ evald e1 + evald e2+    ifz e1 e2 e3 = D $ if evald e1 == 0 then evald e2 else evald e3+    fix e    = D $ hfix (evald e) where hfix f = f (hfix f)++{- |+We can also give operational semantics, by implementing the function of the+following signature:++evalo :: (forall repr. Symantics repr => repr t) ->+         (forall repr. Symantics repr => repr t)++The signature has rank-2 type and hence this file requires a PRAGMA+declaration {-# LANGUAGE Rank2Types #-}++The implementation of evalo is exactly the partial evaluator of the+tagless final paper. Please see the paper for details.++-}++-- Tests+-- Truly the tests differ from those in EvalTaglessI.hs only in the case+-- of `syntax`: (i 1) vs (I 1), etc.++test0d = evald $ l(\vx -> vx +: (i 2)) `a` (i 1) -- 3++term1 = l (\vx -> ifz vx (i 1) (vx +: (i 2)))+test11d = evald $ term1+test11s = tshow $ term1 -- "(\\v0-> (ifz v0 1 (v0 + 2)))"++test12d = evald (term1 `a` (i 2))       -- 4, as Haskell Int+-- test14  = evald (term1 `a` vx)       -- Type error! Not in scope: `vx'+++term2 = l (\vx -> l (\vy -> vx +: vy))+-- *EvalTaglessF> :t term2+-- term2 :: (Symantics repr) => repr (Int -> Int -> Int)++test21  = evald term2+test23d = evald (term2 `a` (i 1) `a` (i 2)) -- 3++termid = l(\vx -> vx)+testid = evald termid -- testid :: t1 -> t1++term2a = l (\vx -> l(\vy -> vx `a` vy))+{- The meta-language figured the (polymorphic) type now+ *EvalTaglessF> :t term2a+ term2a :: (Symantics repr) => repr ((t1 -> t2) -> t1 -> t2)+-}+++-- No longer hidden problems+-- term3 = l (\vx -> ifz vx (i 1) vy) -- Not in scope: `vy'++-- The following is a type error, we can't even enter the term+-- term4 = l (\vx -> ifz vx (i 1) (vx `a` (i 1)))+{- Now we get good error messages!++    Couldn't match expected type `t1 -> Int'+           against inferred type `Int'+      Expected type: repr (t1 -> Int)+      Inferred type: repr Int+    In the first argument of `a', namely `vx'+    In the third argument of `ifz', namely `(vx `a` (i 1))'+-}++++-- (x+1)*y = x*y + y++-- why is this less of a cheating? Try showing the term+-- Now, both type-checking and evaluation of tmul1 works!+tmul1 = l (\vx -> l (\vy ->+          (ifz vx (i 0)+            ((tmul1 `a` (vx +: (i (-1))) `a` vy) +: vy))))++-- tmul1 :: (Symantics repr) => repr (Int -> Int -> Int)++testm1d = evald (tmul1 `a` (i 2) `a` (i 3))  -- 6+++-- Can termY be typechecked?+-- delta = l (\vy -> vy `a` vy)+{-+    Occurs check: cannot construct the infinite type: t1 = t1 -> t2+      Expected type: repr t1+      Inferred type: repr (t1 -> t2)+    In the second argument of `a', namely `vy'+    In the expression: vy `a` vy+-}++tmul = fix (l (\self -> l (\vx -> l (\vy ->+          (ifz vx (i 0)+            ((self `a` (vx +: (i (-1))) `a` vy) +: vy))))))++testm21d = evald tmul+testm23d = evald (tmul `a` (i 2) `a` (i 3)) -- 6++-- Tests of let (cf. the corresponding tests in TInfLetP.hs)++testl1 = let vx = vx in vx               -- why this works in Haskell?+-- testl2 = let vx = vy in (i 1)            -- type error+testl3 = evald $ let vx = i 1 in vx +: vx -- 2++-- this is essentially the test of hygiene+testl5  = evald $ l(\vx -> let vy = vx `a` (i 1) in l(\vx -> vy +: vx))+-- testl5 :: (Int -> Int) -> Int -> Int++-- lambda vs. let-bound variables+testl61 = evald $ l(\vx -> let vy = vx `a` (i 1) in+                           let vz = vy +: (i 2) in vy)+-- testl61 :: (Int -> Int) -> Int+testl62 = evald $ l(\vx -> let vy = vx `a` (i 1) in+                           let vz = vy +: (i 2) in vx)+-- testl62 :: (Int -> Int) -> Int -> Int+testl63 = evald $ l(\vx -> let vy = vx `a` (i 1) in+                           let vz = (i 2) in vx)+-- testl63 :: (Int -> t2) -> Int -> t2++testl71 = evald $ let vx = term2a in vx+-- testl71 :: (t1 -> t2) -> t1 -> t2++testl72 = evald $ let vx = term2a in +                  let vy = vx `a` termid in+                  let vz = vy `a` (i 2) in vx+-- testl72 :: (t1 -> t2) -> t1 -> t2++testl73 = evald $ let vx = term2a in +                  let vy = vx `a` termid in+                  let vz = vy `a` (i 2) in vy+-- testl73 :: t2 -> t2+testl74 = evald $ let vx = term2a in +                  let vy = let z = vx `a` tmul in vx `a` termid+                  in vy+-- testl74 :: t2 -> t2+testl75 = evald $ let vx = term2a in +                  let vy = let z = vx `a` termid in z+                  in vy+-- testl75 :: t2 -> t2++term2id = let id = l(\vx ->vx) in+          l(\f -> l(\vy -> +               ((i 2) +:+                ((id `a` f) `a` ((id `a` vy) +: (i 1))))))+test2id = evald term2id+-- test2id :: (Int -> Int) -> Int -> Int++termlet = let c2 = l(\f -> l(\vx -> f `a` (f `a` vx))) in+          let inc = l(\vx -> vx +: (i 1)) in+          let compose = l(\f -> l(\g -> l(\vx -> f `a` (g `a` vx)))) in+          let id = l(\vx -> vx) in+          c2 `a` (compose `a` inc `a` inc) `a` (i 10) +:+          ((c2 `a` (compose `a` inc) `a` id) `a` (i 100))+testlet = evald termlet -- 116

@@ -0,0 +1,265 @@+{-# LANGUAGE GADTs #-}++-- | Tagless Typed lambda-calculus with integers and the conditional+-- in the higher-order abstract syntax.+-- Haskell itself ensures the object terms are well-typed.+-- Here we use GADT: This file is not in Haskell98+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.EvalTaglessI where++data Term t where+  V    :: t -> Term t                   -- used only for denot semantics+  L    :: (Term t1 -> Term t2) -> Term (t1->t2)+  A    :: Term (t1->t2) -> Term t1 -> Term t2+  I    :: Int -> Term Int+  (:+) :: Term Int -> Term Int -> Term Int              -- addition+  IFZ  :: Term Int -> Term t -> Term t -> Term t        -- if zero+  Fix  :: Term ((a->b) -> (a->b)) -> Term (a->b)+  -- Let :: Term t1 -> (Term t1 -> Term t) -> Term t++-- | Since we rely on the metalanguage for typechecking and hence+-- type generalization, we have to use the metalanguage `let'+-- The (V n) term, aka the polymorphic lift, is not used in user terms.+-- This is the `internal' component for the sake of evald only (evalo doesn't+-- need it).+infixl 9 `A`+++-- | It is quite challenging to show terms. In fact, we can't do it+-- for lambda-terms at all! The argument of the L constructor is a function.+-- We can't show functions; if we find a term to apply the function to,+-- we obtain a term, which we can show then. The only candidate for the+-- term to pass to the body of L is the V term; but to construct+-- (V x) we need x -- the value of some type (and we don't have an idea+-- of the type). So, the best we can do is (V undefined) -- which, alas,+-- we can't show. The only solution is to modify the definition of Term t, +-- and make the V constructor thusly: V :: t -> String -> Term t.+-- In that case, we can show V-term values.++instance Show (Term t) where+    show (I n) = "I " ++ show n+    show (L f) = "<function>"+    -- The other terms are not values, so we won't show them at all.+    -- The above two clauses are enough to show the result of the evalo+    -- evaluator.+++-- | We no longer need variables or the environment and we do+-- normalization by evaluation.++-- | Denotational semantics. Why?+evald :: Term t -> t+evald (V x) = x+evald (L f) = \x -> evald (f (V x))+evald (A e1 e2) = (evald e1) (evald e2)+evald (I n) = n+evald (e1 :+ e2) = evald e1 + evald e2+evald (IFZ e1 e2 e3) = if evald e1 == 0 then evald e2 else evald e3+evald (Fix e) = fix (evald e) where fix f = f (fix f)+++-- | Operational semantics. Why?+-- GADT are still implemented imperfectly: we the default case in case +-- statements (with cannot happen error), to avoid the warning about+-- inexhaustive pattern match -- although these case-brances can never+-- be executed. Why?++evalo :: Term t -> Term t+evalo e@(L _) = e                       -- already a value+evalo (A e1 e2) = +    let v1 = evalo e1+        v2 = evalo e2+    in case v1 of+       L f -> evalo (f v2)              -- could just use e2?+       _     -> error "Cannot happen"+evalo e@(I _) = e                       -- already a value+evalo (e1 :+ e2) =+    let v1 = evalo e1+        v2 = evalo e2+    in case (v1,v2) of+       (I n1, I n2) -> I (n1+n2)+       _     -> error "Cannot happen"+evalo (IFZ e1 e2 e3) =+    let v1 = evalo e1+    in case v1 of+       I 0 -> evalo e2+       I _ -> evalo e3+       _    -> error "Cannot happen"+evalo (Fix e) = evalo (e `A` (Fix e))+++-- Tests++test0d = evald $ L(\vx -> vx :+ (I 2)) `A` (I 1) -- 3+test0o = evalo $ L(\vx -> vx :+ (I 2)) `A` (I 1) -- I 3++term1 = L (\vx -> IFZ vx (I 1) (vx :+ (I 2)))++test11d = evald term1+test11o = evalo term1                   -- <function>+test12d = evald (term1 `A` (I 2))       -- 4, as Haskell Int+test12o = evalo (term1 `A` (I 2))       -- I 4, but as Term Int+-- test14 = evalo (term1 `A` vx)       -- Type error! Not in scope: `vx'++term2 = L (\vx -> L (\vy -> vx :+ vy))+-- *EvalTaglessI> :t term2+-- term2 :: Term (Int -> Int -> Int)+++test21 = evalo term2+test22 = evalo (term2 `A` (I 1))            -- <function>+test23d = evald (term2 `A` (I 1) `A` (I 2)) -- 3+test23o = evalo (term2 `A` (I 1) `A` (I 2)) -- I 3++termid = L(\vx -> vx)+testid = evald termid -- testid :: t1 -> t1++term2a = L (\vx -> L(\vy -> vx `A` vy))+{- The meta-language figured the (polymorphic) type now+ *EvalTaglessI> :t term2a+ term2a :: Term ((t1 -> t2) -> t1 -> t2)+-}++-- No longer hidden problems+-- term3 = L (\vx -> IFZ vx (I 1) vy) -- Not in scope: `vy'++-- The following is a type error, we can't even enter the term+-- term4 = L (\vx -> IFZ vx (I 1) (vx `A` (I 1)))+{- Now we get good error messages!++    Couldn't match expected type `t1 -> Int'+           against inferred type `Int'+      Expected type: Term (t1 -> Int)+      Inferred type: Term Int+    In the first argument of `A', namely `vx'+    In the third argument of `IFZ', namely `(vx `A` (I 1))'+-}+++-- term6  = (L "x" (I 1)) `A` vy  -- Not in scope: `vy'+++-- (x+1)*y = x*y + y++-- why is this less of a cheating? Try showing the term+-- Now, both type-checking and evaluation of tmul1 works!+tmul1 = L (\vx -> L (\vy ->+          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy))))++-- tmul1 :: Term (Int -> Int -> Int)++testm1d = evald (tmul1 `A` (I 2) `A` (I 3))  -- 6+testm1o = evalo  (tmul1 `A` (I 2) `A` (I 3)) -- I 6++-- Can termY be typechecked?+-- delta = L (\vy -> vy `A` vy)+{-+    Occurs check: cannot construct the infinite type: t1 = t1 -> t2+      Expected type: Term t1+      Inferred type: Term (t1 -> t2)+    In the second argument of `A', namely `vy'+    In the expression: vy `A` vy+-}++tmul = Fix (L (\self -> L (\vx -> L (\vy ->+          (IFZ vx (I 0)+            ((self `A` (vx :+ (I (-1))) `A` vy) :+ vy))))))++testm21d = evald tmul+testm21o = evalo tmul+testm23d = evald (tmul `A` (I 2) `A` (I 3)) -- 6+testm23o = evalo (tmul `A` (I 2) `A` (I 3)) -- I 6++-- Tests of let (cf. the corresponding tests in TInfLetP.hs)++testl1 = let vx = vx in vx               -- why this works in Haskell?+-- testl2 = let vx = vy in (I 1)            -- type error+testl3 = evald $ let vx = I 1 in vx :+ vx -- 2++-- this is essentially the test of hygiene+testl5  = evald $ L(\vx -> let vy = vx `A` (I 1) in L(\vx -> vy :+ vx))+-- testl5 :: (Int -> Int) -> Int -> Int++-- lambda vs. let-bound variables+testl61 = evald $ L(\vx -> let vy = vx `A` (I 1) in+                           let vz = vy :+ (I 2) in vy)+-- testl61 :: (Int -> Int) -> Int+testl62 = evald $ L(\vx -> let vy = vx `A` (I 1) in+                           let vz = vy :+ (I 2) in vx)+-- testl62 :: (Int -> Int) -> Int -> Int+testl63 = evald $ L(\vx -> let vy = vx `A` (I 1) in+                           let vz = (I 2) in vx)+-- testl63 :: (Int -> t2) -> Int -> t2++-- Tests from Cardelli, Basic Polymorphic Type Checking, Ex3+testl66 = evald $ L(\vx -> let vy = vx in+                           let vz = vy `A` (I 1) :+ (I 2) in vy)+-- testl66 :: (Int -> Int) -> Int -> Int, monomorphic++{-+testl67 = evald $ L(\vx -> let vy = vx +                           in ((vy `A` (I 1)) :+ (vy `A` L (\vx->vx))))+-}+-- Couldn't match expected type `Int' against inferred type `t1 -> t1'++-- more intricate tests+testl69 = evald $ L(\f -> let g = L(\x -> let vy = A f x in x)+                         in g)+-- testl69 :: (t1 -> t2) -> t1 -> t1++{-+testl6a = evald $ L(\f -> let g = L(\x -> let vy = A f x in x)+                         in A g g)+-- Occurs check: cannot construct the infinite type: t1 = t1 -> t1+-}+++testl71 = evald $ let vx = term2a in vx+-- testl71 :: (t1 -> t2) -> t1 -> t2++testl72 = evald $ let vx = term2a in +                  let vy = vx `A` termid in+                  let vz = vy `A` (I 2) in vx+-- testl72 :: (t1 -> t2) -> t1 -> t2++testl73 = evald $ let vx = term2a in +                  let vy = vx `A` termid in+                  let vz = vy `A` (I 2) in vy+-- testl73 :: t2 -> t2+testl74 = evald $ let vx = term2a in +                  let vy = let z = vx `A` tmul in vx `A` termid+                  in vy+-- testl74 :: t2 -> t2+testl75 = evald $ let vx = term2a in +                  let vy = let z = vx `A` termid in z+                  in vy+-- testl75 :: t2 -> t2++testl76 = evald $ let vx = L(\y -> I 10) in+                  let vy = vx in+                  let z  = vy `A` (I 1) :+ (I 2) in vy+-- testl76 :: t1 -> Int, polymorhic+testl77 = evald $ let vx = L(\y -> I 10) in+                  let vy = vx+                  in (vy `A` (I 1)) :+ (vy `A` (L(\vx->vx)))+-- 20::Int, OK.+++term2id = let id = L(\vx ->vx) in+          L(\f -> L(\vy -> +               ((I 2) :++                ((id `A` f) `A` ((id `A` vy) :+ (I 1))))))+test2id = evald term2id+-- test2id :: (Int -> Int) -> Int -> Int++termlet = let c2 = L(\f -> L(\vx -> f `A` (f `A` vx))) in+          let inc = L(\vx -> vx :+ (I 1)) in+          let compose = L(\f -> L(\g -> L(\vx -> f `A` (g `A` vx)))) in+          let id = L(\vx -> vx) in+          c2 `A` (compose `A` inc `A` inc) `A` (I 10) :++          ((c2 `A` (compose `A` inc) `A` id) `A` (I 100))+testlet = evald termlet -- 116

@@ -0,0 +1,123 @@+-- | Simply-typed Church-style (nominal) lambda-calculus+-- with integers and zero-comparison+-- Type checking+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.TEvalNC where++data Typ = TInt | !Typ :> !Typ deriving (Show, Eq)+infixr 9 :>++data Term = V VarName+          | L VarName Typ Term+          | A Term Term+          | I Int+          | Term :+ Term                -- addition+          | IFZ Term Term Term          -- if zero+          | Fix Term                    -- fix f, where f :: (a->b)->(a->b)+            deriving (Show, Eq)++infixl 9 `A`+type VarName = String++-- | Type Environment: associating types with `free' variables+type TEnv = [(VarName, Typ)]++env0 :: TEnv+env0 = []++lkup :: TEnv -> VarName -> Typ+lkup env x = maybe err id $ lookup x env + where err = error $ "Unbound variable " ++ x++ext :: TEnv -> (VarName,Typ) -> TEnv+ext env xt = xt : env++-- | Type reconstruction: abstract evaluation+teval :: TEnv -> Term -> Typ+teval env (V x) = lkup env x+teval env (L x t e) = t :> teval (ext env (x,t)) e+teval env (A e1 e2) = +    let t1 = teval env e1+        t2 = teval env e2+    in case t1 of+       t1a :> t1r | t1a == t2 -> t1r+       t1a :> t1r -> error $ unwords ["Applying a function of arg type",+                                      show t1a, "to argument of type",+                                      show t2]+       t1 -> error $ "Trying to apply a non-function: " ++ show t1++teval env (I n) = TInt+teval env (e1 :+ e2) =+    let t1 = teval env e1+        t2 = teval env e2+    in case (t1,t2) of+       (TInt, TInt) -> TInt+       ts     -> error $ "Trying to add non-integers: " ++ show ts+teval env (IFZ e1 e2 e3) =+    let t1 = teval env e1+        t2 = teval env e2+        t3 = teval env e3+    in case t1 of+       TInt | t2 == t3 -> t2+       TInt -> error $ unwords ["Branches of IFZ have different types:",+                                show t2, "and", show t3]+       t    -> error $ "Trying to compare a non-integer to 0: " ++ show t++teval env (Fix e) =+    let t = teval env e+    in case t of+       ((ta1 :> tb1) :> (ta2 :> tb2)) | ta1 == ta2 && tb1 == tb2 +           -> ta1 :> tb1+       t -> error $ "Inappropriate type in Fix: " ++ show t++(vx,vy) = (V "x",V "y")++term1 = L "x" TInt (IFZ vx (I 1) (vx :+ (I 2)))++test1 = teval env0 term1 -- TInt :> TInt++term2a = L "x" TInt (L "y" TInt (vx `A` vy))+test2a = teval env0 term2a++term2b = L "x" (TInt :> TInt) (L "y" TInt (vx `A` vy))+test2b = teval env0 term2b -- (TInt :> TInt) :> (TInt :> TInt)++-- can we write term2c with a different assignment of types to x and y?++-- | Used to be hidden problem. The main benefit of types: static approximation+-- of program behavior+term3 = L "x" TInt (IFZ vx (I 1) vy)+test3 = teval env0 term3++term4a = L "x" TInt (IFZ vx (I 1) (vx `A` (I 1)))+test4a = teval env0 term4a++term4b = L "x" (TInt :> TInt) (IFZ vx (I 1) (vx `A` (I 1)))+test4b = teval env0 term4b++term6  = (L "x" TInt (I 1)) `A` vy+test61 = teval env0 term6+++tmul1 = L "x" TInt (L "y" TInt+          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy)))++testm1 = teval env0 tmul1 -- is typechecking really decidable?++-- Can termY be typechecked?+delta = L "y" (TInt :> TInt) (vy `A` vy)+testd = teval env0 delta ++tmul = Fix (L "self" (TInt :> TInt :> TInt) (L "x" TInt (L "y" TInt+          (IFZ vx (I 0)+            (((V "self") `A` (vx :+ (I (-1))) `A` vy) :+ vy)))))++testm21 = teval env0 tmul                       -- TInt :> (TInt :> TInt)+testm22 = teval env0 (tmul `A` (I 2))           -- TInt :> TInt+testm23 = teval env0 (tmul `A` (I 2) `A` (I 3)) -- TInt+testm24 = teval env0 (tmul `A` (I (-1)) `A` (I (-1))) -- TInt+

@@ -0,0 +1,135 @@+-- | Simply-typed Church-style (nominal) lambda-calculus+-- with integers and zero-comparison+-- Type reconstruction, for all subterms+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.TEvalNR where++import qualified Data.Map as M++data Typ = TInt | !Typ :> !Typ deriving (Show, Eq)+infixr 9 :>++data Term = V VarName+          | L VarName Typ Term+          | A Term Term+          | I Int+          | Term :+ Term                -- addition+          | IFZ Term Term Term          -- if zero+          | Fix Term                    -- fix f, where f :: (a->b)->(a->b)+            deriving (Show, Eq)++infixl 9 `A`+type VarName = String++-- | Type Environment: associating types with `free' variables+type TEnv = [(VarName, Typ)]++env0 :: TEnv+env0 = []++lkup :: TEnv -> VarName -> Typ+lkup env x = maybe err id $ lookup x env + where err = error $ "Unbound variable " ++ x++ext :: TEnv -> (VarName,Typ) -> TEnv+ext env xt = xt : env++-- | A virtual typed AST: associating a type to each subterm+type TermIndex = [Int]                  -- an index of a subterm in a term+type Typs = M.Map TermIndex Typ+topterm :: Typ -> Typs+topterm = M.singleton []+toptyp :: Typs -> Typ+toptyp ts = (M.!) ts []+shift :: Int -> Typs -> Typs+shift n = M.mapKeys (n:) ++-- | Type reconstruction: abstract evaluation+teval :: TEnv -> Term -> Typs+teval env (V x) = topterm $ lkup env x+teval env (L x t e) = +    let ts = teval (ext env (x,t)) e+    in topterm (t :> toptyp ts) `M.union` shift 0 ts+teval env (A e1 e2) = +    let t1 = teval env e1+        t2 = teval env e2+    in case toptyp t1 of+       t1a :> t1r | t1a == toptyp t2 -> +                   topterm t1r `M.union` shift 0 t1 `M.union` shift 1 t2+       t1a :> t1r -> error $ unwords ["Applying a function of arg type",+                                      show t1a, "to argument of type",+                                      show $ toptyp t2]+       t1 -> error $ "Trying to apply a non-function: " ++ show t1++teval env (I n) = topterm TInt+teval env (e1 :+ e2) =+    let t1 = teval env e1+        t2 = teval env e2+    in case (toptyp t1,toptyp t2) of+       (TInt, TInt) -> +           topterm TInt `M.union` shift 0 t1 `M.union` shift 1 t2+       ts     -> error $ "Trying to add non-integers: " ++ show ts+teval env (IFZ e1 e2 e3) =+    let t1 = teval env e1+        t2 = teval env e2+        t3 = teval env e3+        tr  = shift 0 t1 `M.union` shift 1 t2 `M.union` shift 2 t3+    in case toptyp t1 of+       TInt | toptyp t2 == toptyp t3 -> topterm (toptyp t2) `M.union` tr+       TInt -> error $ unwords ["Branches of IFZ have different types:",+                                show (toptyp t2), "and", show (toptyp t3)]+       t    -> error $ "Trying to compare a non-integer to 0: " ++ show t++teval env (Fix e) =+    let t = teval env e+    in case toptyp t of+       ((ta1 :> tb1) :> (ta2 :> tb2)) | ta1 == ta2 && tb1 == tb2 +           -> topterm (ta1 :> tb1) `M.union` shift 0 t+       t -> error $ "Inappropriate type in Fix: " ++ show t++(vx,vy) = (V "x",V "y")++term1 = L "x" TInt (IFZ vx (I 1) (vx :+ (I 2)))++test1 = teval env0 term1 -- TInt :> TInt++term2a = L "x" TInt (L "y" TInt (vx `A` vy))+test2a = teval env0 term2a++term2b = L "x" (TInt :> TInt) (L "y" TInt (vx `A` vy))+test2b = teval env0 term2b -- (TInt :> TInt) :> (TInt :> TInt)++-- can we write term2c with a different assignment of types to x and y?++-- Used to be hidden problem. The main benefit of types: static approximation+-- of program behavior+term3 = L "x" TInt (IFZ vx (I 1) vy)+test3 = teval env0 term3++term4a = L "x" TInt (IFZ vx (I 1) (vx `A` (I 1)))+test4a = teval env0 term4a++term4b = L "x" (TInt :> TInt) (IFZ vx (I 1) (vx `A` (I 1)))+test4b = teval env0 term4b+++tmul1 = L "x" TInt (L "y" TInt+          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy)))++testm1 = teval env0 tmul1 -- is typechecking really decidable?++-- Can termY be typechecked?+delta = L "y" (TInt :> TInt) (vy `A` vy)+testd = teval env0 delta ++tmul = Fix (L "self" (TInt :> TInt :> TInt) (L "x" TInt (L "y" TInt+          (IFZ vx (I 0)+            (((V "self") `A` (vx :+ (I (-1))) `A` vy) :+ vy)))))++testm21 = teval env0 tmul                       -- TInt :> (TInt :> TInt)+testm22 = teval env0 (tmul `A` (I 2))           -- TInt :> TInt+testm23 = teval env0 (tmul `A` (I 2) `A` (I 3)) -- TInt 

@@ -0,0 +1,322 @@+{-# LANGUAGE PatternGuards #-}+-- | Simply-typed Curry-style (nominal) lambda-calculus+-- with integers and zero-comparison+-- Let-polymorphism via inlining+-- Type inference+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.TInfLetI where++import qualified Data.IntMap as M+import Control.Monad.State.Strict               -- why needed strict?+-- import Control.Monad.State.Lazy              -- if enable this, run test62++data Typ = TInt | !Typ :> !Typ | TV TVarName deriving (Show, Eq)+infixr 9 :>+type TVarName = Int++data Term = V VarName+          | L VarName Term+          | A Term Term+          | I Int+          | Term :+ Term                -- addition+          | IFZ Term Term Term          -- if zero+          | Fix Term                    -- fix f, where f :: (a->b)->(a->b)+          | Let (VarName,Term) Term+            deriving (Show, Eq)++infixl 9 `A`+type VarName = String++-- | Type Environment: associating *would-be* types with `free' term variables+type TEnv = [(VarName, TVEM Typ)]++env0 :: TEnv+env0 = []++lkup :: TEnv -> VarName -> TVEM Typ+lkup env x = maybe err id $ lookup x env + where err = error $ "Unbound variable " ++ x++ext :: TEnv -> (VarName,TVEM Typ) -> TEnv+ext env xt = xt : env++-- | Type Variable Environment: associating types with `free' type variables+data TVE = TVE Int (M.IntMap Typ) deriving Show++-- | TVE is the state of a monadic computation+type TVEM = State TVE++-- | Allocate a fresh type variable (see the first component of TVE)+newtv :: TVEM Typ+newtv = do+ TVE n s <- get+ put (TVE (succ n) s)+ return (TV n)++tve0 :: TVE+tve0 = TVE 0 M.empty++tvlkup :: TVE -> TVarName -> Maybe Typ+tvlkup (TVE _ s) v = M.lookup v s++tvext :: TVE -> (TVarName,Typ) -> TVE+tvext (TVE c s) (tv,t) = TVE c $ M.insert tv t s++-- | Type variables are logic variables: hypothetical reasoning+tvsub :: TVE -> Typ -> Typ+tvsub tve (t1 :> t2) = tvsub tve t1 :> tvsub tve t2+tvsub tve (TV v) | Just t <- tvlkup tve v = tvsub tve t+tvsub tve t = t++-- | `shallow' substitution; check if tv is bound to anything `substantial'+tvchase :: TVE -> Typ -> Typ+tvchase tve (TV v) | Just t <- tvlkup tve v = tvchase tve t+tvchase _ t = t++-- | The unification. If unification failed, return the reason+unify :: Typ -> Typ -> TVE -> Either String TVE+unify t1 t2 tve = unify' (tvchase tve t1) (tvchase tve t2) tve++-- | If either t1 or t2 are type variables, they are definitely unbound+unify' :: Typ -> Typ -> TVE -> Either String TVE+unify' TInt TInt = Right+unify' (t1a :> t1r) (t2a :> t2r) = either Left (unify t1r t2r) . unify t1a t2a+unify' (TV v1) t2 = unifyv v1 t2+unify' t1 (TV v2) = unifyv v2 t1+unify' t1 t2 = const (Left $ unwords ["constant mismatch:",show t1,"and",+                                      show t2])++-- | Unify a free variable v1 with t2+unifyv :: TVarName -> Typ -> TVE -> Either String TVE+unifyv v1 (TV v2) tve =+    if v1 == v2 then Right tve+       else Right (tvext tve (v1,TV v2)) -- record new constraint+unifyv v1 t2 tve = if occurs v1 t2 tve+                      then Left $ unwords ["occurs check:",show (TV v1),+                                           "in",show $ tvsub tve t2]+                      else Right (tvext tve (v1,t2))++-- | The occurs check: if v appears free in t+occurs :: TVarName -> Typ -> TVE -> Bool+occurs v TInt _ = False+occurs v (t1 :> t2) tve = occurs v t1 tve || occurs v t2 tve+occurs v (TV v2) tve =+    case tvlkup tve v2 of+         Nothing -> v == v2+         Just t  -> occurs v t tve++-- | Monadic version of unify+unifyM :: Typ -> Typ -> (String -> String) -> TVEM ()+unifyM t1 t2 errf = do+  tve <- get+  case unify t1 t2 tve of +       Right tve -> put tve+       Left  err -> fail (errf err)+++-- | Type reconstruction: abstract evaluation+teval' :: TEnv -> Term -> TVEM Typ+teval' env (V x)   = lkup env x+teval' env (L x e) = do+    tv <- newtv+    te <- teval' (ext env (x,return tv)) e+    return $ tv :> te+teval' env (A e1 e2) = do+    t1  <- teval' env e1+    t2  <- teval' env e2+    t1r <- newtv+    unifyM t1 (t2 :> t1r) id+    return t1r++teval' env (I n) = return TInt+teval' env (e1 :+ e2) = do+    t1 <- teval' env e1+    t2 <- teval' env e2+    unifyM t1 TInt ("Trying to add non-integers: " ++)+    unifyM t2 TInt ("Trying to add non-integers: " ++)+    return TInt+teval' env (IFZ e1 e2 e3) = do+    t1 <- teval' env e1+    t2 <- teval' env e2+    t3 <- teval' env e3+    unifyM t1 TInt ("Trying to compare a non-integer to 0: " ++)+    unifyM t2 t3 (\err  -> unwords ["Branches of IFZ have different",+                                    "types. Unification failed:",err])+    return t2++teval' env (Fix e) = do+    t  <- teval' env e+    ta <- newtv+    tb <- newtv+    unifyM t ((ta :> tb) :> (ta :> tb))+           ("Inappropriate type in Fix: " ++)+    return $ ta :> tb++-- | A new clause: type-checking Let+teval' env (Let (x,e) eb) = do+    _  <- teval' env e                  -- what is the point of this?+    teval' (ext env (x,teval' env e)) eb++-- | Resolve all type variables, as far as possible+teval :: TEnv -> Term -> Typ+teval tenv e = let (t,tve) = runState (teval' tenv e) tve0 in tvsub tve t++-- Tests+(vx,vy) = (V "x",V "y")++test0 = runState (teval' env0 ((L "x" (vx :+ (I 2))) `A` (I 1))) tve0+-- (TV 1,TVE 2 (fromList [(0,TInt),(1,TInt)]))++term1 = L "x" (IFZ vx (I 1) (vx :+ (I 2)))+test10 = runState (teval' env0 term1) tve0+-- (TV 0 :> TInt,TVE 1 (fromList [(0,TInt)]))++-- need a better presentation of the final result: cf. teval' and teval++test1 = teval env0 term1 -- TInt :> TInt++termid = L "x" vx+testid = teval env0 termid -- TV 0 :> TV 0++term2a = L "x" (L "y" (vx `A` vy))+test2a = teval env0 term2a+-- (TV 1 :> TV 2) :> (TV 1 :> TV 2)++-- Used to be a hidden problem. The main benefit of types: static approximation+-- of program behavior+term3 = L "x" (IFZ vx (I 1) vy)+test3 = teval env0 term3++term4 = L "x" (IFZ vx (I 1) (vx `A` (I 1)))+test4 = teval env0 term4+-- compare the error message with that of test4a and test4b in TEvalNC.hs++term6  = (L "x" (I 1)) `A` vy+test61 = teval env0 term6++test62 = teval env0 $ (I 1) :+ vx       -- If the state is Lazy: problem+++tmul1 = L "x" (L "y"+          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy)))++testm1 = teval env0 tmul1 -- is typechecking really decidable?++-- Can termY be typechecked?+delta = L "y" (vy `A` vy)+testd = teval env0 delta ++tmul = Fix (L "self" (L "x" (L "y"+          (IFZ vx (I 0)+            (((V "self") `A` (vx :+ (I (-1))) `A` vy) :+ vy)))))++testm21' = runState (teval' env0 tmul) tve0+-- (TV 5 :> TV 6,TVE 7 (fromList +--     [(0,TInt :> TV 3),(1,TInt),(2,TInt),(3,TV 2 :> TV 4),+--      (4,TInt),(5,TInt),(6,TV 2 :> TV 4)]))++testm21 = teval env0 tmul                       -- TInt :> (TInt :> TInt)+testm22 = teval env0 (tmul `A` (I 2))           -- TInt :> TInt+testm23 = teval env0 (tmul `A` (I 2) `A` (I 3)) -- TInt+++-- Tests of let++testl1 = teval env0 $ Let ("x",vx) vx            -- error+testl2 = teval env0 $ Let ("x",vy) (I 1)         -- error+testl3 = teval env0 $ Let ("x",(I 1)) (vx :+ vx) -- TInt++-- these are essentially tests of hygiene+testl4  = teval env0 $ L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2)))+-- (TInt :> TInt) :> TInt+testl42 = teval env0 $ (L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2))))+                      `A` termid+testl43 = teval env0 $ (L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2))))+                      `A` term2a+-- type error++testl5  = teval env0 $ L "x" (Let ("y",vx `A` (I 1)) (L "x" (vy :+ vx)))+-- (TInt :> TInt) :> (TInt :> TInt)++-- lambda vs. let-bound variables+testl61 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))+                               (Let ("z",vy :+ (I 2)) vy))+-- (TInt :> TInt) :> TInt+testl62 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))+                               (Let ("z",vy :+ (I 2)) vx))+-- (TInt :> TInt) :> (TInt :> TInt)+testl63 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))+                               (Let ("z",(I 2)) vx))+-- (TInt :> TV 1) :> (TInt :> TV 1)++-- Tests from Cardelli, Basic Polymorphic Type Checking, Ex3+testl66 = teval env0 $ L "x" (Let ("y",vx) +                              (Let ("z",(vy `A` (I 1) :+ (I 2))) vy))+-- (TInt :> TInt) :> (TInt :> TInt), monomorphic+testl67 = teval env0 $ L "x" (Let ("y",vx) ((vy `A` (I 1)) :++                                            (vy `A` (L "x" vx))))+-- *** Exception: constant mismatch: TInt and TV 2 :> TV 2++-- more intricate tests+testl69 = teval env0 (L "f" $+                           Let ("g", L "x" $ Let ("y", A (V "f") (V "x"))+                                                 (V "x"))+                               (V "g"))+-- (TV 3 :> TV 4) :> (TV 3 :> TV 3)++testl6a = teval env0 (L "f" $+                           Let ("g", L "x" $ Let ("y", A (V "f") (V "x"))+                                                 (V "x"))+                               (A (V "g") (V "g")))+-- *** Exception: occurs check: TV 5 in TV 5 :> TV 5+++testl71 = teval env0 $ Let ("x",term2a) vx+-- (TV 4 :> TV 5) :> (TV 4 :> TV 5)++testl72 = teval env0 $ Let ("x",term2a) (Let ("y",vx `A` termid)+                               (Let ("z",vy `A` (I 2)) vx))+-- (TV 15 :> TV 16) :> (TV 15 :> TV 16)++testl73 = teval env0 $ Let ("x",term2a) (Let ("y",vx `A` termid)+                               (Let ("z",vy `A` (I 2)) vy))+-- TV 17 :> TV 17+testl74 = teval env0 $ Let ("x",term2a) +                        (Let ("y",(Let ("z",vx `A` tmul) (vx `A` termid)))+                         vy)+-- TV 33 :> TV 33+testl75 = teval env0 $ Let ("x",term2a) +                        (Let ("y",(Let ("z",(vx `A` termid)) (V "z")))+                         vy)+-- TV 21 :> TV 21++testl76 = teval env0 $ Let ("x",(L "y" (I 10))) +                           (Let ("y",vx)+                            (Let ("z",(vy `A` (I 1) :+ (I 2))) vy))+-- TV 4 :> TInt, polymorhic+testl77 = teval env0 $ Let ("x",(L "y" (I 10)))+                           (Let ("y",vx) ((vy `A` (I 1)) :++                                          (vy `A` (L "x" vx))))+-- TInt, OK.++-- compared to the corresponding tests in TInfT.hs, we are using+-- the object-level Let+term2id = Let ("id",L "x" vx) (+          L "f" (L "y" +               ((I 2) :++                ((V "id" `A` (V "f")) `A` ((V "id" `A` vy) :+ (I 1))))))+test2id = teval env0 term2id -- (TInt :> TInt) :> (TInt :> TInt)++termlet = Let ("c2", L "f" (L "x" (V "f" `A` (V "f" `A` vx)))) (+          Let ("inc", L "x" (vx :+ (I 1))) (+          Let ("compose", L "f" (L "g" (L "x" (V "f" `A` (V "g" `A` vx))))) (+          Let ("id",L "x" vx) (+          V "c2" `A` (V "compose" `A` V "inc" `A` V "inc") `A` (I 10) :++          (V "c2" `A` (V "compose" `A` V "inc") `A` V "id" `A` (I 100))+          ))))+testlet = teval env0 termlet -- TInt+

@@ -0,0 +1,411 @@+{-# LANGUAGE PatternGuards #-}+-- | Simply-typed Curry-style (nominal) lambda-calculus+-- with integers and zero-comparison+-- Let-polymorphism via type schemes+-- Type inference+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.TInfLetP where++import Data.List (nub)+import qualified Data.IntMap as M+import Control.Monad.State.Strict               -- why needed strict?+-- import Control.Monad.State.Lazy              -- if enable this, run test62++data Typ = TInt | !Typ :> !Typ | TV TVarName deriving (Show, Eq)+infixr 9 :>+type TVarName = Int++data TypS = TypS [TVarName] Typ         -- A type scheme, with n quantified+   deriving Show                        -- type variables (n >= 0)++data Term = V VarName+          | L VarName Term+          | A Term Term+          | I Int+          | Term :+ Term                -- addition+          | IFZ Term Term Term          -- if zero+          | Fix Term                    -- fix f, where f :: (a->b)->(a->b)+          | Let (VarName,Term) Term+            deriving (Show, Eq)++infixl 9 `A`+type VarName = String++-- | Type Environment: associating *would-be* types with `free' term variables+type TEnv = [(VarName, TypS)]++env0 :: TEnv+env0 = []++lkup :: TEnv -> VarName -> TypS+lkup env x = maybe err id $ lookup x env + where err = error $ "Unbound variable " ++ x++ext :: TEnv -> (VarName,TypS) -> TEnv+ext env xt = xt : env++-- | Type Variable Environment: associating types with `free' type variables+data TVE = TVE Int (M.IntMap Typ) deriving Show++-- | TVE is the state of a monadic computation+type TVEM = State TVE++-- | Allocate a fresh type variable (see the first component of TVE)+newtv :: TVEM Typ+newtv = do+ TVE n s <- get+ put (TVE (succ n) s)+ return (TV n)++tve0 :: TVE+tve0 = TVE 0 M.empty++tvlkup :: TVE -> TVarName -> Maybe Typ+tvlkup (TVE _ s) v = M.lookup v s++tvext :: TVE -> (TVarName,Typ) -> TVE+tvext (TVE c s) (tv,t) = TVE c $ M.insert tv t s++-- | TVE domain predicate: check to see if a TVarName is in the domain of TVE+tvdomainp :: TVE -> TVarName -> Bool+tvdomainp (TVE _ s) v = M.member v s++-- | Give the list of all type variables that are allocated in TVE but+-- not bound there+tvfree :: TVE -> [TVarName]+tvfree (TVE c s) = filter (\v -> not (M.member v s)) [0..c-1]++-- | Type variables are logic variables: hypothetical reasoning+tvsub :: TVE -> Typ -> Typ+tvsub tve (t1 :> t2) = tvsub tve t1 :> tvsub tve t2+tvsub tve (TV v) | Just t <- tvlkup tve v = tvsub tve t+tvsub tve t = t++-- | `shallow' substitution; check if tv is bound to anything `substantial'+tvchase :: TVE -> Typ -> Typ+tvchase tve (TV v) | Just t <- tvlkup tve v = tvchase tve t+tvchase _ t = t++-- | The unification. If unification failed, return the reason+unify :: Typ -> Typ -> TVE -> Either String TVE+unify t1 t2 tve = unify' (tvchase tve t1) (tvchase tve t2) tve++-- | If either t1 or t2 are type variables, they are definitely unbound+unify' :: Typ -> Typ -> TVE -> Either String TVE+unify' TInt TInt = Right+unify' (t1a :> t1r) (t2a :> t2r) = either Left (unify t1r t2r) . unify t1a t2a+unify' (TV v1) t2 = unifyv v1 t2+unify' t1 (TV v2) = unifyv v2 t1+unify' t1 t2 = const (Left $ unwords ["constant mismatch:",show t1,"and",+                                      show t2])++-- | Unify a free variable v1 with t2+unifyv :: TVarName -> Typ -> TVE -> Either String TVE+unifyv v1 (TV v2) tve =+    if v1 == v2 then Right tve+       else Right (tvext tve (v1,TV v2)) -- record new constraint+unifyv v1 t2 tve = if occurs v1 t2 tve+                      then Left $ unwords ["occurs check:",show (TV v1),+                                           "in",show $ tvsub tve t2]+                      else Right (tvext tve (v1,t2))++-- | The occurs check: if v appears free in t+occurs :: TVarName -> Typ -> TVE -> Bool+occurs v TInt _ = False+occurs v (t1 :> t2) tve = occurs v t1 tve || occurs v t2 tve+occurs v (TV v2) tve =+    case tvlkup tve v2 of+         Nothing -> v == v2+         Just t  -> occurs v t tve++-- | Compute (quite unoptimally) the characteristic function of the set +--  forall tvb \in fv(tve_before). Union fv(tvsub(tve_after,tvb))+tvdependentset :: TVE -> TVE -> (TVarName -> Bool)+tvdependentset tve_before tve_after = +    \tv -> any (\tvb -> occurs tv (TV tvb) tve_after) tvbs+ where+ tvbs = tvfree tve_before+ ++-- | Monadic version of unify+unifyM :: Typ -> Typ -> (String -> String) -> TVEM ()+unifyM t1 t2 errf = do+  tve <- get+  case unify t1 t2 tve of +       Right tve -> put tve+       Left  err -> fail (errf err)++-- | Given a type scheme, that is, the type t and the list of type variables tvs,+-- for every tvs, replace all of its occurrences in t with a fresh+-- type variable.+-- We do that by creating a substitution tve and applying it to t.+instantiate :: TypS -> TVEM Typ+instantiate (TypS tvs t) = do+  tve <- associate_with_freshvars tvs+  return $ tvsub tve t+ where+ associate_with_freshvars [] = return tve0+ associate_with_freshvars (tv:tvs) = do+   tve     <- associate_with_freshvars tvs+   tvfresh <- newtv+   return $ tvext tve (tv,tvfresh)++-- | Given a typechecking action ta yielding the type t, return the type+-- scheme quantifying over _truly free_ type variables in t+-- with respect to TVE that existed before the typechecking action began.+-- Let tve_before is TVE before the type checking action is executed, +-- and tve_after is TVE after the action. A type variable tv+-- is truly free if it is free in tve_after and remains free if the +-- typechecking action were executed in any tve extending tve_before+-- with arbitrary binding to type variables free in tve_before.+-- To be more precise, a type variable tv is truly free with respect+-- to tve_before if:+--    tv \not\in domain(tve_after)+--    forall tvb \in fv(tve_before). tv \not\in fv(tvsub(tve_after,tvb))+-- In other words, tv is truly free if it is free and `independent' of+-- tve_before.+--+-- Our goal is to reproduce the behavior in TInfLetI.hs:+-- generalize/instantiate should mimic multiple executions of+-- the typechecking action. That means we should quantify over all+-- type variables created by ta that are independent of the type environment+-- in which the action may be executed.++generalize :: TVEM Typ -> TVEM TypS+generalize ta = do+ tve_before <- get      -- type env before ta is executed+ t          <- ta+ tve_after  <- get      -- type env after ta is executed+ let t' = tvsub tve_after t+ let tvdep = tvdependentset tve_before tve_after+ let fv = filter (not . tvdep) (nub (freevars t'))+ return $ TypS fv t'++-- | Return the list of type variables in t (possibly with duplicates)+freevars :: Typ -> [TVarName]+freevars TInt       = []+freevars (t1 :> t2) = freevars t1 ++ freevars t2+freevars (TV v)     = [v]+++-- | Type reconstruction: abstract evaluation+teval' :: TEnv -> Term -> TVEM Typ+teval' env (V x)   = instantiate (lkup env x)+teval' env (L x e) = do+    tv <- newtv+    te <- teval' (ext env (x,TypS [] tv)) e -- extend with the monomorphic type+    return $ tv :> te+teval' env (A e1 e2) = do+    t1  <- teval' env e1+    t2  <- teval' env e2+    t1r <- newtv+    unifyM t1 (t2 :> t1r) id+    return t1r++teval' env (I n) = return TInt+teval' env (e1 :+ e2) = do+    t1 <- teval' env e1+    t2 <- teval' env e2+    unifyM t1 TInt ("Trying to add non-integers: " ++)+    unifyM t2 TInt ("Trying to add non-integers: " ++)+    return TInt+teval' env (IFZ e1 e2 e3) = do+    t1 <- teval' env e1+    t2 <- teval' env e2+    t3 <- teval' env e3+    unifyM t1 TInt ("Trying to compare a non-integer to 0: " ++)+    unifyM t2 t3 (\err  -> unwords ["Branches of IFZ have different",+                                    "types. Unification failed:",err])+    return t2++teval' env (Fix e) = do+    t  <- teval' env e+    ta <- newtv+    tb <- newtv+    unifyM t ((ta :> tb) :> (ta :> tb))+           ("Inappropriate type in Fix: " ++)+    return $ ta :> tb++teval' env (Let (x,e) eb) = do+    t  <- generalize $ teval' env e     -- This is new, cf TInfLetI.hs+    teval' (ext env (x,t)) eb+++-- | Resolve all type variables, as far as possible, and generalize+-- We assume teval will be used for top-level expressions where generalization+-- is appropriate.+teval :: TEnv -> Term -> TypS+teval tenv e = let (ts,tve) = runState (generalize $ teval' tenv e) tve0 in ts++-- | non-generalizing teval (as before)+tevalng :: TEnv -> Term -> Typ+tevalng tenv e = let (t,tve) = runState (teval' tenv e) tve0 in tvsub tve t++-- Tests+(vx,vy) = (V "x",V "y")++test0 = runState (teval' env0 ((L "x" (vx :+ (I 2))) `A` (I 1))) tve0+-- (TV 1,TVE 2 (fromList [(0,TInt),(1,TInt)]))++term1 = L "x" (IFZ vx (I 1) (vx :+ (I 2)))+test10 = runState (teval' env0 term1) tve0+-- (TV 0 :> TInt,TVE 1 (fromList [(0,TInt)]))++-- need a better presentation of the final result: cf. teval' and teval++test1 = teval env0 term1 -- TypS [] (TInt :> TInt)++termid = L "x" vx+testid = teval env0 termid -- TypS [0] (TV 0 :> TV 0), i.e., forall a. a->a++term2a = L "x" (L "y" (vx `A` vy))+test2a = teval env0 term2a+-- TypS [2,1] ((TV 1 :> TV 2) :> (TV 1 :> TV 2))++-- Used to be a hidden problem. The main benefit of types: static approximation+-- of program behavior+term3 = L "x" (IFZ vx (I 1) vy)+test3 = teval env0 term3++term4 = L "x" (IFZ vx (I 1) (vx `A` (I 1)))+test4 = teval env0 term4+-- compare the error message with that of test4a and test4b in TEvalNC.hs++term6  = (L "x" (I 1)) `A` vy+test61 = teval env0 term6++test62 = teval env0 $ (I 1) :+ vx       -- If the state is Lazy: problem+++tmul1 = L "x" (L "y"+          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy)))++testm1 = teval env0 tmul1 -- is typechecking really decidable?++-- Can termY be typechecked?+delta = L "y" (vy `A` vy)+testd = teval env0 delta ++tmul = Fix (L "self" (L "x" (L "y"+          (IFZ vx (I 0)+            (((V "self") `A` (vx :+ (I (-1))) `A` vy) :+ vy)))))++testm21' = runState (teval' env0 tmul) tve0+-- (TV 5 :> TV 6,TVE 7 (fromList +--     [(0,TInt :> TV 3),(1,TInt),(2,TInt),(3,TV 2 :> TV 4),+--      (4,TInt),(5,TInt),(6,TV 2 :> TV 4)]))++testm21 = teval env0 tmul                  -- TypS [] (TInt :> (TInt :> TInt))+testm22 = teval env0 (tmul `A` (I 2))           -- TypS [] (TInt :> TInt)+testm23 = teval env0 (tmul `A` (I 2) `A` (I 3)) -- TypS [] TInt+++-- Tests of let++testl1 = teval env0 $ Let ("x",vx) vx            -- error+testl2 = teval env0 $ Let ("x",vy) (I 1)         -- error+testl3 = teval env0 $ Let ("x",(I 1)) (vx :+ vx) -- TypS [] TInt++-- these are essentially tests of hygiene+testl40 = runState (teval' env0 (L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2)))))+                   tve0+testl4  = teval env0 $ L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2)))+-- TypS [] ((TInt :> TInt) :> TInt)+testl42 = teval env0 $ (L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2))))+                      `A` termid+testl43 = teval env0 $ (L "x" (Let ("x",vx `A` (I 1)) (vx :+ (I 2))))+                      `A` term2a+-- type error++testl5  = teval env0 $ L "x" (Let ("y",vx `A` (I 1)) (L "x" (vy :+ vx)))+-- TypS [] ((TInt :> TInt) :> (TInt :> TInt))++terml51 = L "x" (Let ("y",L"f" ((V "f") `A` vx)) vy)+testl51  = teval env0 terml51 -- TypS [3,0] (TV 0 :> ((TV 0 :> TV 3) :> TV 3))+terml52 = terml51 `A` (I 10)+testl52  = teval env0 terml52 -- TypS [3] ((TInt :> TV 3) :> TV 3)++-- lambda vs. let-bound variables+testl61 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))+                               (Let ("z",vy :+ (I 2)) vy))+-- TypS [] ((TInt :> TInt) :> TInt)+testl62 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))+                               (Let ("z",vy :+ (I 2)) vx))+-- TypS [] ((TInt :> TInt) :> (TInt :> TInt))+testl63 = teval env0 $ L "x" (Let ("y",vx `A` (I 1))+                               (Let ("z",(I 2)) vx))+-- TypS [1] ((TInt :> TV 1) :> (TInt :> TV 1))++-- Tests from Cardelli, Basic Polymorphic Type Checking, Ex3+testl66 = teval env0 $ L "x" (Let ("y",vx) +                              (Let ("z",(vy `A` (I 1) :+ (I 2))) vy))+-- TypS [] ((TInt :> TInt) :> (TInt :> TInt)), monomorphic+testl67 = teval env0 $ L "x" (Let ("y",vx) ((vy `A` (I 1)) :++                                            (vy `A` (L "x" vx))))+-- *** Exception: constant mismatch: TInt and TV 2 :> TV 2+++-- more intricate tests+testl69 = teval env0 (L "f" $+                           Let ("g", L "x" $ Let ("y", A (V "f") (V "x"))+                                                 (V "x"))+                               (V "g"))+-- TypS [1,2] ((TV 1 :> TV 2) :> (TV 1 :> TV 1))++testl6a = teval env0 (L "f" $+                           Let ("g", L "x" $ Let ("y", A (V "f") (V "x"))+                                                 (V "x"))+                               (A (V "g") (V "g")))+-- *** Exception: occurs check: TV 1 in TV 1 :> TV 1+++testl71 = teval env0 $ Let ("x",term2a) vx+-- TypS [4,3] ((TV 3 :> TV 4) :> (TV 3 :> TV 4))++testl72 = teval env0 $ Let ("x",term2a) (Let ("y",vx `A` termid)+                               (Let ("z",vy `A` (I 2)) vx))+-- TypS [10,9] ((TV 9 :> TV 10) :> (TV 9 :> TV 10))++testl73 = teval env0 $ Let ("x",term2a) (Let ("y",vx `A` termid)+                               (Let ("z",vy `A` (I 2)) vy))+-- TypS [9] (TV 9 :> TV 9)+testl74 = teval env0 $ Let ("x",term2a) +                        (Let ("y",(Let ("z",vx `A` tmul) (vx `A` termid)))+                         vy)+-- TypS [17] (TV 17 :> TV 17)+testl75 = teval env0 $ Let ("x",term2a) +                        (Let ("y",(Let ("z",(vx `A` termid)) (V "z")))+                         vy)+-- TypS [8] (TV 8 :> TV 8)++testl76 = teval env0 $ Let ("x",(L "y" (I 10))) +                           (Let ("y",vx)+                            (Let ("z",(vy `A` (I 1) :+ (I 2))) vy))+-- TypS [4] (TV 4 :> TInt), polymorhic+testl77 = teval env0 $ Let ("x",(L "y" (I 10)))+                           (Let ("y",vx) ((vy `A` (I 1)) :++                                          (vy `A` (L "x" vx))))+-- TypS [] TInt, OK.++-- compared to the corresponding tests in TInfT.hs, we are using+-- the object-level Let+term2id = Let ("id",L "x" vx) (+          L "f" (L "y" +               ((I 2) :++                ((V "id" `A` (V "f")) `A` ((V "id" `A` vy) :+ (I 1))))))+test2id = teval env0 term2id+-- TypS [] ((TInt :> TInt) :> (TInt :> TInt))++termlet = Let ("c2", L "f" (L "x" (V "f" `A` (V "f" `A` vx)))) (+          Let ("inc", L "x" (vx :+ (I 1))) (+          Let ("compose", L "f" (L "g" (L "x" (V "f" `A` (V "g" `A` vx))))) (+          Let ("id",L "x" vx) (+          V "c2" `A` (V "compose" `A` V "inc" `A` V "inc") `A` (I 10) :++          (V "c2" `A` (V "compose" `A` V "inc") `A` V "id" `A` (I 100))+          ))))+testlet = teval env0 termlet -- TypS [] TInt+

@@ -0,0 +1,219 @@+-- | Simply-typed Curry-style (nominal) lambda-calculus+-- with integers and zero-comparison+-- Type inference+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.TInfT where++import qualified Data.IntMap as M++data Typ = TInt | !Typ :> !Typ | TV TVarName deriving (Show, Eq)+infixr 9 :>+type TVarName = Int++data Term = V VarName+          | L VarName Term+          | A Term Term+          | I Int+          | Term :+ Term                -- addition+          | IFZ Term Term Term          -- if zero+          | Fix Term                    -- fix f, where f :: (a->b)->(a->b)+            deriving (Show, Eq)++infixl 9 `A`+type VarName = String++-- | Type Environment: associating types with `free' term variables+type TEnv = [(VarName, Typ)]++env0 :: TEnv+env0 = []++lkup :: TEnv -> VarName -> Typ+lkup env x = maybe err id $ lookup x env + where err = error $ "Unbound variable " ++ x++ext :: TEnv -> (VarName,Typ) -> TEnv+ext env xt = xt : env++--  |Type Variable Environment: associating types with `free' type variables+data TVE = TVE Int (M.IntMap Typ) deriving Show++--  |Allocate a fresh type variable (see the first component of TVE)+newtv :: TVE -> (Typ,TVE)+newtv (TVE n s) = (TV n,TVE (succ n) s)++tve0 :: TVE+tve0 = TVE 0 M.empty++tvlkup :: TVE -> TVarName -> Maybe Typ+tvlkup (TVE _ s) v = M.lookup v s++tvext :: TVE -> (TVarName,Typ) -> TVE+tvext (TVE c s) (tv,t) = TVE c $ M.insert tv t s++-- | Type variables are logic variables: hypothetical reasoning+tvsub :: TVE -> Typ -> Typ+tvsub tve (t1 :> t2) = tvsub tve t1 :> tvsub tve t2+tvsub tve (TV v) | Just t <- tvlkup tve v = tvsub tve t+tvsub tve t = t++-- | `shallow' substitution; check if tv is bound to anything `substantial'+tvchase :: TVE -> Typ -> Typ+tvchase tve (TV v) | Just t <- tvlkup tve v = tvchase tve t+tvchase _ t = t++-- | The unification. If unification failed, return the reason+unify :: Typ -> Typ -> TVE -> Either String TVE+unify t1 t2 tve = unify' (tvchase tve t1) (tvchase tve t2) tve++-- | If either t1 or t2 are type variables, they are definitely unbound+unify' :: Typ -> Typ -> TVE -> Either String TVE+unify' TInt TInt = Right+unify' (t1a :> t1r) (t2a :> t2r) = either Left (unify t1r t2r) . unify t1a t2a+unify' (TV v1) t2 = unifyv v1 t2+unify' t1 (TV v2) = unifyv v2 t1+unify' t1 t2 = const (Left $ unwords ["constant mismatch:",show t1,"and",+                                      show t2])++-- | Unify a free variable v1 with t2+unifyv :: TVarName -> Typ -> TVE -> Either String TVE+unifyv v1 (TV v2) tve =+    if v1 == v2 then Right tve+       else Right (tvext tve (v1,TV v2)) -- record new constraint+unifyv v1 t2 tve = if occurs v1 t2 tve+                      then Left $ unwords ["occurs check:",show (TV v1),+                                           "in",show $ tvsub tve t2]+                      else Right (tvext tve (v1,t2))++-- | The occurs check: if v appears free in t+occurs :: TVarName -> Typ -> TVE -> Bool+occurs v TInt _ = False+occurs v (t1 :> t2) tve = occurs v t1 tve || occurs v t2 tve+occurs v (TV v2) tve =+    case tvlkup tve v2 of+         Nothing -> v == v2+         Just t  -> occurs v t tve+++-- | Type reconstruction: abstract evaluation+teval' :: TEnv -> Term -> (TVE -> (Typ,TVE))+teval' env (V x)   = \tve0 -> (lkup env x,tve0)+teval' env (L x e) = \tve0 ->+    let (tv,tve1) = newtv tve0+        (te,tve2) = teval' (ext env (x,tv)) e tve1+    in (tv :> te,tve2)+teval' env (A e1 e2) = \tve0 ->+    let (t1,tve1) = teval' env e1 tve0+        (t2,tve2) = teval' env e2 tve1+        (t1r,tve3)= newtv tve2+    in case unify t1 (t2 :> t1r) tve3 of+       Right tve -> (t1r,tve)+       Left err  -> error $ err++teval' env (I n) = \tve0 -> (TInt,tve0)+teval' env (e1 :+ e2) = \tve0 ->+    let (t1,tve1) = teval' env e1 tve0+        (t2,tve2) = teval' env e2 tve1+    in case either Left (unify t2 TInt) . unify t1 TInt $ tve2 of+       Right tve -> (TInt,tve)+       Left err  -> error $ "Trying to add non-integers: " ++ err+teval' env (IFZ e1 e2 e3) = \tve0 ->+    let (t1,tve1) = teval' env e1 tve0+        (t2,tve2) = teval' env e2 tve1+        (t3,tve3) = teval' env e3 tve2+    in case unify t1 TInt tve3 of+       Right tve -> case unify t2 t3 tve of+        Right tve -> (t2,tve)    +        Left err  -> error $ unwords ["Branches of IFZ have",+                                      "different types.",+                                      "Unification failed:", err]+       Left err -> error $ "Trying to compare a non-integer to 0: " ++ err++teval' env (Fix e) = \tve0 ->+    let (t,tve1)  = teval' env e tve0+        (ta,tve2) = newtv tve1+        (tb,tve3) = newtv tve2+    in case unify t ((ta :> tb) :> (ta :> tb)) tve3 of+       Right tve -> (ta :> tb,tve)+       Left err  -> error $ "Inappropriate type in Fix: "++err++-- | Resolve all type variables, as far as possible+teval :: TEnv -> Term -> Typ+teval tenv e = let (t,tve) = teval' tenv e tve0 in tvsub tve t++-- Tests+(vx,vy) = (V "x",V "y")++test0 = teval' env0 ((L "x" (vx :+ (I 2))) `A` (I 1)) tve0+-- (TV 1,TVE 2 (fromList [(0,TInt),(1,TInt)]))++term1 = L "x" (IFZ vx (I 1) (vx :+ (I 2)))+test10 = teval' env0 term1 tve0+-- (TV 0 :> TInt,TVE 1 (fromList [(0,TInt)]))++-- need a better presentation of the final result: cf. teval' and teval++test1 = teval env0 term1 -- TInt :> TInt++termid = L "x" vx+testid = teval env0 termid -- TV 0 :> TV 0++term2a = L "x" (L "y" (vx `A` vy))+test2a = teval env0 term2a+-- (TV 1 :> TV 2) :> (TV 1 :> TV 2)++-- Used to be hidden problem. The main benefit of types: static approximation+-- of program behavior+term3 = L "x" (IFZ vx (I 1) vy)+test3 = teval env0 term3++term4 = L "x" (IFZ vx (I 1) (vx `A` (I 1)))+test4 = teval env0 term4+-- compare the error message with that of test4a and test4b in TEvalNC.hs++term6  = (L "x" (I 1)) `A` vy+test61 = teval env0 term6+test62 = teval env0 $ (I 1) :+ vx+++tmul1 = L "x" (L "y"+          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy)))++testm1 = teval env0 tmul1 -- is typechecking really decidable?++-- Can termY be typechecked?+delta = L "y" (vy `A` vy)+testd = teval env0 delta ++tmul = Fix (L "self" (L "x" (L "y"+          (IFZ vx (I 0)+            (((V "self") `A` (vx :+ (I (-1))) `A` vy) :+ vy)))))++testm21' = teval' env0 tmul tve0+-- (TV 5 :> TV 6,TVE 7 (fromList +--     [(0,TInt :> TV 3),(1,TInt),(2,TInt),(3,TV 2 :> TV 4),+--      (4,TInt),(5,TInt),(6,TV 2 :> TV 4)]))++testm21 = teval env0 tmul                       -- TInt :> (TInt :> TInt)+testm22 = teval env0 (tmul `A` (I 2))           -- TInt :> TInt+testm23 = teval env0 (tmul `A` (I 2) `A` (I 3)) -- TInt+testm24 = teval env0 (tmul `A` (I (-1)) `A` (I (-1))) -- TInt++-- using the metalanguage definition of termid: `top-level let'+term2id = L "f" (L "y" +               ((I 2) :++                ((termid `A` (V "f")) `A` ((termid `A` vy) :+ (I 1)))))+test2id = teval env0 term2id -- (TInt :> TInt) :> (TInt :> TInt)++-- using the metalanguage let+termlet = let c2  = L "f" (L "x" (V "f" `A` (V "f" `A` vx)))+              inc = L "x" (vx :+ (I 1))+              compose = L "f" (L "g" (L "x" (V "f" `A` (V "g" `A` vx))))+          in c2 `A` (compose `A` inc `A` inc) `A` (I 10) :++             (c2 `A` (compose `A` inc) `A` termid `A` (I 100))+testlet = teval env0 termlet+

@@ -0,0 +1,289 @@+{-# LANGUAGE PatternGuards #-}+-- | Simply-typed Curry-style (nominal) lambda-calculus+-- with integers and zero-comparison+-- Type inference, of the type and of the environment, aka+-- conditional typechecking+-- This code does not in general infer polymorphic bindings as this is akin +-- to higher-order unification.+--+-- The benefit of the approach: we can handle _open_ terms.+-- Some of them we type check, and some of them we reject. The rejection means+-- the term cannot be typed in _any_ type environment.+--+-- One often hears a complaint against typing: one can evaluate+-- terms we can't even type check. This code shows that we can type check+-- terms we can't even evaluate.+-- +-- We cannot evaluate open terms at all, but we can type check them, +-- inferring both the type as well as the _requirement_+-- on the environments in which the term must be used.+--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.TInfTEnv where++import qualified Data.IntMap as M++data Typ = TInt | !Typ :> !Typ | TV TVarName deriving (Show, Eq)+infixr 9 :>+type TVarName = Int++data Term = V VarName+          | L VarName Term+          | A Term Term+          | I Int+          | Term :+ Term                -- addition+          | IFZ Term Term Term          -- if zero+          | Fix Term                    -- fix f, where f :: (a->b)->(a->b)+            deriving (Show, Eq)++infixl 9 `A`+type VarName = String++-- | Type Environment: associating types with `free' term variables+type TEnv = [(VarName, Typ)]++env0 :: TEnv+env0 = []++lkup :: TEnv -> VarName -> Typ+lkup env x = maybe err id $ lookup x env + where err = error $ "Unbound variable " ++ x++ext :: TEnv -> (VarName,Typ) -> TEnv+ext env xt = xt : env++unext :: TEnv -> VarName -> TEnv+unext env v = case break (\(x,_) -> x == v) env of+                   (h,(_:t)) -> h ++ t+                   _         -> error $ "No variable " ++ v++env_map :: (Typ->Typ) -> TEnv -> TEnv+env_map f = map (\(x,t) -> (x,f t))++-- | Merge two environment, using the given function to resolve the conflicts,+-- if any+env_fold_merge :: TEnv -> TEnv -> +                  (Typ -> Typ -> seed -> Either err seed) ->+                  seed -> Either err (TEnv,seed)+env_fold_merge env1 env2 f seed = foldr folder (Right (env1,seed)) env2+ where+ folder _ s@(Left _) = s+ folder (x,t2) (Right (env1,seed)) | Just t1 <- lookup x env1 =+    case f t1 t2 seed of+      Right seed -> Right (env1,seed)+      Left  err  -> Left err+ folder xt2 (Right (env1,seed)) = Right (ext env1 xt2,seed)++-- | Type Variable Environment: associating types with `free' type variables+data TVE = TVE Int (M.IntMap Typ) deriving Show++-- | Allocate a fresh type variable (see the first component of TVE)+newtv :: TVE -> (Typ,TVE)+newtv (TVE n s) = (TV n,TVE (succ n) s)++tve0 :: TVE+tve0 = TVE 0 M.empty++tvlkup :: TVE -> TVarName -> Maybe Typ+tvlkup (TVE _ s) v = M.lookup v s++tvext :: TVE -> (TVarName,Typ) -> TVE+tvext (TVE c s) (tv,t) = TVE c $ M.insert tv t s++-- | Type variables are logic variables: hypothetical reasoning+tvsub :: TVE -> Typ -> Typ+tvsub tve (t1 :> t2) = tvsub tve t1 :> tvsub tve t2+tvsub tve (TV v) | Just t <- tvlkup tve v = tvsub tve t+tvsub tve t = t++-- | `shallow' substitution; check if tv is bound to anything `substantial'+tvchase :: TVE -> Typ -> Typ+tvchase tve (TV v) | Just t <- tvlkup tve v = tvchase tve t+tvchase _ t = t++-- | The unification. If unification failed, return the reason+unify :: Typ -> Typ -> TVE -> Either String TVE+unify t1 t2 tve = unify' (tvchase tve t1) (tvchase tve t2) tve++-- | If either t1 or t2 are type variables, they are definitely unbound+unify' :: Typ -> Typ -> TVE -> Either String TVE+unify' TInt TInt = Right+unify' (t1a :> t1r) (t2a :> t2r) = either Left (unify t1r t2r) . unify t1a t2a+unify' (TV v1) t2 = unifyv v1 t2+unify' t1 (TV v2) = unifyv v2 t1+unify' t1 t2 = const (Left $ unwords ["constant mismatch:",show t1,"and",+                                      show t2])++-- | Unify a free variable v1 with t2+unifyv :: TVarName -> Typ -> TVE -> Either String TVE+unifyv v1 (TV v2) tve =+    if v1 == v2 then Right tve+       else Right (tvext tve (v1,TV v2)) -- record new constraint+unifyv v1 t2 tve = if occurs v1 t2 tve+                      then Left $ unwords ["occurs check:",show (TV v1),+                                           "in",show $ tvsub tve t2]+                      else Right (tvext tve (v1,t2))++-- | The occurs check: if v appears free in t+occurs :: TVarName -> Typ -> TVE -> Bool+occurs v TInt _ = False+occurs v (t1 :> t2) tve = occurs v t1 tve || occurs v t2 tve+occurs v (TV v2) tve =+    case tvlkup tve v2 of+         Nothing -> v == v2+         Just t  -> occurs v t tve++merge_env :: TEnv -> TEnv -> (TVE -> (TEnv,TVE))+merge_env env1 env2 tve = + either error id $ env_fold_merge env1 env2 unify tve++-- | Type reconstruction: abstract evaluation+teval' :: Term -> (TVE -> (Typ,TEnv,TVE))+teval' (V x)   = \tve0 -> +    let (tv,tve1) = newtv tve0+        env1      = ext env0 (x,tv)+    in (tv,env1,tve1)+teval' (L x e) = \tve0 ->+    let (tv,tve1) = newtv tve0+        env1      = ext env0 (x,tv)+        (te,env2,tve2) = teval' e tve1+        (env3,tve3)    = merge_env env2 env1 tve2+        env4           = unext env3 x+    in (tv :> te,env4,tve3)+teval' (A e1 e2) = \tve0 ->+    let (t1,env1,tve1) = teval' e1 tve0+        (t2,env2,tve2) = teval' e2 tve1+        (env3,tve3)    = merge_env env1 env2 tve2+        (t1r,tve4)     = newtv tve3+    in case unify t1 (t2 :> t1r) tve4 of+       Right tve -> (t1r,env3,tve)+       Left err  -> error $ err++teval' (I n) = \tve0 -> (TInt,env0,tve0)+teval' (e1 :+ e2) = \tve0 ->+    let (t1,env1,tve1) = teval' e1 tve0+        (t2,env2,tve2) = teval' e2 tve1+        (env3,tve3)    = merge_env env1 env2 tve2+    in case either Left (unify t2 TInt) . unify t1 TInt $ tve3 of+       Right tve -> (TInt,env3,tve)+       Left err  -> error $ "Trying to add non-integers: " ++ err+teval' (IFZ e1 e2 e3) = \tve0 ->+    let (t1,env1,tve1) = teval' e1 tve0+        (t2,env2,tve2) = teval' e2 tve1+        (t3,env3,tve3) = teval' e3 tve2+        (env4,tve4)    = merge_env env1 env2 tve3+        (env5,tve5)    = merge_env env4 env3 tve4+    in case unify t1 TInt tve5 of+       Right tve -> +           case unify t2 t3 tve of+                Right tve -> (t2,env5,tve)       +                Left err  -> error $ unwords ["Branches of IFZ have different",+                                              "types. Unification failed:",err]+       Left err -> error $ "Trying to compare a non-integer to 0: " ++ err++teval' (Fix e) = \tve0 ->+    let (t,env,tve1)  = teval' e tve0+        (ta,tve2) = newtv tve1+        (tb,tve3) = newtv tve2+    in case unify t ((ta :> tb) :> (ta :> tb)) tve3 of+       Right tve -> (ta :> tb,env,tve)+       Left err  -> error $ "Inappropriate type in Fix: "++err++-- | Resolve all type variables, as far as possible+teval :: Term -> (Typ,TEnv)+teval e = let (t,env,tve) = teval' e tve0 +          in (tvsub tve t, env_map (tvsub tve) env)++-- Tests+(vx,vy) = (V "x",V "y")++test0 = teval' ((L "x" (vx :+ (I 2))) `A` (I 1)) tve0+-- (TV 2,[],TVE 3 (fromList [(0,TInt),(1,TInt),(2,TInt)]))++term1 = L "x" (IFZ vx (I 1) (vx :+ (I 2)))+test10 = teval' term1 tve0+-- (TV 0 :> TInt,[],TVE 3 (fromList [(0,TInt),(1,TInt),(2,TInt)]))++-- need a better presentation of the final result: cf. teval' and teval++test1 = teval term1 -- TInt :> TInt++termid = L "x" vx+testid = teval termid -- (TV 0 :> TV 0,[])++term2a = L "x" (L "y" (vx `A` vy))+test2a = teval term2a+-- ((TV 1 :> TV 4) :> (TV 1 :> TV 4),[])+++-- Used to be hidden problem. The main benefit of types: static approximation+-- of program behavior+-- The terms with unbound variables no longer fail the type check.+-- We infer both the type and the environment+term3 = L "x" (IFZ vx (I 1) vy)+test3 = teval term3+-- (TInt :> TInt,[("y",TInt)]) ++-- That term is ill-typed in any environment...+term4 = L "x" (IFZ vx (I 1) (vx `A` (I 1)))+test4 = teval term4+-- compare the error message with that of test4a and test4b in TEvalNC.hs++term6  = (L "x" (I 1)) `A` vy+test61 = teval term6+-- (TInt,[("y",TV 1)])+test62 = teval $ (I 1) :+ vx+-- (TInt,[("x",TInt)])++-- But some terms still fail type-checking: no environment could+-- be found to make the term typeable+test63 = teval $ IFZ (vx `A` (I 1)) vx (I 2)+-- *** Exception: Branches of IFZ have different types. +-- Unification failed: constant mismatch: TInt :> TV 1 and TInt++-- Here two branches of the conditional make inconsistent assumptions+-- about the environment+test64 = teval $ IFZ (I 1) (vx `A` (I 1)) (vx :+ (I 2))+-- *** Exception: constant mismatch: TInt :> TV 1 and TInt+++tmul1 = L "x" (L "y"+          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy)))++testm1 = teval tmul1 -- is typechecking really decidable?++-- Can termY be typechecked?+delta = L "y" (vy `A` vy)+testd = teval delta ++tmul = Fix (L "self" (L "x" (L "y"+          (IFZ vx (I 0)+            (((V "self") `A` (vx :+ (I (-1))) `A` vy) :+ vy)))))++testm21' = teval' tmul tve0+-- (TV 5 :> TV 6,TVE 7 (fromList +--     [(0,TInt :> TV 3),(1,TInt),(2,TInt),(3,TV 2 :> TV 4),+--      (4,TInt),(5,TInt),(6,TV 2 :> TV 4)]))++testm21 = teval tmul                       -- TInt :> (TInt :> TInt)+testm22 = teval (tmul `A` (I 2))           -- TInt :> TInt+testm23 = teval (tmul `A` (I 2) `A` (I 3)) -- TInt+testm24 = teval (tmul `A` (I (-1)) `A` (I (-1))) -- TInt++-- using the metalanguage definition of termid: `top-level let'+term2id = L "f" (L "y" +               ((I 2) :++                ((termid `A` (V "f")) `A` ((termid `A` vy) :+ (I 1)))))+test2id = teval term2id -- (TInt :> TInt) :> (TInt :> TInt)++-- using the metalanguage let+termlet = let c2  = L "f" (L "x" (V "f" `A` (V "f" `A` vx)))+              inc = L "x" (vx :+ (I 1))+              compose = L "f" (L "g" (L "x" (V "f" `A` (V "g" `A` vx))))+          in c2 `A` (compose `A` inc `A` inc) `A` (I 10) :++             ((c2 `A` (compose `A` inc) `A` termid) `A` (I 100))+testlet = teval termlet -- (TInt,[])+

@@ -0,0 +1,301 @@+-- | Simply-typed Curry-style (nominal) lambda-calculus+-- with integers and zero-comparison+-- Type inference. Hiding the single-threaded state via simple+-- algebraic transformations (beta-expansions). +--+-- <http://okmij.org/ftp/Computation/Computation.html#teval>+--++module Language.TEval.TInfTM where++import qualified Data.IntMap as M+import Prelude hiding ((>>=), return)++data Typ = TInt | !Typ :> !Typ | TV TVarName deriving (Show, Eq)+infixr 9 :>+type TVarName = Int++data Term = V VarName+          | L VarName Term+          | A Term Term+          | I Int+          | Term :+ Term                -- addition+          | IFZ Term Term Term          -- if zero+          | Fix Term                    -- fix f, where f :: (a->b)->(a->b)+            deriving (Show, Eq)++infixl 9 `A`+type VarName = String++-- | Type Environment: associating types with `free' term variables+type TEnv = [(VarName, Typ)]++env0 :: TEnv+env0 = []++lkup :: TEnv -> VarName -> Typ+lkup env x = maybe err id $ lookup x env + where err = error $ "Unbound variable " ++ x++ext :: TEnv -> (VarName,Typ) -> TEnv+ext env xt = xt : env++-- | Type Variable Environment: associating types with `free' type variables+data TVE = TVE Int (M.IntMap Typ) deriving Show++-- | Allocate a fresh type variable (see the first component of TVE)+newtv :: TVE -> (Typ,TVE)+newtv (TVE n s) = (TV n,TVE (succ n) s)++tve0 :: TVE+tve0 = TVE 0 M.empty++tvlkup :: TVE -> TVarName -> Maybe Typ+tvlkup (TVE _ s) v = M.lookup v s++tvext :: TVE -> (TVarName,Typ) -> TVE+tvext (TVE c s) (tv,t) = TVE c $ M.insert tv t s++-- | Type variables are logic variables: hypothetical reasoning+tvsub :: TVE -> Typ -> Typ+tvsub tve (t1 :> t2) = tvsub tve t1 :> tvsub tve t2+tvsub tve (TV v) | Just t <- tvlkup tve v = tvsub tve t+tvsub tve t = t++-- | `shallow' substitution; check if tv is bound to anything `substantial'+tvchase :: TVE -> Typ -> Typ+tvchase tve (TV v) | Just t <- tvlkup tve v = tvchase tve t+tvchase _ t = t++-- | The unification. If unification failed, return the reason+unify :: Typ -> Typ -> TVE -> Either String TVE+unify t1 t2 tve = unify' (tvchase tve t1) (tvchase tve t2) tve++-- | If either t1 or t2 are type variables, they are definitely unbound+unify' :: Typ -> Typ -> TVE -> Either String TVE+unify' TInt TInt = Right+unify' (t1a :> t1r) (t2a :> t2r) = either Left (unify t1r t2r) . unify t1a t2a+unify' (TV v1) t2 = unifyv v1 t2+unify' t1 (TV v2) = unifyv v2 t1+unify' t1 t2 = const (Left $ unwords ["constant mismatch:",show t1,"and",+                                      show t2])++-- | Unify a free variable v1 with t2+unifyv :: TVarName -> Typ -> TVE -> Either String TVE+unifyv v1 (TV v2) tve =+    if v1 == v2 then Right tve+       else Right (tvext tve (v1,TV v2)) -- record new constraint+unifyv v1 t2 tve = if occurs v1 t2 tve+                      then Left $ unwords ["occurs check:",show (TV v1),+                                           "in",show $ tvsub tve t2]+                      else Right (tvext tve (v1,t2))++-- | The occurs check: if v appears free in t+occurs :: TVarName -> Typ -> TVE -> Bool+occurs v TInt _ = False+occurs v (t1 :> t2) tve = occurs v t1 tve || occurs v t2 tve+occurs v (TV v2) tve =+    case tvlkup tve v2 of+         Nothing -> v == v2+         Just t  -> occurs v t tve++-- | Introducing the combinators to hide single-threaded state tve in one+-- case of teval' (the A case). The other cases stay as they are, to illustrate+-- that our transformation is fully compatible with the earlier code.+--+type TVEM a = TVE -> (a,TVE)            -- a convenient abbreviation++(>>=) :: TVEM a -> (a -> TVEM b) -> TVEM b+m >>= f = \tve0 -> let (t1,tve1) = m tve0 in f t1 tve1++return :: a -> TVEM a+return v = \tve3 -> (v,tve3)+++-- | The expression abstracted from the last-but-one re-writing of the A-clause+-- below+unifyM t1 t2 = \tve3 -> +      case unify t1 t2 tve3 of+       Right tve -> ((),tve)+       Left err  -> error $ err+++-- | Type reconstruction: abstract evaluation+teval' :: TEnv -> Term -> (TVE -> (Typ,TVE))+teval' env (V x)   = \tve0 -> (lkup env x,tve0)+teval' env (L x e) = \tve0 ->+    let (tv,tve1) = newtv tve0+        (te,tve2) = teval' (ext env (x,tv)) e tve1+    in (tv :> te,tve2)+++{-  Original code, from TInfT.hs+teval' env (A e1 e2) = \tve0 ->+    let (t1,tve1) = teval' env e1 tve0+        (t2,tve2) = teval' env e2 tve1+        (t1r,tve3)= newtv tve2+    in case unify t1 (t2 :> t1r) tve3 of+       Right tve -> (t1r,tve)+       Left err  -> error $ err+-}++{- After two beta-expansions in the first let and the introduction of the+   combinator (>>=)+teval' env (A e1 e2) = +    (teval' env e1) >>= (\t1 tve1 ->+    let (t2,tve2) = teval' env e2 tve1+        (t1r,tve3)= newtv tve2+    in case unify t1 (t2 :> t1r) tve3 of+       Right tve -> (t1r,tve)+       Left err  -> error $ err)+-}++{- After the elimination of all let forms in the similar fashion+teval' env (A e1 e2) = +    teval' env e1 >>= (\t1 ->+    teval' env e2 >>= (\t2 ->+    newtv         >>= (\t1r tve3 ->+    case unify t1 (t2 :> t1r) tve3 of+       Right tve -> (t1r,tve)+       Left err  -> error $ err)))+-}++{- After beta-expansion in one of the union clauses+teval' env (A e1 e2) = +    teval' env e1 >>= (\t1 ->+    teval' env e2 >>= (\t2 ->+    newtv         >>= (\t1r tve3 ->+    case unify t1 (t2 :> t1r) tve3 of+       Right tve -> ((\tve -> ((),tve)) >>= (\_ tve -> (t1r,tve))) tve+       Left err  -> error $ err)))+-}++{- After factoring out t1r from the result of unify, based on+   beta and eta expansions and the distribution over the `case'+teval' env (A e1 e2) = +    teval' env e1 >>= (\t1 ->+    teval' env e2 >>= (\t2 ->+    newtv         >>= (\t1r tve3 -> +    ((\tve3 -> +      (case unify t1 (t2 :> t1r) tve3 of+       Right tve -> ((),tve)+       Left err  -> error $ err)) >>= (\_ tve ->+       (t1r,tve))) tve3)))+-}++-- | After we finished re-writing, there are no longer any tve left...+-- The other clauses stay the same, to illustrate our re-wriring is local+-- and meaning preserving. If we carry the re-writing for other clauses,+-- we get the code in TInfLetI.hs (beautified with the do-notation).+teval' env (A e1 e2) = +    teval' env e1 >>= (\t1 ->+    teval' env e2 >>= (\t2 ->+    newtv         >>= (\t1r-> +    unifyM t1 (t2 :> t1r) >>= (\_ ->+       return t1r))))+++teval' env (I n) = \tve0 -> (TInt,tve0)+teval' env (e1 :+ e2) = \tve0 ->+    let (t1,tve1) = teval' env e1 tve0+        (t2,tve2) = teval' env e2 tve1+    in case either Left (unify t2 TInt) . unify t1 TInt $ tve2 of+       Right tve -> (TInt,tve)+       Left err  -> error $ "Trying to add non-integers: " ++ err+teval' env (IFZ e1 e2 e3) = \tve0 ->+    let (t1,tve1) = teval' env e1 tve0+        (t2,tve2) = teval' env e2 tve1+        (t3,tve3) = teval' env e3 tve2+    in case unify t1 TInt tve3 of+       Right tve -> case unify t2 t3 tve of+        Right tve -> (t2,tve)    +        Left err  -> error $ unwords ["Branches of IFZ have",+                                      "different types.",+                                      "Unification failed:", err]+       Left err -> error $ "Trying to compare a non-integer to 0: " ++ err++teval' env (Fix e) = \tve0 ->+    let (t,tve1)  = teval' env e tve0+        (ta,tve2) = newtv tve1+        (tb,tve3) = newtv tve2+    in case unify t ((ta :> tb) :> (ta :> tb)) tve3 of+       Right tve -> (ta :> tb,tve)+       Left err  -> error $ "Inappropriate type in Fix: "++err++-- Resolve all type variables, as far as possible+teval :: TEnv -> Term -> Typ+teval tenv e = let (t,tve) = teval' tenv e tve0 in tvsub tve t++-- Tests+(vx,vy) = (V "x",V "y")++test0 = teval' env0 ((L "x" (vx :+ (I 2))) `A` (I 1)) tve0+-- (TV 1,TVE 2 (fromList [(0,TInt),(1,TInt)]))++term1 = L "x" (IFZ vx (I 1) (vx :+ (I 2)))+test10 = teval' env0 term1 tve0+-- (TV 0 :> TInt,TVE 1 (fromList [(0,TInt)]))++-- need a better presentation of the final result: cf. teval' and teval++test1 = teval env0 term1 -- TInt :> TInt++termid = L "x" vx+testid = teval env0 termid -- TV 0 :> TV 0++term2a = L "x" (L "y" (vx `A` vy))+test2a = teval env0 term2a+-- (TV 1 :> TV 2) :> (TV 1 :> TV 2)++-- Used to be hidden problem. The main benefit of types: static approximation+-- of program behavior+term3 = L "x" (IFZ vx (I 1) vy)+test3 = teval env0 term3++term4 = L "x" (IFZ vx (I 1) (vx `A` (I 1)))+test4 = teval env0 term4+-- compare the error message with that of test4a and test4b in TEvalNC.hs++term6  = (L "x" (I 1)) `A` vy+test61 = teval env0 term6+test62 = teval env0 $ (I 1) :+ vx+++tmul1 = L "x" (L "y"+          (IFZ vx (I 0)+            ((tmul1 `A` (vx :+ (I (-1))) `A` vy) :+ vy)))++testm1 = teval env0 tmul1 -- is typechecking really decidable?++-- Can termY be typechecked?+delta = L "y" (vy `A` vy)+testd = teval env0 delta ++tmul = Fix (L "self" (L "x" (L "y"+          (IFZ vx (I 0)+            (((V "self") `A` (vx :+ (I (-1))) `A` vy) :+ vy)))))++testm21' = teval' env0 tmul tve0+-- (TV 5 :> TV 6,TVE 7 (fromList +--     [(0,TInt :> TV 3),(1,TInt),(2,TInt),(3,TV 2 :> TV 4),+--      (4,TInt),(5,TInt),(6,TV 2 :> TV 4)]))++testm21 = teval env0 tmul                       -- TInt :> (TInt :> TInt)+testm22 = teval env0 (tmul `A` (I 2))           -- TInt :> TInt+testm23 = teval env0 (tmul `A` (I 2) `A` (I 3)) -- TInt+testm24 = teval env0 (tmul `A` (I (-1)) `A` (I (-1))) -- TInt++-- using the metalanguage definition of termid: `top-level let'+term2id = L "f" (L "y" +               ((I 2) :++                ((termid `A` (V "f")) `A` ((termid `A` vy) :+ (I 1)))))+test2id = teval env0 term2id -- (TInt :> TInt) :> (TInt :> TInt)++-- using the metalanguage let+termlet = let c2  = L "f" (L "x" (V "f" `A` (V "f" `A` vx)))+              inc = L "x" (vx :+ (I 1))+              compose = L "f" (L "g" (L "x" (V "f" `A` (V "g" `A` vx))))+          in c2 `A` (compose `A` inc `A` inc) `A` (I 10) :++             (c2 `A` (compose `A` inc) `A` termid `A` (I 100))+testlet = teval env0 termlet+

@@ -1,20 +1,20 @@ name:           liboleg-version:        0.1.0.3+version:        0.1.1 license:        BSD3 license-file:   LICENSE author:         Oleg Kiselyov maintainer:     Don Stewart <dons@galois.com> homepage:       http://okmij.org/ftp/ category:       Text-synopsis:       A collection of Oleg Kiselyov's Haskell modules-description:    A collection of Oleg Kiselyov's Haskell modules (released with his permission)+synopsis:       A collection of Oleg Kiselyov's Haskell modules (2009-2008)+description:    A collection of Oleg Kiselyov's Haskell modules (2009-2008) (released with his permission) build-type:     Simple stability:      experimental cabal-version:  >= 1.2  library     build-depends:-            base,+            base < 4,             containers,             mtl,             unix@@ -28,6 +28,17 @@              Language.TypeLC             Language.TypeFN++            Language.TEval.EvalN+            Language.TEval.EvalTaglessF+            Language.TEval.EvalTaglessI+            Language.TEval.TEvalNC+            Language.TEval.TEvalNR+            Language.TEval.TInfLetI+            Language.TEval.TInfLetP+            Language.TEval.TInfT+            Language.TEval.TInfTEnv+            Language.TEval.TInfTM              Text.PrintScan             Text.PrintScanF