Talk:Church numerals: Difference between revisions

(RankNTypes)
 
(2 intermediate revisions by 2 users not shown)
Line 98:
===RankNTypes & coercion===
This is a nice task, it is good at showing different type systems. Several examples refers to Haskell's RankNTypes. What does it do? Does it make all Church numerals the same type? In the C++ implementation of division, I had trouble with 4-2 and 3-1 being different types even though they are both 2. Is that the cause of needing coercion? [[User:Garbanzo|Garbanzo]] ([[User talk:Garbanzo|talk]]) 21:14, 23 December 2022 (UTC)
 
===0^0===
Also, it is amazing that 0^0 works out to 1. Still trying to wrap my head around that one. [[User:Garbanzo|Garbanzo]] ([[User talk:Garbanzo|talk]]) 21:17, 23 December 2022 (UTC)
 
:0^0 is (generally) defined to be 1, which is not necessarily what you might expect, as you note... As a justification, consider x^n: x^n = x(x^(n-1)), so 2^3 = 2(2^2), 2^2 = 2(2^1) and so 2^1 must be 2(2^0). As 2^1 is 2, 2^0 must be 1 and similarly, every integer to the power 0 must be 1. If you imagine drawing a graph of y = x^0, it would be the straight line y = 1. If 0^0 isn't 1, there would be a discontinuity at x = 0. --[[User:Tigerofdarkness|Tigerofdarkness]] ([[User talk:Tigerofdarkness|talk]]) 23:21, 23 December 2022 (UTC)
 
:: Yes, it is amazing that it works out naturally with Church numerals too which seem to come at it from a different angle. [[User:Garbanzo|Garbanzo]] ([[User talk:Garbanzo|talk]]) 08:05, 27 December 2022 (UTC)
125

edits