From ff9064a05c17de2a50ec10afa0bed3ecd90b1c48 Mon Sep 17 00:00:00 2001
From: "Viktor A. Rozenko Voitenko" <sharp.vik@gmail.com>
Date: Fri, 10 May 2024 15:26:29 +0300
Subject: [PATCH 1/8] feat(Parser): parse `when x is` expressions

---
 src/Pure/Expr.hs         | 59 ++++++++++++++++--------------
 src/Pure/Parser.hs       | 39 ++++++++++++++------
 src/Pure/Sacred.hs       |  5 ++-
 src/Pure/Typing/Infer.hs | 78 +++++++++++++++++++++-------------------
 4 files changed, 108 insertions(+), 73 deletions(-)

diff --git a/src/Pure/Expr.hs b/src/Pure/Expr.hs
index 79ca3ca..640cb69 100644
--- a/src/Pure/Expr.hs
+++ b/src/Pure/Expr.hs
@@ -1,4 +1,6 @@
-module Pure.Expr (Expr (..), positionOf) where
+{-# LANGUAGE FlexibleInstances #-}
+
+module Pure.Expr (Expr (..), Literal (..), positionOf) where
 
 import qualified Pure.Sacred as S
 import Text.Parsec (SourcePos)
@@ -9,47 +11,52 @@ import Utility.Strings (Parens (..), list, parenthesised, (+-+))
 
 data Expr
   = Lam Id Expr SourcePos
+  | When Expr [(Expr, Expr)] SourcePos
   | If Expr Expr Expr SourcePos
   | App Expr Expr SourcePos
-  | List [Expr] SourcePos
-  | Id Id SourcePos
-  | Str String SourcePos
-  | Float Double SourcePos
-  | Int Integer SourcePos
-  | Bool Bool SourcePos
+  | Literal Literal SourcePos
+  deriving (Eq)
+
+data Literal
+  = List [Expr]
+  | Id Id
+  | Str String
+  | Float Double
+  | Int Integer
+  | Bool Bool
   deriving (Eq)
 
 -- POSITION --------------------------------------------------------------------
 
 positionOf :: Expr -> SourcePos
 positionOf (Lam _ _ pos) = pos
+positionOf (When _ _ pos) = pos
 positionOf (If _ _ _ pos) = pos
 positionOf (App _ _ pos) = pos
-positionOf (List _ pos) = pos
-positionOf (Id _ pos) = pos
-positionOf (Str _ pos) = pos
-positionOf (Float _ pos) = pos
-positionOf (Int _ pos) = pos
-positionOf (Bool _ pos) = pos
+positionOf (Literal _ pos) = pos
 
 -- SHOW ------------------------------------------------------------------------
 
 instance Parens Expr where
-  parens b@(Bool _ _) = show b
-  parens i@(Int _ _) = show i
-  parens f@(Float _ _) = show f
-  parens s@(Str _ _) = show s
-  parens i@(Id _ _) = show i
-  parens l@(List _ _) = show l
+  parens l@(Literal _ _) = show l
   parens ex = parenthesised $ show ex
 
 instance Show Expr where
-  show (Bool bool _) = show bool
-  show (Int int _) = show int
-  show (Float number _) = show number
-  show (Str str _) = show str
-  show (Id ident _) = ident
-  show (List l _) = list (map show l)
+  show (Literal literal _) = show literal
   show (App f arg _) = show f +-+ parens arg
   show (If x y z _) = S.if_ +-+ show x +-+ S.then_ +-+ show y +-+ S.else_ +-+ show z
-  show (Lam p ex _) = p +-+ S.arrow +-+ show ex
\ No newline at end of file
+  show (Lam p ex _) = p +-+ S.arrow +-+ show ex
+  show (When _ [] _) = undefined
+  show (When e branches _) =
+    S.when +-+ show e +-+ S.is +-+ unwords (map showBranch branches)
+    where
+      showBranch (pattern, result) =
+        [S.bar] +-+ show pattern +-+ S.then_ +-+ show result
+
+instance Show Literal where
+  show (Bool bool) = show bool
+  show (Int int) = show int
+  show (Float number) = show number
+  show (Str str) = show str
+  show (Id ident) = ident
+  show (List l) = list (map show l)
\ No newline at end of file
diff --git a/src/Pure/Parser.hs b/src/Pure/Parser.hs
index 84fdba0..2c7e606 100644
--- a/src/Pure/Parser.hs
+++ b/src/Pure/Parser.hs
@@ -4,7 +4,6 @@
 
 module Pure.Parser
   ( Module (..),
-    Id,
     moduleNames,
     assignmentNames,
     typeHintNames,
@@ -21,7 +20,7 @@ import Data.Char (isLowerCase, isUpperCase)
 import Data.Functor ((<&>))
 import Data.List (intercalate)
 import Data.Maybe (isJust, mapMaybe)
-import Pure.Expr (Expr (..), positionOf)
+import Pure.Expr (Expr (..), Literal (..), positionOf)
 import qualified Pure.Sacred as S
 import Pure.Typing.Type (Type (..))
 import Text.Parsec
@@ -248,7 +247,26 @@ defP = do
   return $ ValueDef name expr
 
 exprP :: Parser Expr
-exprP = try ifP <|> try lambdaP <|> try appP <|> literalP <?> "an expression"
+exprP =
+  try whenP
+    <|> try ifP
+    <|> try lambdaP
+    <|> try appP
+    <|> literalP
+    <?> "an expression"
+
+whenP :: Parser Expr
+whenP = do
+  pos <- sourcePos
+  e <- between (reservedP S.when) (reservedP S.is) notIfP
+  brs <- barP >> sepBy1 branchP barP
+  return $ When e brs pos
+  where
+    barP = reservedOp parser [S.bar]
+    branchP = do
+      pat <- literalP <* reservedP S.then_
+      result <- exprP
+      return (pat, result)
 
 ifP :: Parser Expr
 ifP = do
@@ -295,44 +313,45 @@ listP :: Parser Expr
 listP = do
   pos <- sourcePos
   list <- brackets parser $ commaSep1 parser exprP
-  return $ List list pos
+  return $ Literal (List list) pos
 
 qualifiedP :: Parser Expr
 qualifiedP = do
   pos <- sourcePos
   qual <- sepBy1 nameP (char S.dot) <&> intercalate [S.dot]
-  return $ Id qual pos
+  return $ Literal (Id qual) pos
 
 idP :: Parser Expr
 idP = do
   pos <- sourcePos
   name <- nameP
-  return $ Id name pos
+  return $ Literal (Id name) pos
 
 strP :: Parser Expr
 strP = do
   pos <- sourcePos
   str <- stringLiteral parser
-  return $ Str str pos
+  return $ Literal (Str str) pos
 
 floatP :: Parser Expr
 floatP = do
   pos <- sourcePos
   sign <- optionMaybe $ char S.minus
   number <- float parser
-  return $ Float (if isJust sign then -number else number) pos
+  let flt = Float (if isJust sign then -number else number)
+  return $ Literal flt pos
 
 intP :: Parser Expr
 intP = do
   pos <- sourcePos
   int <- integer parser
-  return $ Int int pos
+  return $ Literal (Int int) pos
 
 boolP :: Parser Expr
 boolP = do
   pos <- sourcePos
   b <- symbolP S.true <|> symbolP S.false
-  return $ Bool (read b) pos
+  return $ Literal (Bool (read b)) pos
 
 reservedP :: String -> Parser ()
 reservedP = reserved parser
diff --git a/src/Pure/Sacred.hs b/src/Pure/Sacred.hs
index e2a3e03..3051590 100644
--- a/src/Pure/Sacred.hs
+++ b/src/Pure/Sacred.hs
@@ -10,7 +10,7 @@ isKeyword :: String -> Bool
 isKeyword = flip List.elem keywords
 
 keywords :: [String]
-keywords = [export, if_, then_, else_, type_, is]
+keywords = [export, if_, then_, else_, type_, when, is]
 
 export :: String
 export = "export"
@@ -27,6 +27,9 @@ else_ = "else"
 type_ :: String
 type_ = "type"
 
+when :: String
+when = "when"
+
 is :: String
 is = "is"
 
diff --git a/src/Pure/Typing/Infer.hs b/src/Pure/Typing/Infer.hs
index 97266c2..f69f025 100644
--- a/src/Pure/Typing/Infer.hs
+++ b/src/Pure/Typing/Infer.hs
@@ -15,7 +15,7 @@ import Control.Monad.Except (ExceptT, runExceptT, throwError, withError)
 import Control.Monad.State (State, evalState, get, put, runState)
 import Data.Functor ((<&>))
 import qualified Data.Set as Set
-import Pure.Expr (Expr (..))
+import Pure.Expr (Expr (..), Literal (..))
 import Pure.Typing.Env (Apply (..), Env (..), (<:>))
 import qualified Pure.Typing.Env as Env
 import Pure.Typing.Error (Error (..))
@@ -71,41 +71,47 @@ assert' ctx hint expr = do
   s2 <- unify tyHint tyExpr
   return $ generalize ctx (s2 <:> s1 +-> tyHint)
 
-infer :: Context -> Expr -> TI (Subst, Type)
-infer _ (Bool _ _) = return (Env.empty, tBool)
-infer _ (Int _ _) = return (Env.empty, tInt)
-infer _ (Float _ _) = return (Env.empty, tFloat)
-infer _ (Str _ _) = return (Env.empty, tStr)
-infer ctx (Id i _) =
-  case Env.typeOf i ctx of
-    Nothing -> throwUnboundVariableError i
-    Just scheme -> instantiate scheme <&> (,) Env.empty
-infer _ (List [] _) = var <&> (,) Env.empty
-infer ctx (List (x : xs) pos) = do
-  (s1, tx) <- infer ctx x
-  (s2, txs) <- infer (s1 +-> ctx) (List xs pos)
-  s3 <- unify (tList tx) txs
-  return (s3 <:> s2 <:> s1, s3 +-> txs)
-infer ctx (App fun arg _) = do
-  (s1, tyFun) <- infer ctx fun
-  (s2, tyArg) <- infer (s1 +-> ctx) arg
-  tyRes <- var
-  s3 <- unify (tyArg :-> tyRes) (s2 +-> tyFun)
-  return (s3 <:> s2 <:> s1, s3 +-> tyRes)
-infer ctx (If condition e1 e2 _) = do
-  (s1, t1) <- infer ctx condition
-  (s2, t2) <- infer (s1 +-> ctx) e1
-  (s3, t3) <- infer (s2 <:> s1 +-> ctx) e2
-  s4 <- unify (s3 <:> s2 <:> s1 +-> t1) tBool
-  s5 <- unify (s4 <:> s3 <:> s2 <:> s1 +-> t2) t3
-  let s = s5 <:> s4 <:> s3 <:> s2 <:> s1
-  let t = s +-> t2
-  return (s, t)
-infer ctx (Lam binder body _) = do
-  tyBinder <- var
-  let tmpCtx = Env.insert binder ([] :. tyBinder) ctx
-  (s1, tyBody) <- infer tmpCtx body
-  return (s1, (s1 +-> tyBinder) :-> tyBody)
+class Infer a where
+  infer :: Context -> a -> TI (Subst, Type)
+
+instance Infer Literal where
+  infer _ (Bool _) = return (Env.empty, tBool)
+  infer _ (Int _) = return (Env.empty, tInt)
+  infer _ (Float _) = return (Env.empty, tFloat)
+  infer _ (Str _) = return (Env.empty, tStr)
+  infer ctx (Id i) =
+    case Env.typeOf i ctx of
+      Nothing -> throwUnboundVariableError i
+      Just scheme -> instantiate scheme <&> (,) Env.empty
+  infer _ (List []) = var <&> (,) Env.empty
+  infer ctx (List (x : xs)) = do
+    (s1, tx) <- infer ctx x
+    (s2, txs) <- infer (s1 +-> ctx) (List xs)
+    s3 <- unify (tList tx) txs
+    return (s3 <:> s2 <:> s1, s3 +-> txs)
+
+instance Infer Expr where
+  infer ctx (Literal literal _) = infer ctx literal
+  infer ctx (App fun arg _) = do
+    (s1, tyFun) <- infer ctx fun
+    (s2, tyArg) <- infer (s1 +-> ctx) arg
+    tyRes <- var
+    s3 <- unify (tyArg :-> tyRes) (s2 +-> tyFun)
+    return (s3 <:> s2 <:> s1, s3 +-> tyRes)
+  infer ctx (If condition e1 e2 _) = do
+    (s1, t1) <- infer ctx condition
+    (s2, t2) <- infer (s1 +-> ctx) e1
+    (s3, t3) <- infer (s2 <:> s1 +-> ctx) e2
+    s4 <- unify (s3 <:> s2 <:> s1 +-> t1) tBool
+    s5 <- unify (s4 <:> s3 <:> s2 <:> s1 +-> t2) t3
+    let s = s5 <:> s4 <:> s3 <:> s2 <:> s1
+    let t = s +-> t2
+    return (s, t)
+  infer ctx (Lam binder body _) = do
+    tyBinder <- var
+    let tmpCtx = Env.insert binder ([] :. tyBinder) ctx
+    (s1, tyBody) <- infer tmpCtx body
+    return (s1, (s1 +-> tyBinder) :-> tyBody)
 
 -- HELPERS ---------------------------------------------------------------------
 

From 7241eb69c1867aa72a0d18341e41c1dec58f1085 Mon Sep 17 00:00:00 2001
From: "Viktor A. Rozenko Voitenko" <sharp.vik@gmail.com>
Date: Sun, 12 May 2024 18:45:13 +0300
Subject: [PATCH 2/8] rename: purist -> pure

---
 CHANGELOG.md          |  2 +-
 README.md             | 29 ++++++++++++++++-------------
 app/Main.hs           |  2 +-
 install.sh            |  6 +++---
 src/Pure/Parser.hs    | 12 ++++--------
 vim/ftdetect/pure.vim |  2 +-
 vim/syntax/pure.vim   |  2 +-
 7 files changed, 27 insertions(+), 28 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index be25259..c1f2b4e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,4 @@
-# Changelog for `purist`
+# Changelog for `pure`
 
 All notable changes to this project will be documented in this file.
 
diff --git a/README.md b/README.md
index a6a22cc..cf898e4 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# `purist` - Pure Dev Suite 🧰
+# `pure` - Pure Dev Suite 🧰
 
 Pure is a
 
@@ -27,15 +27,15 @@ We hope that Pure will be able to target the following use cases:
 You may use the installation script:
 
 ```bash
-source <(curl -s https://raw.githubusercontent.com/prog-lang/purist/main/install.sh)
+source <(curl -s https://raw.githubusercontent.com/prog-lang/pure/main/install.sh)
 ```
 
 Or execute these commands manually (the script does the same as the following
 code snippet):
 
 ```bash
-git clone git@github.com:prog-lang/purist.git
-cd purist
+git clone git@github.com:prog-lang/pure.git
+cd pure
 stack install
 ```
 
@@ -49,7 +49,7 @@ on UNIX systems and probably something similar on Windows.
 Therefore, uninstalling is extremely straightforward:
 
 ```bash
-rm $(which purist)
+rm $(which pure)
 ```
 
 ## Usage Basics 👷‍♀️
@@ -57,10 +57,10 @@ rm $(which purist)
 The following command will transpile `someModule.pure` into `someModule.js`.
 
 ```bash
-purist c < someModule.pure > someModule.js
+pure compile someModule.pure > someModule.js
 ```
 
-**NOTE:** Executing `purist` with no arguments displays the _help_ message. Use
+**NOTE:** Executing `pure` with no arguments displays the _help_ message. Use
 it to get acquainted with its capabilities.
 
 ## Develop 👨‍💻
@@ -73,10 +73,10 @@ We are working hard to give you a tool you can be excited about.
 ### Progress
 
 - [x] [Parser](./src/Pure/Parser.hs)
-- [x] [Module (AST)](./src/Pure.hs)
-- [ ] Type Checker with Inference
-- [ ] [Transpiler $\to$ Node.js](./src/Node/Transpiler.hs)
-- [ ] Transpiler $\to$ Go
+- [x] [Type Checker with Inference](./src/Pure/Typing/)
+- [x] [Transpiler to Node.js](./src/Node/Transpiler.hs)
+- [ ] `when x is` expressions
+- [ ] `trait T a can` and `proof T R can` typing
 
 ### Vision
 
@@ -90,9 +90,14 @@ ever touched Elm or Haskell, you will know what I'm on about.
 
 ### Inspiration
 
+- [Elm][elm] - a delightful language for reliable web applications
 - [Duet][duet] - a subset of Haskell aimed at aiding teachers teach Haskell
 - [PureScript][ps] - a strongly-typed language that compiles to JavaScript
 
+[elm]: https://elm-lang.org/
+[duet]: https://github.com/chrisdone/duet
+[ps]: https://github.com/purescript/purescript
+
 ### Syntactic Analysis
 
 - [Parsec tutorial][parsecTutorial] and some conveniences like
@@ -111,8 +116,6 @@ ever touched Elm or Haskell, you will know what I'm on about.
 - [Programming Languages: Application and Interpretation][langs-ch.15] -
   chapter 15: Checking Program Invariants Statically: Types
 
-[duet]: https://github.com/chrisdone/duet
-[ps]: https://github.com/purescript/purescript
 [thih]: https://github.com/ocramz/thih
 [thih-pdf]: https://web.cecs.pdx.edu/~mpj/thih/thih.pdf
 [warn]: http://moscova.inria.fr/~maranget/papers/warn/warn.pdf
diff --git a/app/Main.hs b/app/Main.hs
index ce9268b..fdb43bc 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -18,7 +18,7 @@ main = runIO app
 app :: Application
 app =
   application
-    "purist"
+    "pure"
     (showVersion version)
     "Development suite for the Pure programming language"
     ["Viktor A. Rozenko Voitenko <sharp.vik@gmail.com>"]
diff --git a/install.sh b/install.sh
index 393d0d0..868624f 100644
--- a/install.sh
+++ b/install.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 
-git clone git@github.com:prog-lang/purist.git
-cd purist
+git clone git@github.com:prog-lang/pure.git
+cd pure
 stack install
 cd ..
-rm -rf purist
+rm -rf pure
diff --git a/src/Pure/Parser.hs b/src/Pure/Parser.hs
index 2c7e606..b213440 100644
--- a/src/Pure/Parser.hs
+++ b/src/Pure/Parser.hs
@@ -188,11 +188,9 @@ definitionP = Def <$> (typeDefP <|> try typeHintP <|> defP)
 
 typeDefP :: Parser Def
 typeDefP = do
-  _ <- reservedP S.type_
-  name <- upperNameP
+  name <- reservedP S.type_ >> upperNameP
   params <- many lowerNameP
-  _ <- reservedP S.is >> barP
-  cons <- sepBy1 typeConsP barP
+  cons <- reservedP S.is >> barP >> sepBy1 typeConsP barP
   return $ TypeDef name params cons
   where
     barP = reservedOp parser [S.bar]
@@ -200,8 +198,7 @@ typeDefP = do
 typeHintP :: Parser Def
 typeHintP = do
   name <- nameP
-  _ <- reservedOp parser S.typed
-  ty <- typeP
+  ty <- reservedOp parser S.typed >> typeP
   return $ TypeHint name ty
 
 typeConsP :: Parser Type
@@ -242,8 +239,7 @@ typeVarP = do
 defP :: Parser Def
 defP = do
   name <- nameP
-  _ <- reservedOp parser S.walrus
-  expr <- exprP
+  expr <- reservedOp parser S.walrus >> exprP
   return $ ValueDef name expr
 
 exprP :: Parser Expr
diff --git a/vim/ftdetect/pure.vim b/vim/ftdetect/pure.vim
index 000ea7e..b0be9fb 100644
--- a/vim/ftdetect/pure.vim
+++ b/vim/ftdetect/pure.vim
@@ -1,2 +1,2 @@
-" directive for Pure (github.com/prog-lang/purist)
+" directive for Pure (github.com/prog-lang/pure)
 autocmd BufRead,BufNewFile *.pure set filetype=pure
\ No newline at end of file
diff --git a/vim/syntax/pure.vim b/vim/syntax/pure.vim
index 8024101..bd8f819 100644
--- a/vim/syntax/pure.vim
+++ b/vim/syntax/pure.vim
@@ -1,4 +1,4 @@
-" syntax highlighting for Pure (github.com/prog-lang/purist)
+" syntax highlighting for Pure (github.com/prog-lang/pure)
 
 if exists('b:current_syntax')
   finish

From 96bded215fbd70fff4669be9ae0ca0af13d4b6f8 Mon Sep 17 00:00:00 2001
From: "Viktor A. Rozenko Voitenko" <sharp.vik@gmail.com>
Date: Tue, 14 May 2024 13:24:40 +0300
Subject: [PATCH 3/8] refactor(Infer): replace Subst and Context

---
 src/Pure/Typing/Infer.hs | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Pure/Typing/Infer.hs b/src/Pure/Typing/Infer.hs
index f69f025..a11d048 100644
--- a/src/Pure/Typing/Infer.hs
+++ b/src/Pure/Typing/Infer.hs
@@ -16,7 +16,7 @@ import Control.Monad.State (State, evalState, get, put, runState)
 import Data.Functor ((<&>))
 import qualified Data.Set as Set
 import Pure.Expr (Expr (..), Literal (..))
-import Pure.Typing.Env (Apply (..), Env (..), (<:>))
+import Pure.Typing.Env (Apply (..), Context, Subst, (<:>))
 import qualified Pure.Typing.Env as Env
 import Pure.Typing.Error (Error (..))
 import Pure.Typing.Free (Free (..))
@@ -28,11 +28,7 @@ import Utility.Result (Result (..))
 import qualified Utility.Result as Result
 import Utility.Strings (base26, (+-+), (+\\+))
 
--- TYPES -----------------------------------------------------------------------
-
-type Subst = Env Type
-
-type Context = Env Scheme
+-- TYPE INFERENCE MONAD --------------------------------------------------------
 
 type TI a = ExceptT Error (State Int) a
 

From e96e679acbf804928585393c87c58f5778537be1 Mon Sep 17 00:00:00 2001
From: "Viktor A. Rozenko Voitenko" <sharp.vik@gmail.com>
Date: Tue, 14 May 2024 13:31:21 +0300
Subject: [PATCH 4/8] refactor(Literal): instance Position

---
 src/Pure/Expr.hs         | 53 ++++++++++++++++++++++++----------------
 src/Pure/Parser.hs       | 16 ++++++------
 src/Pure/Typing/Infer.hs | 18 +++++++-------
 3 files changed, 49 insertions(+), 38 deletions(-)

diff --git a/src/Pure/Expr.hs b/src/Pure/Expr.hs
index 640cb69..a2d78eb 100644
--- a/src/Pure/Expr.hs
+++ b/src/Pure/Expr.hs
@@ -14,35 +14,46 @@ data Expr
   | When Expr [(Expr, Expr)] SourcePos
   | If Expr Expr Expr SourcePos
   | App Expr Expr SourcePos
-  | Literal Literal SourcePos
+  | Literal Literal
   deriving (Eq)
 
 data Literal
-  = List [Expr]
-  | Id Id
-  | Str String
-  | Float Double
-  | Int Integer
-  | Bool Bool
+  = List [Expr] SourcePos
+  | Id Id SourcePos
+  | Str String SourcePos
+  | Float Double SourcePos
+  | Int Integer SourcePos
+  | Bool Bool SourcePos
   deriving (Eq)
 
 -- POSITION --------------------------------------------------------------------
 
-positionOf :: Expr -> SourcePos
-positionOf (Lam _ _ pos) = pos
-positionOf (When _ _ pos) = pos
-positionOf (If _ _ _ pos) = pos
-positionOf (App _ _ pos) = pos
-positionOf (Literal _ pos) = pos
+class Position a where
+  positionOf :: a -> SourcePos
+
+instance Position Expr where
+  positionOf (Lam _ _ pos) = pos
+  positionOf (When _ _ pos) = pos
+  positionOf (If _ _ _ pos) = pos
+  positionOf (App _ _ pos) = pos
+  positionOf (Literal lit) = positionOf lit
+
+instance Position Literal where
+  positionOf (List _ pos) = pos
+  positionOf (Id _ pos) = pos
+  positionOf (Str _ pos) = pos
+  positionOf (Float _ pos) = pos
+  positionOf (Int _ pos) = pos
+  positionOf (Bool _ pos) = pos
 
 -- SHOW ------------------------------------------------------------------------
 
 instance Parens Expr where
-  parens l@(Literal _ _) = show l
+  parens l@(Literal _) = show l
   parens ex = parenthesised $ show ex
 
 instance Show Expr where
-  show (Literal literal _) = show literal
+  show (Literal literal) = show literal
   show (App f arg _) = show f +-+ parens arg
   show (If x y z _) = S.if_ +-+ show x +-+ S.then_ +-+ show y +-+ S.else_ +-+ show z
   show (Lam p ex _) = p +-+ S.arrow +-+ show ex
@@ -54,9 +65,9 @@ instance Show Expr where
         [S.bar] +-+ show pattern +-+ S.then_ +-+ show result
 
 instance Show Literal where
-  show (Bool bool) = show bool
-  show (Int int) = show int
-  show (Float number) = show number
-  show (Str str) = show str
-  show (Id ident) = ident
-  show (List l) = list (map show l)
\ No newline at end of file
+  show (Bool bool _) = show bool
+  show (Int int _) = show int
+  show (Float number _) = show number
+  show (Str str _) = show str
+  show (Id ident _) = ident
+  show (List l _) = list (map show l)
\ No newline at end of file
diff --git a/src/Pure/Parser.hs b/src/Pure/Parser.hs
index b213440..e1c0aa5 100644
--- a/src/Pure/Parser.hs
+++ b/src/Pure/Parser.hs
@@ -309,45 +309,45 @@ listP :: Parser Expr
 listP = do
   pos <- sourcePos
   list <- brackets parser $ commaSep1 parser exprP
-  return $ Literal (List list) pos
+  return $ Literal $ List list pos
 
 qualifiedP :: Parser Expr
 qualifiedP = do
   pos <- sourcePos
   qual <- sepBy1 nameP (char S.dot) <&> intercalate [S.dot]
-  return $ Literal (Id qual) pos
+  return $ Literal $ Id qual pos
 
 idP :: Parser Expr
 idP = do
   pos <- sourcePos
   name <- nameP
-  return $ Literal (Id name) pos
+  return $ Literal $ Id name pos
 
 strP :: Parser Expr
 strP = do
   pos <- sourcePos
   str <- stringLiteral parser
-  return $ Literal (Str str) pos
+  return $ Literal $ Str str pos
 
 floatP :: Parser Expr
 floatP = do
   pos <- sourcePos
   sign <- optionMaybe $ char S.minus
   number <- float parser
-  let flt = Float (if isJust sign then -number else number)
-  return $ Literal flt pos
+  let flt = Float (if isJust sign then -number else number) pos
+  return $ Literal flt
 
 intP :: Parser Expr
 intP = do
   pos <- sourcePos
   int <- integer parser
-  return $ Literal (Int int) pos
+  return $ Literal $ Int int pos
 
 boolP :: Parser Expr
 boolP = do
   pos <- sourcePos
   b <- symbolP S.true <|> symbolP S.false
-  return $ Literal (Bool (read b)) pos
+  return $ Literal $ Bool (read b) pos
 
 reservedP :: String -> Parser ()
 reservedP = reserved parser
diff --git a/src/Pure/Typing/Infer.hs b/src/Pure/Typing/Infer.hs
index a11d048..3d334eb 100644
--- a/src/Pure/Typing/Infer.hs
+++ b/src/Pure/Typing/Infer.hs
@@ -71,23 +71,23 @@ class Infer a where
   infer :: Context -> a -> TI (Subst, Type)
 
 instance Infer Literal where
-  infer _ (Bool _) = return (Env.empty, tBool)
-  infer _ (Int _) = return (Env.empty, tInt)
-  infer _ (Float _) = return (Env.empty, tFloat)
-  infer _ (Str _) = return (Env.empty, tStr)
-  infer ctx (Id i) =
+  infer _ (Bool _ _) = return (Env.empty, tBool)
+  infer _ (Int _ _) = return (Env.empty, tInt)
+  infer _ (Float _ _) = return (Env.empty, tFloat)
+  infer _ (Str _ _) = return (Env.empty, tStr)
+  infer ctx (Id i _) =
     case Env.typeOf i ctx of
       Nothing -> throwUnboundVariableError i
       Just scheme -> instantiate scheme <&> (,) Env.empty
-  infer _ (List []) = var <&> (,) Env.empty
-  infer ctx (List (x : xs)) = do
+  infer _ (List [] _) = var <&> (,) Env.empty
+  infer ctx (List (x : xs) pos) = do
     (s1, tx) <- infer ctx x
-    (s2, txs) <- infer (s1 +-> ctx) (List xs)
+    (s2, txs) <- infer (s1 +-> ctx) (List xs pos)
     s3 <- unify (tList tx) txs
     return (s3 <:> s2 <:> s1, s3 +-> txs)
 
 instance Infer Expr where
-  infer ctx (Literal literal _) = infer ctx literal
+  infer ctx (Literal literal) = infer ctx literal
   infer ctx (App fun arg _) = do
     (s1, tyFun) <- infer ctx fun
     (s2, tyArg) <- infer (s1 +-> ctx) arg

From 43710527537d2f46a33472a53f78f0b49208c55e Mon Sep 17 00:00:00 2001
From: "Viktor A. Rozenko Voitenko" <sharp.vik@gmail.com>
Date: Tue, 14 May 2024 13:41:10 +0300
Subject: [PATCH 5/8] refactor(When): has a Literal

---
 src/Pure/Expr.hs   |  2 +-
 src/Pure/Parser.hs | 41 +++++++++++++++++++++--------------------
 2 files changed, 22 insertions(+), 21 deletions(-)

diff --git a/src/Pure/Expr.hs b/src/Pure/Expr.hs
index a2d78eb..13e8859 100644
--- a/src/Pure/Expr.hs
+++ b/src/Pure/Expr.hs
@@ -11,7 +11,7 @@ import Utility.Strings (Parens (..), list, parenthesised, (+-+))
 
 data Expr
   = Lam Id Expr SourcePos
-  | When Expr [(Expr, Expr)] SourcePos
+  | When Expr [(Literal, Expr)] SourcePos
   | If Expr Expr Expr SourcePos
   | App Expr Expr SourcePos
   | Literal Literal
diff --git a/src/Pure/Parser.hs b/src/Pure/Parser.hs
index e1c0aa5..98f13e5 100644
--- a/src/Pure/Parser.hs
+++ b/src/Pure/Parser.hs
@@ -260,7 +260,7 @@ whenP = do
   where
     barP = reservedOp parser [S.bar]
     branchP = do
-      pat <- literalP <* reservedP S.then_
+      pat <- litP <* reservedP S.then_
       result <- exprP
       return (pat, result)
 
@@ -292,12 +292,14 @@ appP = do
     go f x = App f x (positionOf f)
 
 callerP :: Parser Expr
-callerP = parensP exprP <|> try qualifiedP <|> idP
+callerP = parensP exprP <|> try (qualifiedP <&> Literal) <|> (idP <&> Literal)
 
 literalP :: Parser Expr
-literalP =
-  parensP exprP
-    <|> listP
+literalP = parensP exprP <|> (litP <&> Literal)
+
+litP :: Parser Literal
+litP =
+  listP
     <|> strP
     <|> try boolP
     <|> try qualifiedP
@@ -305,49 +307,48 @@ literalP =
     <|> try floatP
     <|> intP
 
-listP :: Parser Expr
+listP :: Parser Literal
 listP = do
   pos <- sourcePos
   list <- brackets parser $ commaSep1 parser exprP
-  return $ Literal $ List list pos
+  return $ List list pos
 
-qualifiedP :: Parser Expr
+qualifiedP :: Parser Literal
 qualifiedP = do
   pos <- sourcePos
   qual <- sepBy1 nameP (char S.dot) <&> intercalate [S.dot]
-  return $ Literal $ Id qual pos
+  return $ Id qual pos
 
-idP :: Parser Expr
+idP :: Parser Literal
 idP = do
   pos <- sourcePos
   name <- nameP
-  return $ Literal $ Id name pos
+  return $ Id name pos
 
-strP :: Parser Expr
+strP :: Parser Literal
 strP = do
   pos <- sourcePos
   str <- stringLiteral parser
-  return $ Literal $ Str str pos
+  return $ Str str pos
 
-floatP :: Parser Expr
+floatP :: Parser Literal
 floatP = do
   pos <- sourcePos
   sign <- optionMaybe $ char S.minus
   number <- float parser
-  let flt = Float (if isJust sign then -number else number) pos
-  return $ Literal flt
+  return $ Float (if isJust sign then -number else number) pos
 
-intP :: Parser Expr
+intP :: Parser Literal
 intP = do
   pos <- sourcePos
   int <- integer parser
-  return $ Literal $ Int int pos
+  return $ Int int pos
 
-boolP :: Parser Expr
+boolP :: Parser Literal
 boolP = do
   pos <- sourcePos
   b <- symbolP S.true <|> symbolP S.false
-  return $ Literal $ Bool (read b) pos
+  return $ Bool (read b) pos
 
 reservedP :: String -> Parser ()
 reservedP = reserved parser

From 762e0078acf84788a92146f84399ebce609e70f2 Mon Sep 17 00:00:00 2001
From: "Viktor A. Rozenko Voitenko" <sharp.vik@gmail.com>
Date: Tue, 14 May 2024 14:48:46 +0300
Subject: [PATCH 6/8] minimize the language

---
 src/Pure/Expr.hs         | 27 +++++++++++++-------------
 src/Pure/Parser.hs       | 41 ++++++++++++++++++++--------------------
 src/Pure/Typing/Infer.hs | 13 +++++++------
 3 files changed, 40 insertions(+), 41 deletions(-)

diff --git a/src/Pure/Expr.hs b/src/Pure/Expr.hs
index 13e8859..829f78c 100644
--- a/src/Pure/Expr.hs
+++ b/src/Pure/Expr.hs
@@ -11,15 +11,15 @@ import Utility.Strings (Parens (..), list, parenthesised, (+-+))
 
 data Expr
   = Lam Id Expr SourcePos
-  | When Expr [(Literal, Expr)] SourcePos
-  | If Expr Expr Expr SourcePos
+  | -- | When Expr [(Literal, Expr)] SourcePos
+    If Expr Expr Expr SourcePos
   | App Expr Expr SourcePos
   | Literal Literal
   deriving (Eq)
 
 data Literal
-  = List [Expr] SourcePos
-  | Id Id SourcePos
+  = -- = List [Expr] SourcePos
+    Id Id SourcePos
   | Str String SourcePos
   | Float Double SourcePos
   | Int Integer SourcePos
@@ -33,13 +33,12 @@ class Position a where
 
 instance Position Expr where
   positionOf (Lam _ _ pos) = pos
-  positionOf (When _ _ pos) = pos
+  -- positionOf (When _ _ pos) = pos
   positionOf (If _ _ _ pos) = pos
   positionOf (App _ _ pos) = pos
   positionOf (Literal lit) = positionOf lit
 
 instance Position Literal where
-  positionOf (List _ pos) = pos
   positionOf (Id _ pos) = pos
   positionOf (Str _ pos) = pos
   positionOf (Float _ pos) = pos
@@ -57,17 +56,17 @@ instance Show Expr where
   show (App f arg _) = show f +-+ parens arg
   show (If x y z _) = S.if_ +-+ show x +-+ S.then_ +-+ show y +-+ S.else_ +-+ show z
   show (Lam p ex _) = p +-+ S.arrow +-+ show ex
-  show (When _ [] _) = undefined
-  show (When e branches _) =
-    S.when +-+ show e +-+ S.is +-+ unwords (map showBranch branches)
-    where
-      showBranch (pattern, result) =
-        [S.bar] +-+ show pattern +-+ S.then_ +-+ show result
+
+-- show (When _ [] _) = undefined
+-- show (When e branches _) =
+--   S.when +-+ show e +-+ S.is +-+ unwords (map showBranch branches)
+--   where
+--     showBranch (pattern, result) =
+--       [S.bar] +-+ show pattern +-+ S.then_ +-+ show result
 
 instance Show Literal where
   show (Bool bool _) = show bool
   show (Int int _) = show int
   show (Float number _) = show number
   show (Str str _) = show str
-  show (Id ident _) = ident
-  show (List l _) = list (map show l)
\ No newline at end of file
+  show (Id ident _) = ident
\ No newline at end of file
diff --git a/src/Pure/Parser.hs b/src/Pure/Parser.hs
index 98f13e5..f5662e1 100644
--- a/src/Pure/Parser.hs
+++ b/src/Pure/Parser.hs
@@ -244,25 +244,25 @@ defP = do
 
 exprP :: Parser Expr
 exprP =
-  try whenP
-    <|> try ifP
+  -- try whenP
+  try ifP
     <|> try lambdaP
     <|> try appP
     <|> literalP
     <?> "an expression"
 
-whenP :: Parser Expr
-whenP = do
-  pos <- sourcePos
-  e <- between (reservedP S.when) (reservedP S.is) notIfP
-  brs <- barP >> sepBy1 branchP barP
-  return $ When e brs pos
-  where
-    barP = reservedOp parser [S.bar]
-    branchP = do
-      pat <- litP <* reservedP S.then_
-      result <- exprP
-      return (pat, result)
+-- whenP :: Parser Expr
+-- whenP = do
+--   pos <- sourcePos
+--   e <- between (reservedP S.when) (reservedP S.is) notIfP
+--   brs <- barP >> sepBy1 branchP barP
+--   return $ When e brs pos
+--   where
+--     barP = reservedOp parser [S.bar]
+--     branchP = do
+--       pat <- litP <* reservedP S.then_
+--       result <- exprP
+--       return (pat, result)
 
 ifP :: Parser Expr
 ifP = do
@@ -299,19 +299,18 @@ literalP = parensP exprP <|> (litP <&> Literal)
 
 litP :: Parser Literal
 litP =
-  listP
-    <|> strP
+  strP
     <|> try boolP
     <|> try qualifiedP
     <|> try idP
     <|> try floatP
     <|> intP
 
-listP :: Parser Literal
-listP = do
-  pos <- sourcePos
-  list <- brackets parser $ commaSep1 parser exprP
-  return $ List list pos
+-- listP :: Parser Literal
+-- listP = do
+--   pos <- sourcePos
+--   list <- brackets parser $ commaSep1 parser exprP
+--   return $ List list pos
 
 qualifiedP :: Parser Literal
 qualifiedP = do
diff --git a/src/Pure/Typing/Infer.hs b/src/Pure/Typing/Infer.hs
index 3d334eb..8315e3a 100644
--- a/src/Pure/Typing/Infer.hs
+++ b/src/Pure/Typing/Infer.hs
@@ -79,12 +79,13 @@ instance Infer Literal where
     case Env.typeOf i ctx of
       Nothing -> throwUnboundVariableError i
       Just scheme -> instantiate scheme <&> (,) Env.empty
-  infer _ (List [] _) = var <&> (,) Env.empty
-  infer ctx (List (x : xs) pos) = do
-    (s1, tx) <- infer ctx x
-    (s2, txs) <- infer (s1 +-> ctx) (List xs pos)
-    s3 <- unify (tList tx) txs
-    return (s3 <:> s2 <:> s1, s3 +-> txs)
+
+-- infer _ (List [] _) = var <&> (,) Env.empty
+-- infer ctx (List (x : xs) pos) = do
+--   (s1, tx) <- infer ctx x
+--   (s2, txs) <- infer (s1 +-> ctx) (List xs pos)
+--   s3 <- unify (tList tx) txs
+--   return (s3 <:> s2 <:> s1, s3 +-> txs)
 
 instance Infer Expr where
   infer ctx (Literal literal) = infer ctx literal

From a5f8d5427324dc579eda831cce061d87ea7f6df4 Mon Sep 17 00:00:00 2001
From: "Viktor A. Rozenko Voitenko" <sharp.vik@gmail.com>
Date: Tue, 14 May 2024 22:35:15 +0300
Subject: [PATCH 7/8] feat(XLam): type check destructuring lambdas

---
 src/Pure/Expr.hs         |  65 +++++++++++++++---------
 src/Pure/Parser.hs       |  24 ++++-----
 src/Pure/Typing/Env.hs   |  13 +++++
 src/Pure/Typing/Infer.hs | 104 ++++++++++++++++++++++-----------------
 4 files changed, 124 insertions(+), 82 deletions(-)

diff --git a/src/Pure/Expr.hs b/src/Pure/Expr.hs
index 829f78c..c69b152 100644
--- a/src/Pure/Expr.hs
+++ b/src/Pure/Expr.hs
@@ -1,31 +1,49 @@
 {-# LANGUAGE FlexibleInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
 
-module Pure.Expr (Expr (..), Literal (..), positionOf) where
+module Pure.Expr (Expr (..), positionOf) where
 
+import Data.Char (isUpperCase)
+import Data.Set (Set)
+import qualified Data.Set as Set
 import qualified Pure.Sacred as S
+import Pure.Typing.Free (Free (..))
 import Text.Parsec (SourcePos)
 import Utility.Common (Id)
-import Utility.Strings (Parens (..), list, parenthesised, (+-+))
+import Utility.Strings (Parens (..), parenthesised, (+-+))
 
 -- EXPRESSION ------------------------------------------------------------------
 
 data Expr
   = Lam Id Expr SourcePos
-  | -- | When Expr [(Literal, Expr)] SourcePos
-    If Expr Expr Expr SourcePos
+  | XLam Expr Expr SourcePos
+  | If Expr Expr Expr SourcePos
   | App Expr Expr SourcePos
-  | Literal Literal
-  deriving (Eq)
-
-data Literal
-  = -- = List [Expr] SourcePos
-    Id Id SourcePos
+  | Id Id SourcePos
   | Str String SourcePos
   | Float Double SourcePos
   | Int Integer SourcePos
   | Bool Bool SourcePos
+  -- \| When Expr [(Literal, Expr)] SourcePos
   deriving (Eq)
 
+-- FREE ------------------------------------------------------------------------
+
+instance Free Expr where
+  free (Lam i e _) = Set.union (freeVar i) (free e)
+  free (XLam e1 e2 _) = Set.unions $ map free [e1, e2]
+  free (If e1 e2 e3 _) = Set.unions $ map free [e1, e2, e3]
+  free (App e1 e2 _) = Set.unions $ map free [e1, e2]
+  free (Id i _) = freeVar i
+  free _ = Set.empty
+
+freeVar :: Id -> Set Id
+freeVar i@(l : _) =
+  if l == S.underscore || isUpperCase l
+    then Set.empty
+    else Set.singleton i
+freeVar "" = undefined
+
 -- POSITION --------------------------------------------------------------------
 
 class Position a where
@@ -33,12 +51,9 @@ class Position a where
 
 instance Position Expr where
   positionOf (Lam _ _ pos) = pos
-  -- positionOf (When _ _ pos) = pos
+  positionOf (XLam _ _ pos) = pos
   positionOf (If _ _ _ pos) = pos
   positionOf (App _ _ pos) = pos
-  positionOf (Literal lit) = positionOf lit
-
-instance Position Literal where
   positionOf (Id _ pos) = pos
   positionOf (Str _ pos) = pos
   positionOf (Float _ pos) = pos
@@ -48,14 +63,23 @@ instance Position Literal where
 -- SHOW ------------------------------------------------------------------------
 
 instance Parens Expr where
-  parens l@(Literal _) = show l
+  parens literal@(Id _ _) = show literal
+  parens literal@(Str _ _) = show literal
+  parens literal@(Float _ _) = show literal
+  parens literal@(Int _ _) = show literal
+  parens literal@(Bool _ _) = show literal
   parens ex = parenthesised $ show ex
 
 instance Show Expr where
-  show (Literal literal) = show literal
+  show (Id i _) = i
+  show (Str str _) = show str
+  show (Float f _) = show f
+  show (Int int _) = show int
+  show (Bool bool _) = show bool
   show (App f arg _) = show f +-+ parens arg
   show (If x y z _) = S.if_ +-+ show x +-+ S.then_ +-+ show y +-+ S.else_ +-+ show z
-  show (Lam p ex _) = p +-+ S.arrow +-+ show ex
+  show (Lam from to _) = from +-+ S.arrow +-+ show to
+  show (XLam from to _) = parens from +-+ S.arrow +-+ show to
 
 -- show (When _ [] _) = undefined
 -- show (When e branches _) =
@@ -63,10 +87,3 @@ instance Show Expr where
 --   where
 --     showBranch (pattern, result) =
 --       [S.bar] +-+ show pattern +-+ S.then_ +-+ show result
-
-instance Show Literal where
-  show (Bool bool _) = show bool
-  show (Int int _) = show int
-  show (Float number _) = show number
-  show (Str str _) = show str
-  show (Id ident _) = ident
\ No newline at end of file
diff --git a/src/Pure/Parser.hs b/src/Pure/Parser.hs
index f5662e1..d81d216 100644
--- a/src/Pure/Parser.hs
+++ b/src/Pure/Parser.hs
@@ -20,7 +20,7 @@ import Data.Char (isLowerCase, isUpperCase)
 import Data.Functor ((<&>))
 import Data.List (intercalate)
 import Data.Maybe (isJust, mapMaybe)
-import Pure.Expr (Expr (..), Literal (..), positionOf)
+import Pure.Expr (Expr (..), positionOf)
 import qualified Pure.Sacred as S
 import Pure.Typing.Type (Type (..))
 import Text.Parsec
@@ -279,7 +279,7 @@ notIfP = try lambdaP <|> try appP <|> literalP <?> "a condition"
 lambdaP :: Parser Expr
 lambdaP = do
   pos <- sourcePos
-  param <- nameP <* reservedOp parser S.arrow <?> "a named parameter"
+  param <- lowerNameP <* reservedOp parser S.arrow <?> "a named parameter"
   expr <- exprP
   return $ Lam param expr pos
 
@@ -292,12 +292,12 @@ appP = do
     go f x = App f x (positionOf f)
 
 callerP :: Parser Expr
-callerP = parensP exprP <|> try (qualifiedP <&> Literal) <|> (idP <&> Literal)
+callerP = parensP exprP <|> try qualifiedP <|> idP
 
 literalP :: Parser Expr
-literalP = parensP exprP <|> (litP <&> Literal)
+literalP = parensP exprP <|> litP
 
-litP :: Parser Literal
+litP :: Parser Expr
 litP =
   strP
     <|> try boolP
@@ -306,44 +306,44 @@ litP =
     <|> try floatP
     <|> intP
 
--- listP :: Parser Literal
+-- listP :: Parser Expr
 -- listP = do
 --   pos <- sourcePos
 --   list <- brackets parser $ commaSep1 parser exprP
 --   return $ List list pos
 
-qualifiedP :: Parser Literal
+qualifiedP :: Parser Expr
 qualifiedP = do
   pos <- sourcePos
   qual <- sepBy1 nameP (char S.dot) <&> intercalate [S.dot]
   return $ Id qual pos
 
-idP :: Parser Literal
+idP :: Parser Expr
 idP = do
   pos <- sourcePos
   name <- nameP
   return $ Id name pos
 
-strP :: Parser Literal
+strP :: Parser Expr
 strP = do
   pos <- sourcePos
   str <- stringLiteral parser
   return $ Str str pos
 
-floatP :: Parser Literal
+floatP :: Parser Expr
 floatP = do
   pos <- sourcePos
   sign <- optionMaybe $ char S.minus
   number <- float parser
   return $ Float (if isJust sign then -number else number) pos
 
-intP :: Parser Literal
+intP :: Parser Expr
 intP = do
   pos <- sourcePos
   int <- integer parser
   return $ Int int pos
 
-boolP :: Parser Literal
+boolP :: Parser Expr
 boolP = do
   pos <- sourcePos
   b <- symbolP S.true <|> symbolP S.false
diff --git a/src/Pure/Typing/Env.hs b/src/Pure/Typing/Env.hs
index 308e290..f902c6a 100644
--- a/src/Pure/Typing/Env.hs
+++ b/src/Pure/Typing/Env.hs
@@ -10,6 +10,7 @@ module Pure.Typing.Env
     member,
     bind,
     typeOf,
+    members,
     insert,
     Apply (..),
     (<:>),
@@ -19,8 +20,10 @@ where
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.Maybe (fromMaybe)
+import Data.Set (Set)
 import Pure.Typing.Type (Scheme (..), Type (..))
 import Utility.Common (Id)
+import Utility.Strings (li, (+\+))
 
 -- ENVIRONMENT -----------------------------------------------------------------
 
@@ -68,6 +71,9 @@ member k (Env m) = Map.member k m
 typeOf :: Id -> Env a -> Maybe a
 typeOf i (Env m) = Map.lookup i m
 
+members :: Env a -> Set Id
+members (Env m) = Map.keysSet m
+
 -- APPLY -----------------------------------------------------------------------
 
 class Apply a where
@@ -88,3 +94,10 @@ instance Apply Scheme where
 
 instance (Apply a) => Apply (Env a) where
   subst +-> ctx = fmap (subst +->) ctx
+
+-- SHOW ------------------------------------------------------------------------
+
+instance (Show a) => Show (Env a) where
+  show (Env m) = "{" +\+ unlines (map showPair $ Map.toList m) ++ "}"
+    where
+      showPair (k, v) = li k ++ ": " ++ show v
\ No newline at end of file
diff --git a/src/Pure/Typing/Infer.hs b/src/Pure/Typing/Infer.hs
index 8315e3a..b1e7c8e 100644
--- a/src/Pure/Typing/Infer.hs
+++ b/src/Pure/Typing/Infer.hs
@@ -14,8 +14,9 @@ where
 import Control.Monad.Except (ExceptT, runExceptT, throwError, withError)
 import Control.Monad.State (State, evalState, get, put, runState)
 import Data.Functor ((<&>))
+import Data.Set ((\\))
 import qualified Data.Set as Set
-import Pure.Expr (Expr (..), Literal (..))
+import Pure.Expr (Expr (..))
 import Pure.Typing.Env (Apply (..), Context, Subst, (<:>))
 import qualified Pure.Typing.Env as Env
 import Pure.Typing.Error (Error (..))
@@ -67,48 +68,44 @@ assert' ctx hint expr = do
   s2 <- unify tyHint tyExpr
   return $ generalize ctx (s2 <:> s1 +-> tyHint)
 
-class Infer a where
-  infer :: Context -> a -> TI (Subst, Type)
-
-instance Infer Literal where
-  infer _ (Bool _ _) = return (Env.empty, tBool)
-  infer _ (Int _ _) = return (Env.empty, tInt)
-  infer _ (Float _ _) = return (Env.empty, tFloat)
-  infer _ (Str _ _) = return (Env.empty, tStr)
-  infer ctx (Id i _) =
-    case Env.typeOf i ctx of
-      Nothing -> throwUnboundVariableError i
-      Just scheme -> instantiate scheme <&> (,) Env.empty
-
--- infer _ (List [] _) = var <&> (,) Env.empty
--- infer ctx (List (x : xs) pos) = do
---   (s1, tx) <- infer ctx x
---   (s2, txs) <- infer (s1 +-> ctx) (List xs pos)
---   s3 <- unify (tList tx) txs
---   return (s3 <:> s2 <:> s1, s3 +-> txs)
-
-instance Infer Expr where
-  infer ctx (Literal literal) = infer ctx literal
-  infer ctx (App fun arg _) = do
-    (s1, tyFun) <- infer ctx fun
-    (s2, tyArg) <- infer (s1 +-> ctx) arg
-    tyRes <- var
-    s3 <- unify (tyArg :-> tyRes) (s2 +-> tyFun)
-    return (s3 <:> s2 <:> s1, s3 +-> tyRes)
-  infer ctx (If condition e1 e2 _) = do
-    (s1, t1) <- infer ctx condition
-    (s2, t2) <- infer (s1 +-> ctx) e1
-    (s3, t3) <- infer (s2 <:> s1 +-> ctx) e2
-    s4 <- unify (s3 <:> s2 <:> s1 +-> t1) tBool
-    s5 <- unify (s4 <:> s3 <:> s2 <:> s1 +-> t2) t3
-    let s = s5 <:> s4 <:> s3 <:> s2 <:> s1
-    let t = s +-> t2
-    return (s, t)
-  infer ctx (Lam binder body _) = do
-    tyBinder <- var
-    let tmpCtx = Env.insert binder ([] :. tyBinder) ctx
-    (s1, tyBody) <- infer tmpCtx body
-    return (s1, (s1 +-> tyBinder) :-> tyBody)
+infer :: Context -> Expr -> TI (Subst, Type)
+infer _ (Bool _ _) = return (Env.empty, tBool)
+infer _ (Int _ _) = return (Env.empty, tInt)
+infer _ (Float _ _) = return (Env.empty, tFloat)
+infer _ (Str _ _) = return (Env.empty, tStr)
+infer ctx (Id i _) =
+  case Env.typeOf i ctx of
+    Nothing -> throwUnboundVariableError i
+    Just scheme -> instantiate scheme <&> (,) Env.empty
+infer ctx (App fun arg _) = do
+  (s1, tyFun) <- infer ctx fun
+  (s2, tyArg) <- infer (s1 +-> ctx) arg
+  tyRes <- var
+  s3 <- unify (tyArg :-> tyRes) (s2 +-> tyFun)
+  return (s3 <:> s2 <:> s1, s3 +-> tyRes)
+infer ctx (If condition e1 e2 _) = do
+  (s1, t1) <- infer ctx condition
+  (s2, t2) <- infer (s1 +-> ctx) e1
+  (s3, t3) <- infer (s2 <:> s1 +-> ctx) e2
+  s4 <- unify (s3 <:> s2 <:> s1 +-> t1) tBool
+  s5 <- unify (s4 <:> s3 <:> s2 <:> s1 +-> t2) t3
+  let s = s5 <:> s4 <:> s3 <:> s2 <:> s1
+  let t = s +-> t2
+  return (s, t)
+infer ctx (Lam binder body _) = do
+  tyBinder <- var
+  let ctx1 = Env.insert binder ([] :. tyBinder) ctx
+  (s, tyBody) <- infer ctx1 body
+  return (s, (s +-> tyBinder) :-> tyBody)
+infer ctx (XLam pattern body _) = do
+  let fvs = Set.toList $ free pattern \\ Env.members ctx
+  tys <- mapM (const var) fvs
+  let vts = zip fvs tys
+  let ctx1 = foldl (\ctx' (v, t) -> Env.insert v ([] :. t) ctx') ctx vts
+  (s1, tyPat) <- infer ctx1 pattern
+  (s2, tyBody) <- infer (s1 +-> ctx1) body
+  let s = s2 <:> s1
+  return (s, (s +-> tyPat) :-> tyBody)
 
 -- HELPERS ---------------------------------------------------------------------
 
@@ -153,7 +150,7 @@ varBind v ty
   | otherwise = return $ Env.bind v ty
 
 generalize :: Context -> Type -> Scheme
-generalize ctx t = Set.toList (Set.difference (free t) (free ctx)) :. t
+generalize ctx t = Set.toList (free t \\ free ctx) :. t
 
 instantiate :: Scheme -> TI Type
 instantiate (vars :. ty) = do
@@ -190,6 +187,21 @@ primitives =
     [ ("id", ["a"] :. Var "a" :-> Var "a"),
       ("always", ["a", "b"] :. Var "a" :-> Var "b" :-> Var "a"),
       ("(+)", [] :. tInt :-> tInt :-> tInt),
-      ("(:)", ["a"] :. Var "a" :-> tList (Var "a") :-> tList (Var "a")),
-      ("null", ["a"] :. tList (Var "a"))
+      ("Cons", ["a"] :. Var "a" :-> tList (Var "a") :-> tList (Var "a")),
+      ("Null", ["a"] :. tList (Var "a"))
     ]
+
+-- pos = initialPos "main.pure"
+-- testTI $
+--   XLam
+--     ( App
+--         (App (Literal $ Id "Cons" pos) (Literal $ Id "x" pos) pos)
+--         (Literal $ Id "xs" pos)
+--         pos
+--     )
+--     ( App
+--         (App (Literal $ Id "(+)" pos) (Literal $ Id "x" pos) pos)
+--         (Literal $ Int 1 pos)
+--         pos
+--     )
+--     pos
\ No newline at end of file

From 5304b7d45424937705f9c617cfbaf283968545a0 Mon Sep 17 00:00:00 2001
From: "Viktor A. Rozenko Voitenko" <sharp.vik@gmail.com>
Date: Fri, 17 May 2024 20:00:42 +0300
Subject: [PATCH 8/8] fix(Infer): remove pattern vars from env

---
 src/Pure/Expr.hs         | 12 ++++--------
 src/Pure/Typing/Env.hs   | 12 ++++++++++++
 src/Pure/Typing/Infer.hs | 30 ++++++++++++++++++++++++------
 3 files changed, 40 insertions(+), 14 deletions(-)

diff --git a/src/Pure/Expr.hs b/src/Pure/Expr.hs
index c69b152..92ba1cf 100644
--- a/src/Pure/Expr.hs
+++ b/src/Pure/Expr.hs
@@ -24,7 +24,8 @@ data Expr
   | Float Double SourcePos
   | Int Integer SourcePos
   | Bool Bool SourcePos
-  -- \| When Expr [(Literal, Expr)] SourcePos
+  | --         XLam
+    When Expr [Expr] SourcePos
   deriving (Eq)
 
 -- FREE ------------------------------------------------------------------------
@@ -51,6 +52,7 @@ class Position a where
 
 instance Position Expr where
   positionOf (Lam _ _ pos) = pos
+  positionOf (When _ _ pos) = pos
   positionOf (XLam _ _ pos) = pos
   positionOf (If _ _ _ pos) = pos
   positionOf (App _ _ pos) = pos
@@ -80,10 +82,4 @@ instance Show Expr where
   show (If x y z _) = S.if_ +-+ show x +-+ S.then_ +-+ show y +-+ S.else_ +-+ show z
   show (Lam from to _) = from +-+ S.arrow +-+ show to
   show (XLam from to _) = parens from +-+ S.arrow +-+ show to
-
--- show (When _ [] _) = undefined
--- show (When e branches _) =
---   S.when +-+ show e +-+ S.is +-+ unwords (map showBranch branches)
---   where
---     showBranch (pattern, result) =
---       [S.bar] +-+ show pattern +-+ S.then_ +-+ show result
+  show (When x opts _) = S.when +-+ show x +-+ S.is +-+ unwords (map show opts)
diff --git a/src/Pure/Typing/Env.hs b/src/Pure/Typing/Env.hs
index f902c6a..5dc5599 100644
--- a/src/Pure/Typing/Env.hs
+++ b/src/Pure/Typing/Env.hs
@@ -12,6 +12,9 @@ module Pure.Typing.Env
     typeOf,
     members,
     insert,
+    delete,
+    without,
+    unions,
     Apply (..),
     (<:>),
   )
@@ -58,11 +61,20 @@ bind k = Env . Map.singleton k
 s1@(Env m1) <:> (Env m2) = Env $ Map.union (Map.map (s1 +->) m2) m1
 -- ^ The union is left biased.
 
+unions :: (Foldable t) => t (Env Type) -> Env Type
+unions = foldl (<:>) empty
+
 -- UPDATE ----------------------------------------------------------------------
 
 insert :: Id -> a -> Env a -> Env a
 insert i a (Env m) = Env $ Map.insert i a m
 
+delete :: Id -> Env a -> Env a
+delete i (Env m) = Env $ Map.delete i m
+
+without :: (Foldable t) => t Id -> Env a -> Env a
+without is env = foldr delete env is
+
 -- QUERY -----------------------------------------------------------------------
 
 member :: Id -> Env a -> Bool
diff --git a/src/Pure/Typing/Infer.hs b/src/Pure/Typing/Infer.hs
index b1e7c8e..207dfb9 100644
--- a/src/Pure/Typing/Infer.hs
+++ b/src/Pure/Typing/Infer.hs
@@ -11,6 +11,7 @@ module Pure.Typing.Infer
   )
 where
 
+import Control.Monad (mapAndUnzipM)
 import Control.Monad.Except (ExceptT, runExceptT, throwError, withError)
 import Control.Monad.State (State, evalState, get, put, runState)
 import Data.Functor ((<&>))
@@ -80,9 +81,9 @@ infer ctx (Id i _) =
 infer ctx (App fun arg _) = do
   (s1, tyFun) <- infer ctx fun
   (s2, tyArg) <- infer (s1 +-> ctx) arg
-  tyRes <- var
-  s3 <- unify (tyArg :-> tyRes) (s2 +-> tyFun)
-  return (s3 <:> s2 <:> s1, s3 +-> tyRes)
+  tyResult <- var
+  s3 <- unify (tyArg :-> tyResult) (s2 +-> tyFun)
+  return (s3 <:> s2 <:> s1, s3 +-> tyResult)
 infer ctx (If condition e1 e2 _) = do
   (s1, t1) <- infer ctx condition
   (s2, t2) <- infer (s1 +-> ctx) e1
@@ -99,16 +100,33 @@ infer ctx (Lam binder body _) = do
   return (s, (s +-> tyBinder) :-> tyBody)
 infer ctx (XLam pattern body _) = do
   let fvs = Set.toList $ free pattern \\ Env.members ctx
-  tys <- mapM (const var) fvs
-  let vts = zip fvs tys
+  vts <- mapM (const var) fvs <&> zip fvs
   let ctx1 = foldl (\ctx' (v, t) -> Env.insert v ([] :. t) ctx') ctx vts
   (s1, tyPat) <- infer ctx1 pattern
   (s2, tyBody) <- infer (s1 +-> ctx1) body
-  let s = s2 <:> s1
+  let s = Env.without fvs (s2 <:> s1)
+  -- !    ^^^^^^^^^^^^^^^
+  -- ? Deleting these because patterns of the same `when` expression may
+  -- ? redeclare variables.
   return (s, (s +-> tyPat) :-> tyBody)
+infer ctx (When x opts _) = do
+  (s1, tyCorpse) <- infer ctx x
+  (s2, tyOpts) <- mapAndUnzipM (infer $ s1 +-> ctx) opts
+  tyResult <- var
+  s3 <- unifyList $ (tyCorpse :-> tyResult) : tyOpts
+  let s = s3 <:> Env.unions s2 <:> s1
+  return (s, s +-> tyResult)
 
 -- HELPERS ---------------------------------------------------------------------
 
+unifyList :: [Type] -> TI Subst
+unifyList [] = return Env.empty
+unifyList [_] = return Env.empty
+unifyList (t : r : ts) = do
+  s1 <- unify t r
+  s2 <- unifyList ts
+  return $ s2 <:> s1
+
 unify :: Type -> Type -> TI Subst
 unify (Var u) t = varBind u t
 unify t (Var u) = varBind u t