Skip to content

Commit

Permalink
Use s and z for Church numeral abstractions
Browse files Browse the repository at this point in the history
  • Loading branch information
severen committed May 20, 2024
1 parent 5905348 commit 010938c
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 11 deletions.
6 changes: 3 additions & 3 deletions src/Sly/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -74,9 +74,9 @@ astShow = T.unpack . go
-- | Convert a nonnegative integer into a Church numeral term.
toChurchNat :: Int -> Term
toChurchNat n =
Abs (Name "f") $
Abs (Name "x") $
iterate (App (Var $ Name "f")) (Var $ Name "x") !! n
Abs (Name "s") $
Abs (Name "z") $
iterate (App (Var $ Name "s")) (Var $ Name "z") !! n

-- | Convert a term into a nonnegative integer if it has the shape of a Church
-- numeral.
Expand Down
16 changes: 8 additions & 8 deletions tests/UnitTests.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,21 +20,21 @@ import Sly.Syntax (
unitTests :: IO TestTree
unitTests = testSpec "Unit Tests" do
describe "Church Numerals" do
it "0 == \\f x -> x" do
let zero = Abs (Name "f") $ Abs (Name "x") (Var $ Name "x")
it "0 == \\s z -> z" do
let zero = Abs (Name "s") $ Abs (Name "z") (Var $ Name "z")
toChurchNat 0 `shouldBe` zero
fromChurchNat zero `shouldBe` Just 0

it "1 == \\f x -> f x" do
let one = Abs (Name "f") $ Abs (Name "x") $ App (Var $ Name "f") (Var $ Name "x")
it "1 == \\s z -> s z" do
let one = Abs (Name "s") $ Abs (Name "z") $ App (Var $ Name "s") (Var $ Name "z")
toChurchNat 1 `shouldBe` one
fromChurchNat one `shouldBe` Just 1

it "2 == \\f x -> f (f x)" do
it "2 == \\s z -> s (s z)" do
let two =
Abs (Name "f") $
Abs (Name "x") $
App (Var $ Name "f") (App (Var $ Name "f") (Var $ Name "x"))
Abs (Name "s") $
Abs (Name "z") $
App (Var $ Name "s") (App (Var $ Name "s") (Var $ Name "z"))
toChurchNat 2 `shouldBe` two
fromChurchNat two `shouldBe` Just 2

Expand Down

0 comments on commit 010938c

Please sign in to comment.