Church Numerals | Hacker News Reader

Church Numerals

karczmarczuk.users.greyc.fr

30 pointsjbarrow9 comments

I like this, but it is yet another page that makes me wonder whether professors conspire to use the worst possible color palettes for their sites.

Also math is a lot quicker in FORTRAN

For anyone who finds this interesting, I cannot recommend enough investing a half hour in watching the "Programming With Nothing" talk:

https://www.youtube.com/watch?v=VUhlNx_-wYk

In it, the speaker implements fizzbuzz using only lambda calculus (making significant use of church encoding).

Thanks! There’s a transcript at http://codon.com/programming-with-nothing, and the FizzBuzz implementation was recently added to Ruby itself: https://github.com/ruby/ruby/commit/628dac1

To my surprise, the Haskell was not the difficult part for me. I spent more time wondering why this is the definition of "zero":

    zero s z = z

My understanding is you can call this like so:

    zero 3 7 #returns 7

So.... in what way does this relate to "zero"?

I got to the definition of "one" and that made me realize that `s` is supposed to a function (because AFAIK, Haskell can only return 1 thing). This doesn't clarify my initial confusion, but it does make the type definitions a little more concrete in my head.

Yeah... I'm going to stop reading. I think this could be written better. Maybe it would be a good reference if I already had a decent grasp of what Church Numerals are, but I don't.

Let's say `n` is a natural number then `C(n)` is the Church encoding of that natural number. `C(n)` is a function of two arguments called, traditionally, `succ` and `zero` such that

    C(n)(succ, zero) = succ(succ(succ(succ(...succ(zero)))))

where `succ` is applied `n` times. So if you have a normal datatype encoding of natural numbers

    data Nat = Zero | Succ Nat

then you can convert Church numerals to that data type very trivially

    C(n)(Succ, Zero)

To maybe see the pattern a little more clearly, let's consider something very similar to Naturals---linked lists!

The Church encoding of a linked list, `l`, (also known as its right fold or recursor) is a function of two arguments traditionally called `cons` and `nil`

    C(l)(cons, nil)

such that the following equations hold

    C([]    )(cons, nil) = nil
    C(a : as)(cons, nil) = cons a (C(as)(cons, nil))

In other words, it changes a list like

    a : b : c : d : e : f : []

into

    cons a (cons b (cons c (cons d (cons e (cons f nil)))))

for whatever the choice of `cons` and `nil` were. Again, if we take the standard constructors for a List

    data List a = Nil | Cons a (List a)

then we can apply them to the Church encoding to immediately transform it into its data type

    C(l)(Cons, Nil)

Finally, take note that the `cons` function here is the same as the "reduction function" talked about so much in Clojure transducers (also: everywhere else). It's really fundamental to the type of lists and streams.

`zero` doesn't act on integers, it acts on other functions.

The second argument to `zero` is a placeholder. The intuition is that `zero s` is "apply the function `s` zero times". What do you get if you apply the function `s` zero times to an argument `z`? You get `z`.

There's a hint later down in the article about type-checking.

Technically, it can act on integers:

    Prelude> let zero s z = z
    Prelude> :t zero
    zero :: t -> t1 -> t1
    Prelude>

t and t1 can be integers. Really the point of my comment is that the article could be written much better (assuming I'm the intended demographic).

Similar page in style, form, language choice, and even content!

http://www.willamette.edu/~fruehr/haskell/evolution.html

It's just a joke instead.

Reply on news.ycombinator.com