Recursion: See "Recursion"

So, taking a brief break from history, let's take yet another look at type inference in Mix. Way back when I mentioned that one of the restrictions we needed to place on the subset of Mix for which the algorithm worked was that no recursive calls we allowed. First, let's recall why; consider the following code:

Factorial(i)
{
  if(i == 0)
    return 1;
  else
    return i * Factorial(i - 1);
}

main()
{
  var i = Factorial(7);
}

A simple factorial, no big deal. So, what should they type of i be? Well, first let's get our terminology straight: what concrete types should be in the typeset of i?

Just by thinking about it we should conclude that it should hold only Int[...]. But, if we run the original, or even the iterative algorithm on this code, what happens? Infinite loopiness. The terror!

(Incidentally; if the call to Factorial in main were Factorial(7.0f), i would hold both Int[...] and Float[...] in it's typeset; the base case should tell you why).

The problem is that, when type checking the right hand side of the assignment in main, we are obligated to check the type of Factorial with an argument of Int[...]. In so doing, we check that Int[...] implements operator==, operator*, and operator-. And then we check Factorial with an argument of Int[...]. In so doing we check that... And on and on.

However, this is easy enough to fix (or at least, it's easy enough to partially fix): let's keep track of the "call chain", and whenever we start checking a new call, we'll search the call chain for said call. If it is not in the call chain, we'll add it to the call chain and check the type like normal. But if it is in the call chain, we get to stop type checking: we know that checking the call will only get us right back where we started.

Pause for a second: what exactly is a "call", and how do we represent a "call chain"? A call is just the (unique) name of a function or method, along with the type of each argument. This last bit is important, because otherwise we might realize that a previous call to AddTwoNumbers succeeded with integers, and imagine that it would succeed on files. A call chain is a list of such calls, in the order we've invoked them.

But, is finding a call in the call chain an error, or success? And anyway, what does it mean? Second question first: it means that there is a loop in the call graph, just like we saw in the code above, and furthermore that the recursive call is at the same types: the function is being used in a monomorphically recursive way. First question second: we'll treat this as a success, because it indicates that along this call chain all possible method invocations succeed (possibly while looping infinitely). If they succeed, it meets the correctness requirement we've already talked about. If it loops infinitely, it still meets this requirement. (Side note: we're essentially saying "it's correct, unless this other runtime error comes up, but that error will hide the incorrectness"; we'll see this with respect to null next time).

Side note: this is rather strange, in that it somehow means that we are interested in a greatest fixed point, whereas normally we are interested in least fixed points. We're taking the view (in a handwavish sort of way) that, if when trying to prove P, we eventually have to prove P, we'll consider this to be true, or provable.

So, if you take the above as correct, are we back to a terminating algorithm? Well... not necessarily. Once again we would have termination "for free" if only we had a finite number of types to deal with. Unfortunately, we don't, and so this doesn't terminate so easily. In fact we could force this to terminate by requiring that all recursive calls to a particular function have the same type (that is, make all functions monomorphically recursive), but that's no good -- check out this simple function that isn't monomorphically recursive:

identity(arg)
{
  if(identity(rand() == 42))
    return identity(arg);
  return arg;
}

It's just the identity function, but with a little twist: no matter what the type of arg is, the function might recursively called with a Bool[...] argument. In ML the type of the function is 'a -> 'a, but it is used in a polymorphically recursive way. Anyway, a strange function, but they can be found in "real life" (especially when mutual recursion comes into play); Henglein had an interesting (and approachable) paper on inference in the presence of generalized polymorphic recursion in an ML-like settings -- check it out. If you don't bother, let me just mention that inference for such a language can be shown to be undecidable (indeed that's a contribution of the paper) by showing that it is equivalent to semi-unification. And that means that, in what I'm trying to do with Mix, I will inevitably face some tough choices to reign in this undecidability somehow; sounds fun!