From 3a67e69bfe9492d2a2fc5e4b07cc8c909a346064 Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud@pankzsoft.com>
Date: Mon, 13 Oct 2025 09:27:07 +0200
Subject: add minimal evaluator and type inference

---
 .../haskell/test/Minilang/Lambda/EvalSpec.hs       | 40 ++++++++++++++++++
 .../haskell/test/Minilang/Lambda/InferSpec.hs      | 47 ++++++++++++++++++++++
 lambda-calcul/haskell/test/Spec.hs                 |  1 +
 3 files changed, 88 insertions(+)
 create mode 100644 lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
 create mode 100644 lambda-calcul/haskell/test/Minilang/Lambda/InferSpec.hs
 create mode 100644 lambda-calcul/haskell/test/Spec.hs

(limited to 'lambda-calcul/haskell/test')

diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
new file mode 100644
index 0000000..df933a4
--- /dev/null
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -0,0 +1,40 @@
+module Minilang.Lambda.EvalSpec (spec) where
+
+import Control.Concurrent (threadDelay)
+import Control.Concurrent.Async (race_)
+import Minilang.Lambda.Eval (Term (..), eval, evalNeed)
+import Test.Hspec (Spec, describe, it, shouldBe)
+
+spec :: Spec
+spec = do
+  let fix = Lam "x" (App (Var "x") (Var "x"))
+  let omega = App fix fix
+  let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z")
+
+  describe "call-by-value eval" $ do
+    it "evaluates 'x' as itself" $ do
+      let term = Var "x"
+      eval term [] `shouldBe` Var "x"
+    it "evaluates '((λ x. x) y)' as 'y'" $ do
+      let term = App (Lam "x" (Var "x")) (Var "y")
+      eval term [] `shouldBe` Var "y"
+    it "evaluates '((λ x y. y) y z t)' as '(z t)'" $ do
+      let snd' = Lam "x" (Lam "y" (Var "y"))
+      let term = App (App (App snd' (Var "y")) (Var "z")) (Var "t")
+      eval term [] `shouldBe` App (Var "z") (Var "t")
+    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"
+    it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
+      evalNeed term [] `shouldBe` Var "z"
+    it "diverges on evaluating ω" $
+      shouldDiverge $ evalNeed omega []
+
+shouldDiverge :: Term -> IO ()
+shouldDiverge t =
+  race_
+    (t `seq` fail "Did not diverge")
+    (threadDelay 1000000)
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/InferSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/InferSpec.hs
new file mode 100644
index 0000000..dac76ec
--- /dev/null
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/InferSpec.hs
@@ -0,0 +1,47 @@
+module Minilang.Lambda.InferSpec (spec) where
+
+import Minilang.Lambda.Eval (Term (..))
+import Minilang.Lambda.Infer (TypeError (..), annotate)
+import qualified Minilang.Lambda.Infer as Ann
+import Minilang.Lambda.Unify (Type (..), UnifyError (..))
+import Test.Hspec (Spec, describe, it, shouldBe)
+
+spec :: Spec
+spec = do
+  describe "annotate" $ do
+    it "annotates unknown variable with fresh type variable" $ do
+      let term = Var "x"
+      annotate term `shouldBe` Right (Ann.Var "x" (TyVar "a"))
+    it "annotates bound λ variable with fresh type variable" $ do
+      let term = Lam "x" (Var "x")
+      annotate term `shouldBe` Right (Ann.Lam "x" (Ann.Var "x" (TyVar "a")) (TyVar "a" :-> TyVar "a"))
+    it "annotates application with fresh type variables" $ do
+      let term = App (Var "x") (Var "y")
+      annotate term `shouldBe` Right (Ann.App (Ann.Var "x" (TyVar "a")) (Ann.Var "y" (TyVar "b")) (TyVar "c"))
+    it "reuse free variables types" $ do
+      let term = App (Var "x") (Var "x")
+      annotate term `shouldBe` Right (Ann.App (Ann.Var "x" (TyVar "a")) (Ann.Var "x" (TyVar "a")) (TyVar "b"))
+  describe "infer" $ do
+    it "infers correctly some expressions" $ do
+      let id' = Lam "x" (Var "x")
+      let fst' = Lam "x" (Lam "y" (Var "x"))
+      let snd' = Lam "x" (Lam "y" (Var "y"))
+      let comp = Lam "f" (Lam "g" (Lam "x" (App (Var "f") (App (Var "g") (Var "x")))))
+      let k = Lam "x" (Lam "y" (Lam "z" (App (App (Var "x") (Var "z")) (App (Var "y") (Var "z")))))
+
+      Ann.infer id' `shouldBe` Right (TyVar "a" :-> TyVar "a")
+      Ann.infer fst' `shouldBe` Right (TyVar "a" :-> (TyVar "b" :-> TyVar "a"))
+      Ann.infer snd' `shouldBe` Right (TyVar "a" :-> (TyVar "b" :-> TyVar "b"))
+      Ann.infer comp `shouldBe` Right ((TyVar "d" :-> TyVar "e") :-> ((TyVar "c" :-> TyVar "d") :-> (TyVar "c" :-> TyVar "e")))
+      Ann.infer k
+        `shouldBe` Right
+          ( (TyVar "c" :-> TyVar "e" :-> TyVar "f")
+              :-> (TyVar "c" :-> TyVar "e")
+              :-> TyVar "c"
+              :-> TyVar "f"
+          )
+
+    it "rejects circular references" $ do
+      let circ = Lam "f" (App (Lam "x" (App (App (Var "f") (Var "x")) (Var "x"))) (Lam "y" (App (App (Var "f") (Var "y")) (Var "y"))))
+
+      Ann.infer circ `shouldBe` Left (UnifyError $ Circularity "e" (TyVar "e" :-> TyVar "g"))
diff --git a/lambda-calcul/haskell/test/Spec.hs b/lambda-calcul/haskell/test/Spec.hs
new file mode 100644
index 0000000..a824f8c
--- /dev/null
+++ b/lambda-calcul/haskell/test/Spec.hs
@@ -0,0 +1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
-- 
cgit v1.2.3