I am reading this OCaml walking through slides, and I find an intersting question here:
It seems that oops function will generate an compiling error :
the type of this expression contains type variables that cannot be generalized
I don't know the reason so I quick do some test on this function using OCaml version 4.01.0 on my Mac, to my surprise, I didn't see any errors when interpret this code
I don't know why the slide claim it is an error because of currying, and I can not re-create this error...
Could anyone give me some help?
Best How To :
The compiler complains about this error, but the toplevel doesn't.
$ cat ungen.ml
let oops = fold_left (fun a _ -> a + 1) 0
$ ocamlc -c ungen.ml
File "ungen.ml", line 2, characters 11-41:
Error: The type of this expression, '_a list -> int,
contains type variables that cannot be generalized
The problem still exists in the toplevel; you would see it if you tried to use
oops to calculate the length of two lists of different types:
OCaml version 4.01.0
# open List;;
# let oops = fold_left (fun a _ -> a + 1) 0;;
val oops : '_a list -> int = <fun>
# oops [1;2;3;4];;
- : int = 4
# oops ['a';'b';'c'];;
Error: This expression has type char but an expression was expected of type
Note that if you use
oops with exactly one type of list (not zero or two), there is no error. The compiler can complain if you use
oops (an exported symbol) zero times because it can see the whole module and knows how
oops is used. The toplevel can't complain about zero uses because it never knows what you might type next.
Sorry, I should have said more about what the actual error is (at the level I understand it). In my opinion this has little to do with currying.
This is the notorious "value restriction". The short description of the value restriction is as follows: there are some expressions that can't safely be generalized. That is, you can't make them polymorphic and thus allow them to be used with all types. The simplest example is something like this:
let mylist = ref 
If you allowed
mylist to have the type
'a list ref, you could then store lists of all different types in it, which isn't safe.
However, this is safe to generalize:
let mylist2 = 
There is no problem in generalizing
mylist2 to the type
In modern ML derivatives like OCaml, the restrictions on generalization have been reduced to a more or less simple rule. A "value" (like
) can be generalized. An expression that's not a value (like
ref ) can't be generalized.
fold_left (fun a _ -> a + 1) 0
is not a value. It's a function application, with the same rough form as
ref . This (obviously) is the definition of
On the other hand, the expression:
fun xs -> fold_left (fun a _ -> a + 1) 0 xs
IS a value; it's a lambda. So it can be generalized. This (after unfolding a convenient syntactic abbreviation) is the definition of
len above. That's why
len works on all lists, but
oops is not so useful.
The distinction between values and non-values is syntactic; i.e., it can be determined just by looking locally at the form of the expression. You don't need to know anything about the types or the meaning of the expression to make the determination.
One argument for using the value restriction in its current form is that in most cases you can recover the desired generalization (i.e., the polymorphism) of a function by defining it in the form of
len instead of in the form of
oops. This simple transformation is called "eta expansion."
The fact that eta expansion changes just the syntax but not the meaning of the function shows that the value restriction is just an approximation. That is, it forbids generalization of some number of expressions that it would be safe to generalize. But it's nice and simple, and not too restrictive in cases that occur in real programs.
Since OCaml 3.07, the value restriction of OCaml has been improved from basic ML, in that it allows generalization in more cases. You can read about it here: J. Garrigue, Relaxing the Value Restriction. This paper also contains an excellent capsule summary of the value restriction and its history.