HN Explorer

9 comments

[ 2.8 ms ] story [ 28.5 ms ] thread
gamegoblin
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).

alexbecker
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.
PaulHoule
Also math is a lot quicker in FORTRAN
tieTYT
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.

tel
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.
gohrt
`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.

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