3 ms·

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 understa

by tieTYT 12y ago

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 12y ago
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 12y ago
`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 12y ago
  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).

by tieTYT 12y ago

tel 12y ago

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 12y ago

`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 12y ago
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).