Search code examples
haskelllambda-calculus

Haskell Church Numerals with custom types


I'm trying to solve a Church numerals parser I have a custom type which distinguishes between variable, lambda and application

type Var = String

data Term =
    Variable Var
  | Lambda   Var  Term
  | Apply    Term Term
  deriving Show

I have a function called church I can define a cases manually for different variations of church. So let's say:

  • church 0 Lambda "f" (Lambda "x" (Variable "x"))
  • church 1 should output Lambda "f" (Lambda "x" (Apply (Variable "f") (Variable "x")))
  • church 2 should output Lambda "f" (Lambda "x" (Apply (Variable "f") (Apply (Variable "f") (Variable "x"))))

and so on.

I've tried recursively call the church function as per:

church :: Int -> Term
church 0 = Lambda "f" (Lambda "x" (Variable  "x"))
church i = Apply (church(i -1)) (Apply (Variable "f") (Variable "x"))

However that keeps repeating also the part with Lambda "f" (Lambda "x"

The other approach I've tried was

church :: Int -> Term
church 0 = Lambda "f" (Lambda "x" (Variable  "x"))
church i = Apply (church (i -1)) (Apply (Variable "f") (Variable "x"))

However this also yields result with copied lambdas. Am I missing something here? How can I only repeat the application part (Apply (Variable "f") (Variable "x"))


Solution

  • All church numerals start with an \f -> (\i -> …), so that means that our function should look like:

    church :: Int -> Term
    church n = Lambda f (Lambda x (go n))

    where we still need to implement go :: Int -> Term. This thus means that for go we have to find a function that looks like:

    go 0 = Variable "x"
    go 1 = Apply (Variable ("f")) (Variable "x")
    go 2 = Apply (Variable "x") (Apply (Variable ("f")) (Variable "x"))
    

    so for a go n, we thus have to return a Variable "x" wrapped in n items with Apply (Variable "x")

    The implementation thus should look like:

    go :: Int -> Term
    go 0 = Variable "x"
    go n = … (go (n-1))

    Where I leave implementing as an exercise.