summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lambda-calcul/haskell/.gitignore1
-rw-r--r--lambda-calcul/haskell/README.md8
-rw-r--r--lambda-calcul/haskell/minilang.cabal95
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs36
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs97
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs57
-rw-r--r--lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs40
-rw-r--r--lambda-calcul/haskell/test/Minilang/Lambda/InferSpec.hs47
-rw-r--r--lambda-calcul/haskell/test/Spec.hs1
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 #-}
generated by cgit v1.2.3 (git 2.39.1) at 2026-02-05 22:17:31 +0000