SML: Generalizable vs. Non-Generalizable Type Variables

Question

I just came across these in Ch. 5 of Ullman's Elements of ML Programming. He says:

"A type variable such as 'a has two different meanings. It can mean "for every type T, there is an instance of this object with type T in place of 'a. This type variable is called generalizable."

Then he says:

"'a may also represent any one type that we choose. However, after that one type is selected, the type cannot change, even if we reuse the object whose type was described using the original type variable 'a. This type variable is called non-generalizable."

Could someone give an example of each type? Having a hard time wrapping my head around this one and understanding the distinction seems important (he builds on these definitions).

Thanks!

Answer 1

That's a result of the value restriction in SML.

As the language infers types for your program, it can find expressions that would work for any type, which it represents with type variables. The map function is a good example. (My syntax might be a bit off because I've never used SML.)

fun map f nil     = nil
  | map f (x::xs) = f x :: map f xs

Since this function works for lists of any type, it gets a type variable:

('a -> 'b) -> 'a list -> 'b list

We can use the same map function for both int list and string list—this is a generalizable type variable. One thing worth noting is the nil case: nil can as easily be an empty list of int as an empty list of string. It has the type 'a list.

In a perfect world, this is all we would have. However there's a problem: mutable references. Following the same logic as above, the following ref would have a type variable in its type too:

val x = ref nil

We expect x to be a ('a list) ref. Just like nil itself, it can as easily be a (int list) ref or a (string list) ref—or can it? The problem is that we can set references. If we can use x as if it has the more specific type (int list) ref we could set it to [1,2,3]. And then, if we could use it as a (string list) ref somewhere else, we could read out [1,2,3] to something expecting a list of strings! That's a problem.

To overcome this problem, SML has the value restriction. Roughly speaking, it means that things that don't "look" like functions can't be fully polymorphic—they can't have generalizable type variables. Instead, the type of x would be based on the first concrete type we use it with (ie (int list) ref). If we then go on and try to use x with a different concrete type, we would get an error about non-generalizable type variables.,

In a sense, a non-generalizable type variable is just a placeholder until we do use x and give it a concrete type. It's a bit confusing because it still looks like a normal type variable ('a) but gives us an error if we use it in more than one way. I think OCaml does a much better job of differentiating between the two. OCaml would infer the type of x as '_a which is syntactically different from normal type variables and makes it clear that it's just a placeholder, not a normal polymorphic value.

It's a bit of a wart in the language but something that's basically unavoidable if you want to have mutable references like that.