update README

README.md

@@ -5,9 +5,11 @@ A (very WIP) lambda expression evaluator and debugger.
 I'd like to build the following:
 
 - [X] parsing with parsec
-  - need to harden tests a bit more but existing tests pass
 - [X] alpha/beta reduction to beta normal
 - [ ] substitutions for known abstractions (numbers can be written and are displayed as numbers rather than lambda terms)
+  - [ ] replace known terms in input
+  - [X] replace known terms in output
+  - [ ] support detection and replacement for generic church numerals (not just 1 and 0 (false))
 - [ ] persisted variables
 - [ ] display all steps in alpha/beta reductions until beta normal form is reached
 - [ ] online web-based lambda playground

lamb.cabal

@@ -14,8 +14,9 @@ executable lamb
     main-is:          Main.hs
     other-modules:    Parser,
                       Evaluation,
-                      Bruijn
+                      Bruijn,
-    build-depends:    base, containers, parsec
+                      Niceties
+    build-depends:    base, bimap, containers, parsec
     hs-source-dirs:   src
     default-language: Haskell2010
 
@@ -27,7 +28,10 @@ test-suite lamb-tests
                         ParserSpec,
                         Evaluation,
                         EvaluationSpec,
-                        BruijnSpec
+                        Bruijn,
-    build-depends:      base, containers, hspec, parsec
+                        BruijnSpec,
+                        Niceties,
+                        NicetiesSpec
+    build-depends:      base, bimap, containers, hspec, parsec
     build-tool-depends: hspec-discover:hspec-discover
     default-language:   Haskell2010

src/Main.hs

@@ -1,6 +1,7 @@
 module Main where
 
 import Evaluation (run)
+import Niceties (replaceKnowns)
 import Parser (parse)
 import System.Environment (getArgs)
 import System.IO (IOMode (ReadMode), hGetContents, openFile)
@@ -15,5 +16,5 @@ main = do
   case command of
     "run" -> do
       content <- openFile path ReadMode >>= hGetContents
-      either putStrLn putStrLn $ show . run <$> parse content
+      either putStrLn putStrLn $ show . replaceKnowns . run <$> parse content
     _ -> putStrLn $ "Unrecognized command: " ++ command

src/Niceties.hs

@@ -0,0 +1,245 @@
+module Niceties where
+
+import Bruijn (toDeBruijn)
+import Data.Bimap (Bimap, fromList, lookupR)
+import Parser (Expr (Abstraction, Application, Variable))
+
+findKnown :: Expr -> Maybe String
+findKnown e = lookupR (toDeBruijn e) knownValues
+
+-- | Replace known values in expression with proper names
+replaceKnowns :: Expr -> Expr
+replaceKnowns a@(Abstraction name body) = case findKnown a of
+  Just name' -> Variable name'
+  Nothing -> Abstraction name $ replaceKnowns body
+replaceKnowns (Application f arg) = Application (replaceKnowns f) (replaceKnowns arg)
+replaceKnowns v = v
+
+knownValues :: Bimap String Expr
+knownValues =
+  Data.Bimap.fromList
+    [ ( "I",
+        toDeBruijn $ Abstraction "x" (Variable "x")
+      ),
+      ( "true",
+        -- same as K
+        toDeBruijn $
+          Abstraction "x" (Abstraction "y" (Variable "x"))
+      ),
+      ( "false",
+        -- same as K*, `0`, `nil`
+        toDeBruijn $
+          Abstraction "x" (Abstraction "y" (Variable "y"))
+      ),
+      ( "S",
+        toDeBruijn $
+          Abstraction "x" $
+            Abstraction "y" $
+              Abstraction "z" $
+                Application
+                  (Application (Variable "x") (Variable "z"))
+                  (Application (Variable "y") (Variable "z"))
+      ),
+      ( "B",
+        toDeBruijn $
+          Abstraction "x" $
+            Abstraction "y" $
+              Abstraction "z" $
+                Application
+                  (Variable "x")
+                  (Application (Variable "y") (Variable "z"))
+      ),
+      ( "C",
+        toDeBruijn $
+          Abstraction "x" $
+            Abstraction "y" $
+              Abstraction "z" $
+                Application
+                  (Application (Variable "x") (Variable "z"))
+                  (Variable "y")
+      ),
+      ( "W",
+        toDeBruijn $
+          Abstraction "x" $
+            Abstraction "y" $
+              Application
+                (Application (Variable "x") (Variable "y"))
+                (Variable "y")
+      ),
+      ( "ω",
+        toDeBruijn $
+          Abstraction "x" $
+            Application (Variable "x") (Variable "x")
+      ),
+      -- Fixed points
+      ( "Y",
+        toDeBruijn $
+          Abstraction "f" $
+            Application
+              ( Abstraction "x" $
+                  Application
+                    (Variable "f")
+                    (Application (Variable "x") (Variable "x"))
+              )
+              ( Abstraction "x" $
+                  Application
+                    (Variable "f")
+                    (Application (Variable "x") (Variable "x"))
+              )
+      ),
+      ( "Z",
+        toDeBruijn $
+          Abstraction "f" $
+            Application
+              ( Abstraction "x" $
+                  Application (Variable "f") $
+                    Abstraction "v" $
+                      Application
+                        (Application (Variable "x") (Variable "x"))
+                        (Variable "v")
+              )
+              ( Abstraction "x" $
+                  Application (Variable "f") $
+                    Abstraction "v" $
+                      Application
+                        (Application (Variable "x") (Variable "x"))
+                        (Variable "v")
+              )
+      ),
+      -- Church numerals
+      -- Note: if you use the Church numeral recognition algorithm,
+      -- you may not need these in the Bimap at all.
+      ( "succ",
+        toDeBruijn $
+          Abstraction "n" $
+            Abstraction "f" $
+              Abstraction "x" $
+                Application
+                  (Variable "f")
+                  ( Application
+                      (Application (Variable "n") (Variable "f"))
+                      (Variable "x")
+                  )
+      ),
+      ( "plus",
+        toDeBruijn $
+          Abstraction "m" $
+            Abstraction "n" $
+              Abstraction "f" $
+                Abstraction "x" $
+                  Application
+                    (Application (Variable "m") (Variable "f"))
+                    ( Application
+                        (Application (Variable "n") (Variable "f"))
+                        (Variable "x")
+                    )
+      ),
+      ( "mult",
+        toDeBruijn $
+          Abstraction "m" $
+            Abstraction "n" $
+              Abstraction "f" $
+                Application
+                  (Variable "m")
+                  (Application (Variable "n") (Variable "f"))
+      ),
+      ( "exp",
+        toDeBruijn $
+          Abstraction "m" $
+            Abstraction "n" $
+              Application (Variable "n") (Variable "m")
+      ),
+      ( "pred",
+        toDeBruijn $
+          Abstraction "n" $
+            Abstraction "f" $
+              Abstraction "x" $
+                Application
+                  ( Application
+                      ( Application (Variable "n") $
+                          Abstraction "g" $
+                            Abstraction "h" $
+                              Application
+                                (Variable "h")
+                                (Application (Variable "g") (Variable "f"))
+                      )
+                      (Abstraction "u" (Variable "x"))
+                  )
+                  (Abstraction "u" (Variable "u"))
+      ),
+      ( "isZero",
+        toDeBruijn $
+          Abstraction "n" $
+            Application
+              ( Application (Variable "n") $
+                  Abstraction "x" $
+                    Abstraction "a" $
+                      Abstraction "b" (Variable "b")
+              )
+              (Abstraction "a" $ Abstraction "b" (Variable "a"))
+      ),
+      -- Church booleans
+      ( "and",
+        toDeBruijn $
+          Abstraction "p" $
+            Abstraction "q" $
+              Application
+                (Application (Variable "p") (Variable "q"))
+                (Variable "p")
+      ),
+      ( "or",
+        toDeBruijn $
+          Abstraction "p" $
+            Abstraction "q" $
+              Application
+                (Application (Variable "p") (Variable "p"))
+                (Variable "q")
+      ),
+      ( "not",
+        toDeBruijn $
+          Abstraction "p" $
+            Abstraction "a" $
+              Abstraction "b" $
+                Application
+                  (Application (Variable "p") (Variable "b"))
+                  (Variable "a")
+      ),
+      -- Pairs
+      ( "pair",
+        toDeBruijn $
+          Abstraction "x" $
+            Abstraction "y" $
+              Abstraction "f" $
+                Application
+                  (Application (Variable "f") (Variable "x"))
+                  (Variable "y")
+      ),
+      ( "fst",
+        toDeBruijn $
+          Abstraction "p" $
+            Application (Variable "p") $
+              Abstraction "x" $
+                Abstraction "y" (Variable "x")
+      ),
+      ( "snd",
+        toDeBruijn $
+          Abstraction "p" $
+            Application (Variable "p") $
+              Abstraction "x" $
+                Abstraction "y" (Variable "y")
+      ),
+      -- Lists
+      ( "cons",
+        toDeBruijn $
+          Abstraction "h" $
+            Abstraction "t" $
+              Abstraction "f" $
+                Abstraction "x" $
+                  Application
+                    (Application (Variable "f") (Variable "h"))
+                    ( Application
+                        (Application (Variable "t") (Variable "f"))
+                        (Variable "x")
+                    )
+      )
+    ]

src/Parser.hs

@@ -6,7 +6,7 @@ import Text.Parsec
 import Text.Parsec.String (Parser)
 
 data Expr = Variable String | Abstraction String Expr | Application Expr Expr
-  deriving (Eq)
+  deriving (Eq, Ord)
 
 instance Show Expr where
   show (Variable name) = name

test.lm

@@ -1 +1 @@
-(λx.λy.λz. x z (y z)) (λa.λb. a) (λa.λb. a)
+(λn. n (λx. λa. λb. b) (λa. λb. a)) (λf. λx. x)

test/NicetiesSpec.hs

@@ -0,0 +1,19 @@
+module NicetiesSpec (spec) where
+
+import Bruijn (toDeBruijn)
+import Niceties (findKnown, replaceKnowns)
+import Parser (Expr (Abstraction, Application, Variable))
+import Test.Hspec
+
+spec :: Spec
+spec = do
+  describe "can find knowns" $ do
+    it "can find identity" $
+      findKnown identity `shouldBe` Just "I"
+  describe "replaceKnowns" $ do
+    it "can replace identity" $
+      replaceKnowns identity `shouldBe` Variable "I"
+    it "can replace identity of identity" $
+      replaceKnowns (Application identity identity) `shouldBe` Application (Variable "I") (Variable "I")
+  where
+    identity = toDeBruijn $ Abstraction "x" (Variable "x")