From 1d1f0efc7de1eaa0c8a6b503892c2f950008fde6 Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud@pankzsoft.com>
Date: Tue, 28 Oct 2025 20:14:16 +0100
Subject: wip: port REPL from minilang

---
 lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs  | 36 +++++-----------------
 lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs | 24 +++++++--------
 lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs | 11 +++++++
 3 files changed, 30 insertions(+), 41 deletions(-)

(limited to 'lambda-calcul/haskell/src/Minilang/Lambda')

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index cbbdc51..58f8ba6 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -9,36 +9,14 @@ data Term
   | App Term Term
   deriving (Show, Read, Eq)
 
-type Env = [(Text, Value)]
+type Env = [(Text, Term)]
 
-data Value
-  = V Text
-  | Abs Text Term Env -- a closure, ie. lambda with its captured environment
-  | Ap Value Value
-  deriving (Show, Read, Eq)
+newEnv :: Env
+newEnv = []
 
 -- call-by-value evaluator
-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 -> 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
-        Abs x body env' -> eval body ((x, a') : env')
-        f' -> Ap f' a'
+eval :: Term -> Env -> Term
+eval = undefined
 
-evalNeed :: Term -> Env -> Value
-evalNeed (Var x) env = case lookup x env of
-  Just v -> v
-  Nothing -> V x
-evalNeed (Lam x body) env = Abs x body env
-evalNeed (App f a) env =
-  let a' = eval a env
-   in case evalNeed f env of
-        Abs x body env' -> evalNeed body ((x, a') : env')
-        f' -> Ap f' a'
+evalNeed :: Term -> Env -> Term
+evalNeed = undefined
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
index 415849a..94fecb3 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
@@ -48,14 +48,14 @@ typeOf (Var _ t) = t
 typeOf (Lam _ _ t) = t
 typeOf (App _ _ t) = t
 
-data Env = Env {nextVar :: Int, typeEnv :: Map.Map Text Type}
+data Context = Context {nextVar :: Int, typeContext :: Map.Map Text Type}
   deriving (Eq, Show)
 
 annotate :: Eval.Term -> Either TypeError (ATerm Type)
 annotate t =
-  evalStateT (go (fromTerm t) []) newEnv
+  evalStateT (go (fromTerm t) []) newContext
   where
-    go :: ATerm a -> [(Text, Type)] -> StateT Env (Either TypeError) (ATerm Type)
+    go :: ATerm a -> [(Text, Type)] -> StateT Context (Either TypeError) (ATerm Type)
     go t bounds = case t of
       Var x _ -> case List.lookup x bounds of
         Just ty -> pure $ Var x ty
@@ -73,22 +73,22 @@ annotate t =
       App a b _ ->
         App <$> go a bounds <*> go b bounds <*> freshVar
 
-newEnv :: Env
-newEnv = Env 0 Map.empty
+newContext :: Context
+newContext = Context 0 Map.empty
 
-bind :: Text -> Type -> StateT Env (Either TypeError) ()
+bind :: Text -> Type -> StateT Context (Either TypeError) ()
 bind x ty = do
-  modify (\(Env n env) -> Env n (Map.insert x ty env))
+  modify (\(Context n env) -> Context n (Map.insert x ty env))
 
-lookup :: Text -> StateT Env (Either TypeError) (Maybe Type)
+lookup :: Text -> StateT Context (Either TypeError) (Maybe Type)
 lookup x = do
-  Env _ env <- get
+  Context _ env <- get
   pure $ Map.lookup x env
 
-freshVar :: (Monad m) => StateT Env m Type
+freshVar :: (Monad m) => StateT Context m Type
 freshVar = do
-  get >>= \(Env n _) ->
-    modify (\(Env n' env') -> Env (n' + 1) env') >> pure (TyVar $ nameOf n)
+  get >>= \(Context n _) ->
+    modify (\(Context n' env') -> Context (n' + 1) env') >> pure (TyVar $ nameOf n)
   where
     nameOf n
       | n < 26 = pack [chr (n + ord 'a')]
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
index ad06552..df66113 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
@@ -1,4 +1,5 @@
 --  ported from https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-inference/type-inference.htm
+{-# LANGUAGE LambdaCase #-}
 module Minilang.Lambda.Unify where
 
 import Data.Text (Text)
@@ -12,6 +13,16 @@ data Type
 
 infixr 5 :->
 
+pretty :: Type -> Text
+pretty = \case
+  TyVar x -> x
+  f :-> g ->
+    let left = case f of
+          TyVar _ -> pretty f
+          _ -> "(" <> pretty f <> ")"
+        right = pretty g
+     in left <> " -> " <> right
+
 -- 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.
-- 
cgit v1.3.1