add minimal evaluator and type inference

9 files changed, 382 insertions, 0 deletions

diff --git a/lambda-calcul/haskell/.gitignore b/lambda-calcul/haskell/.gitignore
new file mode 100644
index 0000000..c33954f
--- /dev/null
+++ b/lambda-calcul/haskell/.gitignore
@@ -0,0 +1 @@
+dist-newstyle/
diff --git a/lambda-calcul/haskell/README.md b/lambda-calcul/haskell/README.md
new file mode 100644
index 0000000..096627c
--- /dev/null
+++ b/lambda-calcul/haskell/README.md
@@ -0,0 +1,8 @@
+
+# minilang
+
+A minimal functional language to learn and experiment with type systems.
+
+* http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf
+* https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
+* https://github.com/kino3/Mini-TT
diff --git a/lambda-calcul/haskell/minilang.cabal b/lambda-calcul/haskell/minilang.cabal
new file mode 100644
index 0000000..817672e
--- /dev/null
+++ b/lambda-calcul/haskell/minilang.cabal
@@ -0,0 +1,95 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.35.1.
+--
+-- see: https://github.com/sol/hpack
+
+name:           minilang
+version:        0.1.0.0
+description:    Please see the README on Github at <https://github.com/abailly/xxi-century-typed/minilang#readme>
+homepage:       https://github.com/abailly/minilang#readme
+bug-reports:    https://github.com/abailly/minilang/issues
+author:         Arnaud Bailly
+maintainer:     arnaud@pankzsoft.com
+copyright:      2025 Arnaud Bailly
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/abailly/minilang
+
+library
+  exposed-modules:
+      Minilang.Lambda.Unify
+      Minilang.Lambda.Eval
+      Minilang.Lambda.Infer
+  hs-source-dirs:
+      src
+  default-extensions:
+      DeriveGeneric
+      OverloadedStrings
+      FlexibleInstances
+      MultiParamTypeClasses
+      FlexibleContexts
+      RecordWildCards
+      NamedFieldPuns
+      GeneralizedNewtypeDeriving
+  ghc-options: -Wall -fno-warn-orphans
+  build-depends:
+      aeson
+    , async
+    , base
+    , bytestring
+    , containers
+    , data-default
+    , directory
+    , exceptions
+    , filepath
+    , mtl
+    , stm
+    , text
+    , unordered-containers
+  default-language: Haskell2010
+
+test-suite minilang-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Minilang.Lambda.InferSpec
+      Minilang.Lambda.EvalSpec
+  hs-source-dirs:
+      test
+  default-extensions:
+      DeriveGeneric
+      OverloadedStrings
+      FlexibleInstances
+      MultiParamTypeClasses
+      FlexibleContexts
+      RecordWildCards
+      NamedFieldPuns
+      GeneralizedNewtypeDeriving
+  ghc-options: -Wall -fno-warn-orphans -threaded -rtsopts -with-rtsopts=-N
+  build-tool-depends:
+      hspec-discover:hspec-discover
+  build-depends:
+      QuickCheck
+    , async
+    , base
+    , bytestring
+    , containers
+    , data-default
+    , directory
+    , exceptions
+    , filepath
+    , hspec
+    , hspec-discover
+    , minilang
+    , mtl
+    , text
+    , unordered-containers
+  default-language: Haskell2010
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
new file mode 100644
index 0000000..68b01be
--- /dev/null
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -0,0 +1,36 @@
+module Minilang.Lambda.Eval where
+
+import Data.Text (Text)
+
+data Term
+  = Var Text
+  | Lam Text Term
+  | App Term Term
+  deriving (Show, Eq)
+
+type Env = [(Text, Term)]
+
+-- call-by-value evaluator
+eval :: Term -> Env -> Term
+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
+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'
+
+evalNeed :: Term -> Env -> Term
+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
+evalNeed (App f a) env =
+  case evalNeed f env of
+    Lam x body -> evalNeed body ((x, a) : env)
+    f' -> App f' a
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
new file mode 100644
index 0000000..415849a
--- /dev/null
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Minilang.Lambda.Infer where
+
+import Control.Monad.State (MonadState (..), StateT, evalStateT, modify)
+import Data.Bifunctor (first)
+import Data.Char (chr, ord)
+import qualified Data.List as List
+import qualified Data.Map as Map
+import Data.Text (Text, pack)
+import qualified Minilang.Lambda.Eval as Eval
+import Minilang.Lambda.Unify (Type (..), UnifyError, apply, unify)
+import Prelude hiding (lookup)
+
+data ATerm ann
+  = Var Text ann
+  | Lam Text (ATerm ann) ann
+  | App (ATerm ann) (ATerm ann) ann
+  deriving (Show, Eq)
+
+data TypeError
+  = UnifyError UnifyError
+  deriving (Show, Eq)
+
+fromTerm :: Eval.Term -> ATerm ()
+fromTerm (Eval.Var x) = Var x ()
+fromTerm (Eval.Lam x body) = Lam x (fromTerm body) ()
+fromTerm (Eval.App a b) = App (fromTerm a) (fromTerm b) ()
+
+infer :: Eval.Term -> Either TypeError Type
+infer t = do
+  annotated <- annotate t
+  constraints <- collect [annotated] []
+  subs <- first UnifyError $ unify constraints
+  pure $ apply subs (typeOf annotated)
+
+collect :: [ATerm Type] -> [(Type, Type)] -> Either TypeError [(Type, Type)]
+collect terms constraints = case terms of
+  [] -> Right constraints
+  (Var _ _) : rest -> collect rest constraints
+  (Lam _ body _) : rest -> collect (body : rest) constraints
+  (App x y t) : rest ->
+    let (f, b) = (typeOf x, typeOf y)
+     in collect (x : y : rest) ((f, b :-> t) : constraints)
+
+typeOf :: ATerm Type -> Type
+typeOf (Var _ t) = t
+typeOf (Lam _ _ t) = t
+typeOf (App _ _ t) = t
+
+data Env = Env {nextVar :: Int, typeEnv :: Map.Map Text Type}
+  deriving (Eq, Show)
+
+annotate :: Eval.Term -> Either TypeError (ATerm Type)
+annotate t =
+  evalStateT (go (fromTerm t) []) newEnv
+  where
+    go :: ATerm a -> [(Text, Type)] -> StateT Env (Either TypeError) (ATerm Type)
+    go t bounds = case t of
+      Var x _ -> case List.lookup x bounds of
+        Just ty -> pure $ Var x ty
+        Nothing ->
+          lookup x >>= \case
+            Just ty -> pure $ Var x ty
+            Nothing -> do
+              v <- freshVar
+              bind x v
+              pure $ Var x v
+      Lam x body _ -> do
+        ty <- freshVar
+        body' <- go body ((x, ty) : bounds)
+        pure $ Lam x body' (ty :-> typeOf body')
+      App a b _ ->
+        App <$> go a bounds <*> go b bounds <*> freshVar
+
+newEnv :: Env
+newEnv = Env 0 Map.empty
+
+bind :: Text -> Type -> StateT Env (Either TypeError) ()
+bind x ty = do
+  modify (\(Env n env) -> Env n (Map.insert x ty env))
+
+lookup :: Text -> StateT Env (Either TypeError) (Maybe Type)
+lookup x = do
+  Env _ env <- get
+  pure $ Map.lookup x env
+
+freshVar :: (Monad m) => StateT Env m Type
+freshVar = do
+  get >>= \(Env n _) ->
+    modify (\(Env n' env') -> Env (n' + 1) env') >> pure (TyVar $ nameOf n)
+  where
+    nameOf n
+      | n < 26 = pack [chr (n + ord 'a')]
+      | otherwise =
+          let (d, r) = n `divMod` 26
+           in pack $ chr (r + ord 'a') : show d
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
new file mode 100644
index 0000000..ad06552
--- /dev/null
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
@@ -0,0 +1,57 @@
+--  ported from https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-inference/type-inference.htm
+module Minilang.Lambda.Unify where
+
+import Data.Text (Text)
+
+type Identifier = Text
+
+data Type
+  = TyVar Text
+  | Type :-> Type
+  deriving (Show, Eq)
+
+infixr 5 :->
+
+-- invariant: no identifier on the left hand-side can appear in
+-- an earlier term in the list, ie. the list is in "dependency order"
+-- and forms a DAG.
+type Substitution = [(Identifier, Type)]
+
+occurs :: Identifier -> Type -> Bool
+occurs x (TyVar y) = x == y
+occurs x (f :-> g) = occurs x f || occurs x g
+
+subst :: Type -> Identifier -> Type -> Type
+subst s x t@(TyVar y)
+  | x == y = s
+  | otherwise = t
+subst s x (f :-> g) = subst s x f :-> subst s x g
+
+apply :: Substitution -> Type -> Type
+apply subs t =
+  foldr (\(x, s) -> subst s x) t subs
+
+data UnifyError
+  = MismatchHead Text Text [Type] [Type]
+  | Circularity Identifier Type
+  deriving (Show, Eq)
+
+unifyOne :: Type -> Type -> Either UnifyError Substitution
+unifyOne (TyVar x) (TyVar y) = if x == y then Right [] else Right [(x, TyVar y)]
+unifyOne (f :-> g) (f' :-> g') =
+  unify [(f, f'), (g, g')]
+unifyOne (TyVar x) t =
+  if occurs x t
+    then Left $ Circularity x t
+    else Right [(x, t)]
+unifyOne t (TyVar x) =
+  if occurs x t
+    then Left $ Circularity x t
+    else Right [(x, t)]
+
+unify :: [(Type, Type)] -> Either UnifyError Substitution
+unify [] = Right []
+unify ((s, t) : rest) = do
+  sub2 <- unify rest
+  sub1 <- unifyOne (apply sub2 s) (apply sub2 t)
+  return $ sub1 ++ sub2
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 #-}