fix call-by-value evaluator base on NBE

2 files changed, 83 insertions, 48 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index 9d56c49..e5530eb 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -4,7 +4,8 @@
 module Minilang.Lambda.Eval where
 
 import Data.Aeson (FromJSON, ToJSON)
-import Data.Text (Text)
+import Data.String (IsString (..))
+import Data.Text (Text, pack)
 import GHC.Generics (Generic)
 
 data Term
@@ -13,6 +14,9 @@ data Term
   | App Term Term
   deriving (Show, Read, Eq, Generic, ToJSON, FromJSON)
 
+instance IsString Term where
+  fromString = Var . pack
+
 data Value = Clos EnvValue Text Term | VNeut Neutral
   deriving (Show, Read, Eq)
 
@@ -26,15 +30,21 @@ type EnvValue = [(Text, Value)]
 newEnv :: Env
 newEnv = []
 
+normalise :: Term -> Term
+normalise term = readBack (eval [] term)
+
 -- call-by-value evaluator
 -- from https://davidchristiansen.dk/tutorials/nbe/#%28part._untyped-eval%29
 eval :: EnvValue -> Term -> Value
 eval env = \case
   Var x -> case lookup x env of
     Just term -> term
-    Nothing -> error $ "Unbound variable: " ++ show x
+    Nothing -> VNeut (NVar x)
   Lam x body -> Clos env x body
-  App f a -> apply (eval env f) (eval env a)
+  App f a ->
+    let f' = eval env f
+        a' = eval env a
+     in f' `seq` a' `seq` apply f' a'
 
 apply :: Value -> Value -> Value
 apply f a =
@@ -56,9 +66,6 @@ readBack = go []
       VNeut (NVar n) -> Var n
       VNeut (NApp f a) -> App (go names (VNeut f)) (go names a)
 
-normalise :: Term -> Term
-normalise term = readBack (eval [] term)
-
 freshName :: Text -> [Text] -> Text
 freshName x names
   | x `elem` names = freshName (x <> "'") names
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index 3dbe3cd..d772fe0 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -2,52 +2,80 @@ module Minilang.Lambda.EvalSpec (spec) where
 
 import Control.Concurrent (threadDelay)
 import Control.Concurrent.Async (race_)
-import Minilang.Lambda.Eval (Term (..), eval)
+import Minilang.Lambda.Eval (Term (..), Value, eval, normalise)
 import Test.Hspec (Spec, describe, it, pending, shouldBe)
 
 spec :: Spec
-spec = it "evaluates Term" pending
+spec = do
+  let y =
+        Lam
+          "f"
+          ( App
+              (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
+              (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
+          )
+      z =
+        Lam
+          "f"
+          ( App
+              (Lam "x" (App (Var "f") (Lam "y" (App (App (Var "x") (Var "x")) (Var "y")))))
+              (Lam "x" (App (Var "f") (Lam "y" (App (App (Var "x") (Var "x")) (Var "y")))))
+          )
 
---   let fix =
---         Lam
---           "f"
---           ( App
---               (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
---               (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
---           )
---   let omega = App fix fix
---   let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z")
---   let fst' = Lam "x" (Lam "y" (Var "x"))
+      omega =
+        App (Lam "x" (App (Var "x") (Var "x"))) (Lam "x" (App (Var "x") (Var "x")))
 
---   describe "call-by-value eval" $ do
---     it "evaluates 'x' as itself" $ do
---       let term = 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` 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` 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` V "z"
---     it "diverges on evaluating argument bound to ω" $
---       shouldDiverge $
---         eval term []
+      fst' = Lam "x" (Lam "y" (Var "x"))
+      snd' = Lam "x" (Lam "y" (Var "y"))
 
---   describe "call-by-need eval" $ do
---     it "evaluates 'x' as itself" $ do
---       evalNeed (Var "x") [] `shouldBe` V "x"
---     it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
---       evalNeed term [] `shouldBe` V "z"
---     it "diverges on evaluating ω" $
---       shouldDiverge $
---         evalNeed omega []
+  describe "call-by-value eval" $ do
+    it "evaluates 'x' as itself" $ do
+      let term = Var "x"
+      normalise term `shouldBe` Var "x"
+    it "evaluates '((λ x. x) y)' as 'y'" $ do
+      let term = App (Lam "x" (Var "x")) (Var "y")
+      normalise term `shouldBe` Var "y"
+    it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do
+      let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y")
+      normalise term `shouldBe` App (Var "t") (Var "y")
+    it "evaluates '((λ x y. x) z t)' as 'z'" $ do
+      let term = App (App fst' (Var "z")) (Var "t")
+      normalise term `shouldBe` Var "z"
+    it "diverges on evaluating ω" $
+      shouldDiverge $
+        normalise omega
+    it "diverges on evaluating ω applied to a function that use it" $
+      shouldDiverge $
+        normalise (App fst' omega)
+    it "diverges on evaluating ω applied to a function that do not use it" $
+      shouldDiverge $
+        normalise (App snd' omega)
+  describe "Church numerals" $ do
+    let zero = Lam "s" (Lam "z" (Var "z"))
+        one = Lam "s" (Lam "z" (App (Var "s") (Var "z")))
+        two = Lam "s" (Lam "z" (App "s" (App (Var "s") (Var "z"))))
+        succ' = Lam "n" (Lam "s" (Lam "z" (App (Var "s") (App (App (Var "n") (Var "s")) (Var "z")))))
+        add' = Lam "j" (Lam "k" (Lam "s" (Lam "z" (App (App "j" "s") (App (App "k" "s") "z")))))
 
--- shouldDiverge :: Value -> IO ()
--- shouldDiverge t =
---   race_
---     (t `seq` fail "Did not diverge")
---     (threadDelay 1000000)
+    it "normalises successor" $
+      normalise (App succ' zero)
+        `shouldBe` one
+
+    it "adds two numerals" $
+      normalise (App (App add' one) one)
+        `shouldBe` two
+
+  -- describe "call-by-name eval" $ do
+  --   it "evaluates 'x' as itself" $ do
+  --     normalise' (Var "x") `shouldBe` Var "x"
+  --   it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
+  --     normalise' (App (App snd' omega) "z") `shouldBe` Var "z"
+  --   it "diverges on evaluating ω" $
+  --     shouldDiverge $
+  --       normalise' omega
+
+shouldDiverge :: Term -> IO ()
+shouldDiverge t =
+  race_
+    (t `seq` fail "Did not diverge")
+    (threadDelay 1000000)