Fix evaluation with environment by introducing Value

3 files changed, 31 insertions, 23 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index 0829186..a15d3f9 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -1,6 +1,7 @@
 module Minilang.Lambda.Eval where
 
-import Data.Text (Text)
+import Data.Text (Text, unpack)
+import Debug.Trace (trace)
 
 data Term
   = Var Text
@@ -8,29 +9,36 @@ data Term
   | App Term Term
   deriving (Show, Read, Eq)
 
-type Env = [(Text, Term)]
+type Env = [(Text, Value)]
+
+data Value
+  = V Text
+  | Abs Text Term Env
+  | Ap Value Value
+  deriving (Show, Read, Eq)
 
 -- call-by-value evaluator
-eval :: Term -> Env -> Term
+eval :: Term -> Env -> Value
 eval (Var x) env = case lookup x env of
   Just v -> v -- we do not need to eval v again
-  Nothing -> Var x
-eval (Lam x body) _env = Lam x body
+  Nothing -> V x -- x is not bound in env
+eval (Lam x body) env = Abs x body env
 eval (App f a) env =
   -- we need to force evaluation of the argument
   -- because haskell's default semantics is non-strict
   -- so if a' is never used, it will not be evaluated!
   let a' = eval a env
    in seq a' $ case eval f env of
-        Lam x body -> eval body ((x, a') : env)
-        f' -> App f' a'
+        Abs x body env' -> eval body ((x, a') : env')
+        f' -> Ap f' a'
 
-evalNeed :: Term -> Env -> Term
+evalNeed :: Term -> Env -> Value
 evalNeed (Var x) env = case lookup x env of
-  Just v -> evalNeed v env -- we need to eval v because it might be a redex
-  Nothing -> Var x
-evalNeed (Lam x body) _env = Lam x body
+  Just v -> v
+  Nothing -> V x
+evalNeed (Lam x body) env = Abs x body env
 evalNeed (App f a) env =
-  case evalNeed f env of
-    Lam x body -> evalNeed body ((x, a) : env)
-    f' -> App f' a
+  let a' = eval a env
+   in case evalNeed f env of
+        Abs x body env' -> evalNeed body ((x, a') : env')
+        f' -> Ap f' a'
diff --git a/lambda-calcul/haskell/test/Minilang/IOSpec.hs b/lambda-calcul/haskell/test/Minilang/IOSpec.hs
index 14d279d..80cda6c 100644
--- a/lambda-calcul/haskell/test/Minilang/IOSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/IOSpec.hs
@@ -27,7 +27,7 @@ spec = parallel $
 
         out <- readFile outputFileName
 
-        out `shouldBe` "Var \"z\"\n"
+        out `shouldBe` "V \"z\"\n"
 
 withTempFile :: (String -> IO ()) -> IO ()
 withTempFile =
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index 11cf394..718b46d 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -2,7 +2,7 @@ module Minilang.Lambda.EvalSpec (spec) where
 
 import Control.Concurrent (threadDelay)
 import Control.Concurrent.Async (race_)
-import Minilang.Lambda.Eval (Term (..), eval, evalNeed)
+import Minilang.Lambda.Eval (Term (..), Value (..), eval, evalNeed)
 import Test.Hspec (Spec, describe, it, shouldBe)
 
 spec :: Spec
@@ -21,31 +21,31 @@ spec = do
   describe "call-by-value eval" $ do
     it "evaluates 'x' as itself" $ do
       let term = Var "x"
-      eval term [] `shouldBe` Var "x"
+      eval term [] `shouldBe` V "x"
     it "evaluates '((λ x. x) y)' as 'y'" $ do
       let term = App (Lam "x" (Var "x")) (Var "y")
-      eval term [] `shouldBe` Var "y"
+      eval term [] `shouldBe` V "y"
     it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do
       let snd' = Lam "x" (Lam "y" (Var "y"))
       let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y")
-      eval term [] `shouldBe` App (Var "t") (Var "y")
+      eval term [] `shouldBe` Ap (V "t") (V "y")
     it "evaluates '((λ x y. x) z t)' as 'z'" $ do
       let term = App (App fst' (Var "z")) (Var "t")
-      eval term [] `shouldBe` Var "z"
+      eval term [] `shouldBe` V "z"
     it "diverges on evaluating argument bound to ω" $
       shouldDiverge $
         eval term []
 
   describe "call-by-need eval" $ do
     it "evaluates 'x' as itself" $ do
-      evalNeed (Var "x") [] `shouldBe` Var "x"
+      evalNeed (Var "x") [] `shouldBe` V "x"
     it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
-      evalNeed term [] `shouldBe` Var "z"
+      evalNeed term [] `shouldBe` V "z"
     it "diverges on evaluating ω" $
       shouldDiverge $
         evalNeed omega []
 
-shouldDiverge :: Term -> IO ()
+shouldDiverge :: Value -> IO ()
 shouldDiverge t =
   race_
     (t `seq` fail "Did not diverge")