summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/src/Minilang/Lambda
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud@pankzsoft.com>2025-10-28 20:14:16 +0100
committerArnaud Bailly <arnaud@pankzsoft.com>2025-10-28 20:14:16 +0100
commit1d1f0efc7de1eaa0c8a6b503892c2f950008fde6 (patch)
treebd2e2ea5963d8a208d302854502f580d8ffd73cb /lambda-calcul/haskell/src/Minilang/Lambda
parenta210419fd60c00d011f70fb1b968031621e4c01a (diff)
downloadlambda-nantes-1d1f0efc7de1eaa0c8a6b503892c2f950008fde6.tar.gz
wip: port REPL from minilang
Diffstat (limited to 'lambda-calcul/haskell/src/Minilang/Lambda')
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs36
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs24
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs11
3 files changed, 30 insertions, 41 deletions
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.