User loginNavigation |
Theoretical Pearl: Church numerals, twice!
Ralf Hinze. Theoretical Pearl: Church numerals, twice! Journal of Functional Programming, 2004. To appear.
This pearl explains Church numerals, twice. The first explanation links Church numerals to Peano numerals via the well-known encoding of data types in the polymorphic LC. This view suggests that Church numerals are folds in disguise. The second explanation, which is more elaborate, but also more insightful, derives Church numerals from first principles, that is, from an algebraic specification of addition and multiplication. Additionally, we illustrate the use of the parametricity theorem by proving exponentiation as reverse application correct. A simple concept is used to demonstrate several interesting and useful techniques. |
Browse archives
Active forum topics
|
Recent comments
15 weeks 1 day ago
19 weeks 3 days ago
21 weeks 23 hours ago
21 weeks 23 hours ago
23 weeks 5 days ago
28 weeks 3 days ago
28 weeks 3 days ago
28 weeks 6 days ago
28 weeks 6 days ago
31 weeks 4 days ago