System Eff

So, last time I mentioned that the first example was one "that cannot be handled under Hindley-Milner style inference". So the question is, "Ummm... what?" Let's look at the same code, but in an ML-like syntax:

let twice f x = f (f x)
let pair x = (x, x)

The types inferred for these lovely functions are:

val twice : ('a -> 'a) -> 'a -> 'a
val pair : 'a -> ('a * 'a)

So, what does the type of twice mean? Well, each 'a stands for a universally quantified variable, and in particular one that is quantified at the top level. So it means that, "for all types x, twice takes a function from x to x, and an item of type x, and returns something of type x". But is this really what we "meant" when we wrote out the definition of twice?

Maybe not. When we try to use it with pair we are treating it as though it really had the following type: "for all types x, twice takes a function from any type to the same type, and an item of type x, and returns an x". That is, we want twice to take, as its first argument, a universally quantified type. So, if we throw in some new syntax, we want this type:

val twice : (forall 'y. 'y -> 'y) -> 'x -> 'x.

We want to be able to introduce a universal quantification within the type of twice, and not just at the top level. And this is the problem: in our system of choice, this is not possible.

Now, there are of course systems in which this sort of quantification is perfectly legal; System F, for example, allows all this and more, for just 27 payments of $34.95! But, then again, type inference in System F is undecidable, which might burst your balloon.

This post is brought to you by the Greek letter...

So, a long time ago I said that a Mix alpha release is coming, and it really is, I swear. Here are some examples of Mix code that the implementation can currently compile correctly.

1: This is an example of some code that cannot be handled under Hindley-Milner style inference. Specifically, notice that in the body of twice we apply f to the type of its own result. This requires that f have type 'a -> 'a, and therefore that twice have type ('a -> 'a) -> a'. Clearly in our application of twice the argument pair doesn't have such a restricted type.

twice(f)
{
    return function(x){ return f(f(x)); };
}

pair(x)
{
  return new Pair(x, x);
}

Int main(String args)
{
  var p = twice(pair)(1);
  return p.First.First;
}

2: This example shows how cool container classes are in Mix, at least to me. I love homogenous containers because they (well, the type system) take care of ensuring I don't do anything too stupid with its elements. However, in a language like C# or Java you must introduce an (often artificial) interface in order to group objects of different type but related functionality in such a container -- otherwise you just have to relegate yourself to containers of object, and live with the lack of type safety. Here Mix infers what operations are possible on all elements of the array. The error arrises because Mix infers that the array possibly contains both integers and strings, the latter of which do not implement the negation operator -operator.

Another note: arrays are enumerable (which just means that they implement GetEnumerator correctly), and enumerables implement ToString by simply concatenating the string representations of all of their elements. So as long as all of the elements of an enumerable implement ToString, the enumerable itself does as well, which is how we can call IO.print on the array.

Int main(String args)
{
  var a = new Array(10);
  for(var i = 0; i < a.Length(); i++)
  {
    a[i] = i;
  }
  a[random(10)] = "Hello!";

  IO.print(a);  //Enumerable.

  a[4] = -a[4]; //Error, strings cannot be negated.
  return 0;
}

3: Here's a funny example in which iterating to a fixed point proves critical. Essentially f gets a type that should be interpreted as "either a pointer to an integer, or a pointer to a pointer to a string, or a pointer to a pointer to a pointer to an integer, or..." Which essentially means that the only operations you can really perform on f are ToString and Get (which gets the value of a pointer).

Int main(String s)
{
  var f = new Ptr(0);
  var g = new Ptr("Foo!");
  
  for(var i = 0; i < 10; i += 1)
  {
    var temp = f;
    f = new Ptr(g);
    g = new Ptr(temp);
  };
  
  IO.print("f: " + f);
  IO.print("g: " + g);
  return 0;
}

I wanted to put a few more up, but it is time to get back to work.