From f055d600fd5e2489fc875f1d57ceaf996cb70a51 Mon Sep 17 00:00:00 2001
From: Matei Adriel <rafaeladriel11@gmail.com>
Date: Sun, 29 Oct 2023 02:03:27 +0200
Subject: [PATCH] Add lambda calculus

---
 purescript/README.md                      |   2 +
 purescript/lambda-calculus/.gitignore     |  11 +
 purescript/lambda-calculus/packages.dhall |   4 +
 purescript/lambda-calculus/spago.dhall    |  30 +++
 purescript/lambda-calculus/src/Main.purs  | 272 ++++++++++++++++++++++
 purescript/lambda-calculus/test/Main.purs |  11 +
 6 files changed, 330 insertions(+)
 create mode 100644 purescript/lambda-calculus/.gitignore
 create mode 100644 purescript/lambda-calculus/packages.dhall
 create mode 100644 purescript/lambda-calculus/spago.dhall
 create mode 100644 purescript/lambda-calculus/src/Main.purs
 create mode 100644 purescript/lambda-calculus/test/Main.purs

diff --git a/purescript/README.md b/purescript/README.md
index aef2410..5d09b7a 100644
--- a/purescript/README.md
+++ b/purescript/README.md
@@ -10,9 +10,11 @@
 | [existentials-blog](./existentials-blog) | Perhaps supposed to turn into a blog about existentials?                                                             |
 | [existentials](./existentials)           | Experiment regarding the Church-encoding of existential types                                                        |
 | [gadts](./gadts)                         | Experiment regarding ways to encode GADTs in Purescript                                                              |
+| [lambda-calculus](./lambda-calculus)     | Lambda calculus evaluator                                                                                            |
 | [lune](./lune)                           | Failed effect-system project                                                                                         |
 | [maps](./maps)                           | Attempt at implementing maps with membership proofs                                                                  |
 | [proofs](./proofs)                       | Attempt at expressing mathematical proofs using Purescript's effect system                                           |
+| [purebird](./purebird)                   | Flappy-bird game                                                                                                     |
 | [purpleflow](./purpleflow)               | Unfinished dependently-typed programming language                                                                    |
 | [slice](./slice)                         | Basic benchmarks and a `Slice` type                                                                                  |
 | [sprint](./sprint)                       | Failled effect-system based on typelevel lists                                                                       |
diff --git a/purescript/lambda-calculus/.gitignore b/purescript/lambda-calculus/.gitignore
new file mode 100644
index 0000000..39af3d6
--- /dev/null
+++ b/purescript/lambda-calculus/.gitignore
@@ -0,0 +1,11 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago
+index.js
diff --git a/purescript/lambda-calculus/packages.dhall b/purescript/lambda-calculus/packages.dhall
new file mode 100644
index 0000000..9becfd7
--- /dev/null
+++ b/purescript/lambda-calculus/packages.dhall
@@ -0,0 +1,4 @@
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.1-20210516/packages.dhall sha256:f5e978371d4cdc4b916add9011021509c8d869f4c3f6d0d2694c0e03a85046c8
+
+in  upstream
diff --git a/purescript/lambda-calculus/spago.dhall b/purescript/lambda-calculus/spago.dhall
new file mode 100644
index 0000000..2899968
--- /dev/null
+++ b/purescript/lambda-calculus/spago.dhall
@@ -0,0 +1,30 @@
+{ name = "lc"
+, dependencies =
+  [ "aff"
+  , "arrays"
+  , "console"
+  , "control"
+  , "effect"
+  , "either"
+  , "fixed-points"
+  , "foldable-traversable"
+  , "identity"
+  , "lists"
+  , "matryoshka"
+  , "maybe"
+  , "node-buffer"
+  , "node-process"
+  , "node-streams"
+  , "nonempty"
+  , "parsing"
+  , "prelude"
+  , "psci-support"
+  , "refs"
+  , "strings"
+  , "transformers"
+  , "tuples"
+  , "unordered-collections"
+  ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}
diff --git a/purescript/lambda-calculus/src/Main.purs b/purescript/lambda-calculus/src/Main.purs
new file mode 100644
index 0000000..8e0dbdf
--- /dev/null
+++ b/purescript/lambda-calculus/src/Main.purs
@@ -0,0 +1,272 @@
+module Main where
+
+import Prelude
+
+import Control.Alt ((<|>))
+import Control.Lazy (fix)
+import Control.Monad.Reader (ask, local, runReader)
+import Control.Plus (empty)
+import Data.Array (reverse)
+import Data.Array as Array
+import Data.Array.NonEmpty (some)
+import Data.Array.NonEmpty as NonEmptyArray
+import Data.Either (Either(..))
+import Data.Foldable (foldl, foldlDefault)
+import Data.Foldable as Foldable
+import Data.Functor.Mu (Mu(..))
+import Data.HashMap as HashMap
+import Data.Identity (Identity)
+import Data.List (List(..), (:))
+import Data.Maybe (Maybe(..), fromMaybe, maybe)
+import Data.NonEmpty (NonEmpty(..))
+import Data.String (joinWith)
+import Data.Traversable (class Foldable, class Traversable, foldrDefault, traverseDefault)
+import Data.Tuple.Nested ((/\))
+import Effect (Effect)
+import Effect.Aff (Aff, effectCanceler, launchAff_, makeAff)
+import Effect.Class.Console (logShow)
+import Effect.Ref as Ref
+import Matryoshka (class Corecursive, cata, embed, project)
+import Node.Encoding (Encoding(..))
+import Node.Process (stdin)
+import Node.Stream (Readable, onDataString, onEnd, onError, pause)
+import Text.Parsing.Parser (ParseError, Parser, runParser)
+import Text.Parsing.Parser.String (oneOf)
+import Text.Parsing.Parser.Token (GenLanguageDef(..), GenTokenParser, LanguageDef, alphaNum, letter, makeTokenParser)
+
+readText :: forall w. Readable w -> Aff (Maybe String)
+readText r = makeAff $ \res -> do
+  dataRef <- Ref.new ""
+  onDataString r UTF8 \chunk ->
+    Ref.modify_ (_ <> chunk) dataRef
+  onEnd r do
+    allData <- Ref.read dataRef
+    res $ Right (Just allData)
+  onError r $ Left >>> res
+  pure $ effectCanceler (pause r)
+
+main :: Effect Unit
+main = launchAff_ do
+  text <- fromMaybe " " <$> readText stdin
+  case parseLambdaCalculus text of
+    Left err -> logShow err
+    Right ast -> logShow $ project $ reduce $ introduceDeBrujinIndices ast
+
+
+---------- Types
+data AstF v f
+  = Call f f
+  | Lambda String f
+  | Var v
+
+type Ast v = Mu (AstF v)
+
+data DeBrujin 
+  = Bound Int String
+  | Free String
+
+derive instance functorAst :: Functor (AstF v)
+
+instance foldableAst :: Foldable (AstF v) where
+  foldMap f = case _ of
+    Call function argument -> f function <> f argument
+    Var _ -> mempty
+    Lambda _ body -> f body
+
+  foldr f = foldrDefault f
+  foldl f = foldlDefault f
+
+instance traversableAst :: Traversable (AstF v) where
+  sequence = case _ of
+    Call f a -> Call <$> f <*> a
+    Lambda name body -> Lambda name <$> body
+    Var v -> pure $ Var v
+
+  traverse = traverseDefault
+
+instance showAst :: Show (AstF DeBrujin (Ast DeBrujin)) where
+  show :: AstF DeBrujin (Ast DeBrujin) -> String
+  show = case _ of
+    Var (Free name) -> name
+    Var (Bound _ name) -> name
+    Call function argument 
+      -> withParensIf (project function) needsParensLeft 
+      <> " "
+      <> withParensIf (project argument) needsParensRight
+    Lambda name body -> showLambdas (name : Nil) (project body)
+    where
+    showLambdas names (Lambda name body) = showLambdas (name:names) (project body)
+    showLambdas Nil body = show body
+    showLambdas names body 
+      = "\\" 
+      <> joinWith " " (reverse $ Array.fromFoldable names) 
+      <> ". " 
+      <> show body 
+
+    withParensIf term predicate = if predicate term
+      then "(" <> show term <> ")" 
+      else show term
+
+    needsParensLeft = case _ of
+      Lambda _ _ -> true
+      _ -> false
+
+    needsParensRight = case _ of
+      Call _ _ -> true
+      Lambda _ _ -> true
+      _ -> false
+
+data Error
+  = NotInScope Int String
+
+---------- Constructors
+call :: forall t v. Corecursive t (AstF v) => t -> t -> t
+call f a = embed (Call f a)
+
+var :: forall t v. Corecursive t (AstF v) => v -> t
+var = Var >>> embed
+
+lambda :: forall t v. Corecursive t (AstF v) => String -> t -> t
+lambda l t = embed (Lambda l t)
+
+---------- Reduction
+introduceDeBrujinIndices :: Ast String -> Ast DeBrujin
+introduceDeBrujinIndices i = cata go i # flip runReader HashMap.empty 
+  where
+  go = case _ of
+    Var name -> ado
+      indices <- ask
+      in var $ maybe (Free name) (\index -> Bound index name) $ HashMap.lookup name indices
+    Call func arg -> call <$> func <*> arg
+    Lambda name body -> lambda name <$> local updateContext body
+      where
+      updateContext m = ((+) one <$> m) `HashMap.union` HashMap.singleton name zero
+
+betaReduction :: Ast DeBrujin -> Ast DeBrujin
+betaReduction = cata case _ of
+  Var v -> var v
+  Call function argument -> do
+    case project function of
+      Lambda _ body -> betaReduction $ unshift $ substitute 0 (shift argument) body
+      _ -> call function argument
+  Lambda name body -> lambda name body
+
+etaReduction :: Ast DeBrujin -> Ast DeBrujin 
+etaReduction = cata case _ of
+  Var v -> var v
+  Call f a -> call f a 
+  Lambda _ (In (Call term (In (Var (Bound 0 _))))) | not (occurs 0 term) -> unshift term
+  Lambda name l -> lambda name l
+
+substitute :: Int -> Ast DeBrujin -> Ast DeBrujin -> Ast DeBrujin
+substitute at with within = cata go within # flip runReader (at /\ with) 
+  where
+  go = case _ of
+    Call f a -> call <$> f <*> a
+    Var (Bound index name) -> ado
+      at' /\ with'  <- ask
+      in if index == at' then with'  else var (Bound index name)
+    Var v -> pure $ var v
+    Lambda name body -> lambda name <$> local updateContext body 
+      where updateContext (at' /\ with') = (at' + 1) /\ shift with' 
+
+shiftBy :: Int -> Ast DeBrujin -> Ast DeBrujin
+shiftBy amount term = cata go term 0 
+  where
+  go = case _ of
+    Var (Bound index name) -> \over -> var $ flip Bound name if index < over then index else index + amount 
+    Var v -> const $ var v
+    Call f a -> \over -> call (f over) (a over)
+    Lambda name body -> \over -> lambda name $ body (over + 1)
+  
+
+shift :: Ast DeBrujin -> Ast DeBrujin
+shift = shiftBy 1
+
+unshift :: Ast DeBrujin -> Ast DeBrujin
+unshift = shiftBy (-1)
+
+occurs :: Int -> Ast DeBrujin -> Boolean
+occurs = flip (cata go)
+  where
+  go = case _ of
+    Var (Bound index _) -> (==) index
+    Call f a -> f || a
+    Lambda _ body -> (+) 1 >>> body
+    _ -> const false
+
+reduce :: Ast DeBrujin -> Ast DeBrujin
+reduce = betaReduction >>> etaReduction
+
+---------- Parser
+-- | Punctuation to start the declaration of a lambda expression.
+lambdaStarts :: Array String
+lambdaStarts = [ "\\", "λ" ]
+
+-- | Punctuation to start the declaration of the body of a lambda expression.
+lambdaBodyStarts :: Array String
+lambdaBodyStarts = [ "->", "." ]
+
+-- | Declaration for lambda calculus (with comments).
+-- | This is used to generate the lexer
+language :: LanguageDef
+language =
+  LanguageDef
+    { commentStart: "{-"
+    , commentEnd: "-}"
+    , commentLine: "--"
+    , nestedComments: true
+    , opStart: empty
+    , opLetter: empty
+    , caseSensitive: true
+    , reservedOpNames: lambdaStarts <> lambdaBodyStarts
+    , reservedNames: []
+    , identStart: letter
+    , identLetter: alphaNum <|> oneOf [ '_', '\'' ]
+    }
+
+-- | The lexer
+tokenParser :: GenTokenParser String Identity
+tokenParser = makeTokenParser language
+
+-- | Parsers which run in the identity monad and parse strings
+type LambdaParser r
+  = Parser String r
+
+-- | Parser for individual lambda calculus expressions.
+-- | This references itself so we use it within a fixpoint operator
+expression' :: LambdaParser (Ast String) -> LambdaParser (Ast String)
+expression' expr = do
+  -- expression'' <- atom
+  (NonEmpty expression'' args) <- NonEmptyArray.toNonEmpty <$> some atom
+  pure $ foldl call expression'' args
+  where
+  { parens, identifier, reservedOp } = tokenParser
+
+  atom :: LambdaParser (Ast String)
+  atom = wrapped <|> lambdaExpr <|> variable
+
+  wrapped :: LambdaParser (Ast String)
+  wrapped = parens expr
+
+  variable :: LambdaParser (Ast String)
+  variable = var <$> identifier
+
+  lambdaExpr :: LambdaParser (Ast String)
+  lambdaExpr = do
+    Foldable.oneOf $ reservedOp <$> lambdaStarts
+    (NonEmpty arg args) <- NonEmptyArray.toNonEmpty <$> NonEmptyArray.reverse <$> some identifier
+    Foldable.oneOf $ reservedOp <$> lambdaBodyStarts
+    body <- expr
+    let
+      baseAst = lambda arg body
+    pure $ foldl (flip lambda) baseAst args
+
+-- | Parser for lambda calculus.
+expression :: LambdaParser (Ast String)
+expression = fix expression'
+
+-- | Try parsing a string into a lambda calculus ast.
+parseLambdaCalculus :: String -> Either ParseError (Ast String)
+parseLambdaCalculus = flip runParser expression
+
diff --git a/purescript/lambda-calculus/test/Main.purs b/purescript/lambda-calculus/test/Main.purs
new file mode 100644
index 0000000..f91f98c
--- /dev/null
+++ b/purescript/lambda-calculus/test/Main.purs
@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."