Also checkout Scott encoding - for numerals each number is constructed by embedding it's predecessor (with 0 as per Church): 0 = \f \x x N+1 = \f \x f N T

Also checkout Scott encoding - for numerals each number is constructed by embedding it's predecessor (with 0 as per Church): 0 = \f \x x N+1 = \f \x f N To interrogate such a numeral, you supply a function that accepts the predecessor numeral, and a constant for zero. Recursion is needed to effect a fold. On the face of it heavier than Church, but allows the recursive definition of infinity. Lists and more complex structures can be similarly defined, again with the possibility of recursively defined infinite components. Then you can do fun stuff like 'taking' infinite elements from a (possibly infinite) list, adding infinity to any number to get infinity, multiplying likewise. Division by zero naturally returns infinity by construction, no convention necessary. 'dropping' infinity elements from an infinite list does not terminate however - you can never reach the first element of that result.