On Infinite Things

Infinite things don't really exist. Consider the simplest example: the natural numbers 0,1,2,3,... We have strong intuitions about this set and we use that intuition in applying mathematics to the real world. Yet everything about Nat, the natural numbers, follows logically from the following simple, and finite, set of rules:

• Zero and Succ are primitive entities, completely defined by the following:
• Zero belongs to Nat;
• Succ maps from Nat to Nat. If N belongs to Nat, then Succ(N) belongs to Nat.

The recurrence relation is real but not easy to think about. The infinite set of natural numbers is something we are more comfortable with.

Consider the test program in the recently released first draft of Wombat compiler code:

   `fact1 _n = if (_n:Int>=?0)==0 then {1} else {_n*fact1(_n-1)};

   `fact2 = { `n = $:Int>=?0; if n==0 then {1} else {n*fact2(n-1)}};

   `in = getInt();

   putInt( fact1 in = fact2 in)

To understand the first line, consider this very finite situation. We have 2 expressions within a closure:

1. `not true = false
2. `not false = true

The first thing to note is that it is OK to declare the same name more than once in a closure as long as the names are compatible. Being equal is the simplest form of compatibility. The other acceptable form of compatibility is by combining procedures, and that is what applies here. For the gory details see http://wombatlang.blogspot.com.au/2015/05/combining-procedures-in-wombat.html. But basically they have to agree (or be combined!) where they overlap, and where one fails (harmlessly = Fail.next) and the other doesn't, the combination takes that value. The declared name can't be used until all declarations are complete.

Getting back to that first line above:

   `fact1 _n = if (_n:Int>=?0)==0 then {1} else {_n*fact1(_n-1)}

The first thing to notice is that this expression is the left parameter of a semicolon(;) operator, so the value is discarded, and only the side affect (defining fact1) is relevant. For the record the value would be a Type.

The expression involves a free variable (_n). That means this is an application of a Wombat macro. Since no macro is specified, the default applies, which is "forall". So this is really:

   forall _n (`fact1 _n = if (_n:Int>=?0)==0 then {1} else {_n*fact1(_n-1)})

This is the same as our definition of "not" above, except that there are an infinite number of procedures to be combined (all possibilities for which the expression doesn't fail):

   `fact1 0 = if (0:Int>=?0)==0 then {1} else {0*fact1(0-1)}

   `fact1 1 = if (1:Int>=?0)==0 then {1} else {1*fact1(1-1)}

   `fact1 2 = if (2:Int>=?0)==0 then {1} else {2*fact1(2-1)}

   ...

Except that it is not to be regarded as being in any order.

Note that we can refer to fact1 inside the definition because that is inside a closure. It is technically a forward reference which is filled in, completing the construction of the closure, when the definition completes. The closure can not be called until all forward references are filled in.

[update 2016-09-28: This is no longer quite correct in the new wombat.]