Hacker News Reader

Comment by tieTYT | Hacker News Reader

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.

View on HN

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

Reply on news.ycombinator.com