This Big: Infinity

So, does the iterative algorithm we last discussed actually terminate? It's easy enough to see that it would if there were only a finite number of types, but last time I claimed that there are in fact an infinite number of concrete types. Let's see why:

class Pointer
{
  private var obj;
  public new(o) {this.obj = o;}
  public Get() {return this.obj;}
  public Set(o) {this.obj = o;}
}

Using just this class (and not even the "built-in" classes like Int and so on) we can construct an infinite number of concrete types. We have Pointer[obj: {}; ...], and Pointer[obj: {Pointer[obj: {}; ...]}; ...], and so on (the fields Get and Set have been ellided). That is, we could have a pointer to the empty typeset, or a pointer to a pointer to the empty typeset, or a pointer to a pointer to a pointer, and on and on.

So clearly we can't just rely on there being a finite number of concrete types when iterating to ensure the algorithm eventually terminates. We need to be a bit more clever. First, let's write some Mix code that leads to an infinite number of types as described above:

main()
{
  var p = new Pointer(null);
  for(...)
  {
    p = new Pointer(p);
  }
}

So, what happens here? First, p's typeset just has a Pointer[...] to an empty typeset. After one iteration, it's has a typeset has two elements: Pointer[...], as before, and another Pointer to it's own typeset. That is, if we could name p's typeset (let's call it p), then p = {Pointer[obj:{}; ...], Pointer[obj: p; ...]}.

So, what happens after another iteration? In fact, we try to add the same concrete type to the typeset again: a Pointer to p. As long as we can recognize that this is the same concrete type as last time, we can stop iterating as no typeset will have changed.

So, that takes care of this example, but what about in general? Is there any way to construct an infinite number of concrete types, without them being cyclic? Clearly it is possible to define a non-cyclic concrete type of arbitrary size, but is it possible to write code that leads to one? We'll see.