4 ms·

Church Numerals

30 points by jbarrow 12y ago

gamegoblin 12y ago
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 https://www.youtube.com/watch?v=VUhlNx_-wYk In it, the speaker implements fizzbuzz using only lambda calculus (making significant use of church encoding).
- tomstuart 12y ago
  Thanks! There’s a transcript at http://codon.com/programming-with-nothing http://codon.com/programming-with-nothing, and the FizzBuzz implementation was recently added to Ruby itself: https://github.com/ruby/ruby/commit/628dac1 https://github.com/ruby/ruby/commit/628dac1
alexbecker 12y ago
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 12y ago
  Also math is a lot quicker in FORTRAN
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).
tel 12y ago
Similar page in style, form, language choice, and even content! http://www.willamette.edu/~fruehr/haskell/evolution.html http://www.willamette.edu/~fruehr/haskell/evolution.html It's just a joke instead.

30 points by jbarrow 12y ago

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 https://www.youtube.com/watch?v=VUhlNx_-wYk In it, the speaker implements fizzbuzz using only lambda calculus (making significant use of church encoding).

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

alexbecker 12y ago

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 12y ago
Also math is a lot quicker in FORTRAN

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

tel 12y ago

Similar page in style, form, language choice, and even content! http://www.willamette.edu/~fruehr/haskell/evolution.html http://www.willamette.edu/~fruehr/haskell/evolution.html It's just a joke instead.