From ebf093525eb22d2cb5ec7f1cd58441fd65967994 Mon Sep 17 00:00:00 2001
From: James Martin <james@jtmar.me>
Date: Mon, 22 Mar 2021 17:34:51 -0700
Subject: [PATCH] Replace `fix` builtin with `letrec` syntax.

---
 README.md                            | 11 +++++-----
 app/Main.hs                          |  5 +++--
 examples.lc                          | 32 ++++++++++++++++++++++------
 package.yaml                         |  3 +++
 src/LambdaCalculus/Expression.hs     |  3 ++-
 src/LambdaCalculus/Syntax/Base.hs    | 21 ++++++++++++------
 src/LambdaCalculus/Syntax/Parser.hs  | 22 +++++++++++++------
 src/LambdaCalculus/Syntax/Printer.hs | 10 ++++-----
 8 files changed, 74 insertions(+), 33 deletions(-)

diff --git a/README.md b/README.md
index 6c36dcb..1d72a0f 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Lambda Calculus
 This is a simple programming language derived from lambda calculus,
-using the Hindley-Milner type system, plus some builtin types, `fix`, and `callcc`
+using the Hindley-Milner type system, plus `letrec` and `callcc`.
 
 ## Usage
 Run the program using `stack run` (or run the tests with `stack test`).
@@ -34,11 +34,13 @@ The parser's error messages currently are virtually useless, so be very careful
 * Function application: `f x y`
 * Lambda abstraction: `\x y z. E` or `λx y z. E`
 * Let expressions: `let x = E; y = F in G`
+  * Or letrec expressions, which can only define variable,
+    but which can be self-referential: `letrec x = ... x ... in E`
 * Parenthetical expressions: `(E)`
 * Constructors: `()`, `(x, y)` (or `(,) x y`), `Left x`, `Right y`, `Z`, `S`, `[]`, `(x :: xs)` (or `(:) x xs`), `Char n`.
   * The parentheses around the cons constructor are not optional.
   * `Char` takes a natural number and turns it into a character.
-* Pattern matchers: `case { Left a -> e ; Right y -> f }`
+* Pattern matchers: `{ Left a -> e ; Right y -> f }`
   * Pattern matchers can be applied like functions, e.g. `{ Z -> x, S -> y } 10` reduces to `y`.
   * Patterns must use the regular form of the constructor, e.g. `(x :: xs)` and not `((::) x xs)`.
   * There are no nested patterns or default patterns.
@@ -49,9 +51,9 @@ The parser's error messages currently are virtually useless, so be very careful
 * Comments: `// line comment`, `/* block comment */`
 
 Top-level contexts (e.g. the REPL or a source code file)
-allow declarations (`let` expressions without `in ...`),
+allow declarations (`let(rec) x = E` without multiple definitions `in ...`),
 which make your definitions available for the rest of the program's execution.
-You may separate multiple declarations and expressions with `;`.
+You must separate your declarations and expressions with `;`.
 
 ## Types
 Types are checked/inferred using the Hindley-Milner type inference algorithm.
@@ -71,7 +73,6 @@ Builtins are variables that correspond with a built-in language feature
 that cannot be replicated by user-written code.
 They still are just variables though; they do not receive special syntactic treatment.
 
-* `fix : ∀a. ((a -> a) -> a)`: an alias for the strict fixpoint combinator that the typechecker can typecheck.
 * `callcc : ∀a b. (((a -> b) -> a) -> a)`: [the call-with-current-continuation control flow operator](https://en.wikipedia.org/wiki/Call-with-current-continuation).
 
 Continuations are printed as `λ!. ... ! ...`, like a lambda abstraction
diff --git a/app/Main.hs b/app/Main.hs
index e310b69..a2435d0 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,4 +1,3 @@
-{-# OPTIONS_GHC -Wno-unused-do-bind -Wno-monomorphism-restriction #-}
 module Main (main) where
 
 import LambdaCalculus
@@ -107,7 +106,9 @@ commandParser = do
     load = Load <$> do
       try $ string "load "
       spaces
-      many1 anyChar
+      filename <- many1 (noneOf " ")
+      spaces
+      pure filename
 
     clear = Clear <$ try (string "clear")
 
diff --git a/examples.lc b/examples.lc
index 3850d52..1045551 100644
--- a/examples.lc
+++ b/examples.lc
@@ -1,26 +1,44 @@
 // Create a list by iterating `f` `n` times:
-let iterate = fix \iterate f x. { Z -> [] ; S n -> (x :: iterate f (f x) n) };
+letrec iterate = \f x.
+    { Z   -> []
+    ; S n -> (x :: iterate f (f x) n)
+    };
+
 // Use the iterate function to count to 10:
-let countTo = iterate S 1 in countTo 10;
+let countTo = iterate S 1
+in countTo 10;
 
 // Append two lists together:
-let append = fix \append xs ys. { [] -> ys ; (x :: xs) -> (x :: append xs ys) } xs;
+letrec append = \xs ys.
+    { []        -> ys
+    ; (x :: xs) -> (x :: append xs ys)
+    } xs;
+
 // Reverse a list:
-let reverse = fix \reverse. { [] -> [] ; (x :: xs) -> append (reverse xs) [x] };
+letrec reverse =
+    { []         -> []
+    ; (x :: xs)  -> append (reverse xs) [x]
+    };
+
 // Now we can reverse `"reverse"`:
 reverse "reverse";
 
 // Calculating `3 + 2` with the help of Church-encoded numerals:
-let Sf = \n f x. f (n f x); plus = \x. x Sf in plus (\f x. f (f (f x))) (\f x. f (f x)) S Z;
+let Sf   = \n f x. f (n f x)
+  ; plus = \x. x Sf
+in plus (\f x. f (f (f x))) (\f x. f (f x)) S Z;
+
+letrec undefined = undefined;
 
 // This expression would loop forever, but `callcc` saves the day!
-S (callcc \k. (fix \x. x) (k Z));
+S (callcc \k. undefined (k Z));
 
 // And if it wasn't clear, this is what the `Char` constructor does:
 { Char c -> Char (S c) } 'a;
 // (it outputs `'b`)
 
-// Here are a few expressions which don't typecheck but are handy for debugging the evaluator:
+// Here are a few expressions which don't typecheck but are handy for debugging the evaluator
+// (you can run them using `:check off off`:
 /*
 let D = \x. x x; F = \f. f (f y) in D (F \x. x);
 // y y
diff --git a/package.yaml b/package.yaml
index 81a3489..c6e991b 100644
--- a/package.yaml
+++ b/package.yaml
@@ -71,6 +71,9 @@ executables:
     - -threaded
     - -rtsopts
     - -with-rtsopts=-N
+    - -Wno-missing-export-lists
+    - -Wno-monomorphism-restriction
+    - -Wno-unused-do-bind
     dependencies:
     - jtm-lambda-calculus
     - exceptions >= 0.10.4 && < 0.11
diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs
index 749f881..b2524fa 100644
--- a/src/LambdaCalculus/Expression.hs
+++ b/src/LambdaCalculus/Expression.hs
@@ -27,7 +27,7 @@ import Data.List.NonEmpty (toList)
 import Data.Text (unpack)
 
 builtins :: HashMap Text CheckExpr
-builtins = HM.fromList [("callcc", CallCCC), ("fix", FixC)]
+builtins = HM.fromList [("callcc", CallCCC)]
 
 -- | Convert from an abstract syntax tree to a typechecker expression.
 ast2check :: AST -> CheckExpr
@@ -38,6 +38,7 @@ ast2check = substitute builtins . cata \case
   LetF ds e ->
     let letExpr name val body' = App (Abs name body') val
     in foldr (uncurry letExpr) e $ getNonEmptyDefFs ds
+  LetRecFP (nx, ex) e -> App (Abs nx e) (App FixC (Abs nx ex))
   CtrF ctr es -> foldl' App (CtrC ctr) es
   CaseF ps -> Case ps
   PNatF n -> int2ast n
diff --git a/src/LambdaCalculus/Syntax/Base.hs b/src/LambdaCalculus/Syntax/Base.hs
index 18610e9..039b899 100644
--- a/src/LambdaCalculus/Syntax/Base.hs
+++ b/src/LambdaCalculus/Syntax/Base.hs
@@ -2,8 +2,9 @@ module LambdaCalculus.Syntax.Base
   ( Expr (..), ExprF (..), Ctr (..), Pat, Def, DefF (..), PatF (..), VoidF, Text, NonEmpty (..)
   , substitute, substitute1, rename, rename1, free, bound, used
   , Parse, AST, ASTF, ASTX, ASTXF (..), NonEmptyDefFs (..)
-  , pattern LetFP, pattern PNat, pattern PNatF, pattern PList, pattern PListF
-  , pattern PChar, pattern PCharF, pattern PStr, pattern PStrF, pattern HoleP, pattern HoleFP
+  , pattern LetFP, pattern LetRecP, pattern LetRecFP
+  , pattern PNat, pattern PNatF, pattern PList, pattern PListF, pattern PChar, pattern PCharF
+  , pattern PStr, pattern PStrF, pattern HoleP, pattern HoleFP
   , simplify
   ) where
 
@@ -46,8 +47,10 @@ type instance CtrArgsF Parse = []
 type instance XExprF   Parse = ASTXF
 
 data ASTXF r
+  -- | A let expression where the definitions may reference each other recursively.
+  = LetRecP_ !(Text, r) !r
   -- | A natural number literal, e.g. `10`.
-  = PNat_ Int
+  | PNat_ Int
   -- | A list literal, e.g. `[x, y, z]`.
   | PList_ [r]
   -- | A character literal, e.g. `'a`.
@@ -68,6 +71,12 @@ newtype NonEmptyDefFs r = NonEmptyDefFs { getNonEmptyDefFs :: NonEmpty (Text, r)
 pattern LetFP :: NonEmpty (Text, r) -> r -> ASTF r
 pattern LetFP ds e = LetF (NonEmptyDefFs ds) e
 
+pattern LetRecP :: (Text, AST) -> AST -> AST
+pattern LetRecP d e = ExprX (LetRecP_ d e)
+
+pattern LetRecFP :: (Text, r) -> r -> ASTF r
+pattern LetRecFP d e = ExprXF (LetRecP_ d e)
+
 pattern PNat :: Int -> AST
 pattern PNat n = ExprX (PNat_ n)
 
@@ -99,9 +108,9 @@ pattern HoleFP :: ASTF r
 pattern HoleFP = ExprXF HoleP_
 
 {-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, ExprXF                               #-}
-{-# COMPLETE Var,  App,  Abs,  Let,   Ctr,  Case,  PNat,  PList,  PChar,  PStr,  HoleP  #-}
-{-# COMPLETE VarF, AppF, AbsF, LetF , CtrF, CaseF, PNatF, PListF, PCharF, PStrF, HoleFP #-}
-{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, PNatF, PListF, PCharF, PStrF, HoleFP #-}
+{-# COMPLETE Var,  App,  Abs,  Let,   Ctr,  Case,  LetRecP,  PNat,  PList,  PChar,  PStr,  HoleP  #-}
+{-# COMPLETE VarF, AppF, AbsF, LetF , CtrF, CaseF, LetRecFP, PNatF, PListF, PCharF, PStrF, HoleFP #-}
+{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, LetRecFP, PNatF, PListF, PCharF, PStrF, HoleFP #-}
 
 -- TODO: Implement Substitutable for AST.
 
diff --git a/src/LambdaCalculus/Syntax/Parser.hs b/src/LambdaCalculus/Syntax/Parser.hs
index 8ffb08f..dc029ce 100644
--- a/src/LambdaCalculus/Syntax/Parser.hs
+++ b/src/LambdaCalculus/Syntax/Parser.hs
@@ -80,10 +80,13 @@ definition = do
   pure (name, value)
 
 let_ :: Parser AST
-let_ = Let <$> between (keyword "let") (keyword "in") (fromList <$> definitions) <*> ambiguous
+let_ = letrecstar <|> letstar
   where
-    definitions :: Parser [Def Parse]
-    definitions = sepBy1 definition (token ';')
+    letrecstar = LetRecP <$> between (try (keyword "letrec")) (keyword "in") definition <*> ambiguous
+    letstar = Let <$> between (keyword "let") (keyword "in") definitions <*> ambiguous
+
+    definitions :: Parser (NonEmpty (Def Parse))
+    definitions = fromList <$> sepBy1 definition (token ';')
 
 ctr :: Parser AST
 ctr = pair <|> unit <|> either <|> nat <|> list <|> str
@@ -187,10 +190,15 @@ parseAST = parse (spaces *> ambiguous <* eof) "input"
 type Declaration = (Text, AST)
 
 declaration :: Parser Declaration
-declaration = do
-  notFollowedBy (try let_)
-  keyword "let"
-  definition
+declaration = notFollowedBy (try let_) >> (declrec <|> decl)
+  where
+    declrec = do
+      try $ keyword "letrec"
+      (name, expr) <- definition
+      pure (name, LetRecP (name, expr) (Var name))
+    decl = do
+      keyword "let"
+      definition
 
 -- | A program is a series of declarations and expressions to execute.
 type ProgramAST = [DeclOrExprAST]
diff --git a/src/LambdaCalculus/Syntax/Printer.hs b/src/LambdaCalculus/Syntax/Printer.hs
index 481b1d7..6742943 100644
--- a/src/LambdaCalculus/Syntax/Printer.hs
+++ b/src/LambdaCalculus/Syntax/Printer.hs
@@ -56,11 +56,8 @@ unparseAST = toStrict . toLazyText . snd . cata \case
   AbsF names body -> tag Block $
     let names' = fromLazyText (unwords $ map fromStrict $ toList names)
     in "λ" <> names' <> ". " <> unambiguous body
-  LetFP defs body -> tag Block $
-    let
-      unparseDef (name, val) = fromText name <> " = " <> unambiguous val
-      defs' = fromLazyText (intercalate "; " $ map (toLazyText . unparseDef) $ toList defs)
-    in "let " <> defs' <> " in " <> unambiguous body
+  LetFP defs body -> tag Block $ "let " <> unparseDefs defs <> " in " <> unambiguous body
+  LetRecFP def body -> tag Block $ "letrec " <> unparseDef def <> " in " <> unambiguous body
   CtrF ctr e -> unparseCtr ctr e
   CaseF pats ->
     let pats' = fromLazyText $ intercalate "; " $ map (toLazyText . unparsePat) pats
@@ -77,6 +74,9 @@ unparseAST = toStrict . toLazyText . snd . cata \case
     unparseApp ef (unsnoc -> (exs, efinal))
       = tag Ambiguous $ foldr (\e es' -> ambiguous e <> " " <> es') (final efinal) (ef : exs)
 
+    unparseDef (name, val) = fromText name <> " = " <> unambiguous val
+    unparseDefs defs = fromLazyText (intercalate "; " $ map (toLazyText . unparseDef) $ toList defs)
+
     unparseCtr :: Ctr -> [Tagged Builder] -> Tagged Builder
     -- Fully-applied special syntax forms
     unparseCtr CPair [x, y] = tag Finite $ "(" <> unambiguous x <>  ", "  <> unambiguous y <> ")"