diff --git a/Language/TEval/EvalN.hs b/Language/TEval/EvalN.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/EvalN.hs @@ -0,0 +1,150 @@ +-- | +-- Untyped (nominal) lambda-calculus with integers and the conditional +-- +-- +-- +-- +-- [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 _) = "" + +-- | 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] diff --git a/Language/TEval/EvalTaglessF.hs b/Language/TEval/EvalTaglessF.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/EvalTaglessF.hs @@ -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. +-- +-- +-- + +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 diff --git a/Language/TEval/EvalTaglessI.hs b/Language/TEval/EvalTaglessI.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/EvalTaglessI.hs @@ -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 +-- +-- +-- + +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) = "" + -- 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 -- +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)) -- +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 diff --git a/Language/TEval/TEvalNC.hs b/Language/TEval/TEvalNC.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/TEvalNC.hs @@ -0,0 +1,123 @@ +-- | Simply-typed Church-style (nominal) lambda-calculus +-- with integers and zero-comparison +-- Type checking +-- +-- +-- + +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 + diff --git a/Language/TEval/TEvalNR.hs b/Language/TEval/TEvalNR.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/TEvalNR.hs @@ -0,0 +1,135 @@ +-- | Simply-typed Church-style (nominal) lambda-calculus +-- with integers and zero-comparison +-- Type reconstruction, for all subterms +-- +-- +-- + +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 diff --git a/Language/TEval/TInfLetI.hs b/Language/TEval/TInfLetI.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/TInfLetI.hs @@ -0,0 +1,322 @@ +{-# LANGUAGE PatternGuards #-} +-- | Simply-typed Curry-style (nominal) lambda-calculus +-- with integers and zero-comparison +-- Let-polymorphism via inlining +-- Type inference +-- +-- +-- + +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 + diff --git a/Language/TEval/TInfLetP.hs b/Language/TEval/TInfLetP.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/TInfLetP.hs @@ -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 +-- +-- +-- + +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 + diff --git a/Language/TEval/TInfT.hs b/Language/TEval/TInfT.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/TInfT.hs @@ -0,0 +1,219 @@ +-- | Simply-typed Curry-style (nominal) lambda-calculus +-- with integers and zero-comparison +-- Type inference +-- +-- +-- + +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 + diff --git a/Language/TEval/TInfTEnv.hs b/Language/TEval/TInfTEnv.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/TInfTEnv.hs @@ -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. +-- +-- +-- + +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,[]) + diff --git a/Language/TEval/TInfTM.hs b/Language/TEval/TInfTM.hs new file mode 100644 --- /dev/null +++ b/Language/TEval/TInfTM.hs @@ -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). +-- +-- +-- + +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 + diff --git a/liboleg.cabal b/liboleg.cabal --- a/liboleg.cabal +++ b/liboleg.cabal @@ -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 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