Haskell Church Numerals with custom types

user_15343982 0
Viewed 147

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"))

lambda-calculus haskell
1 Answers

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.

user_675790
Related