Why "currying" requirement matters?

Question

The compiler complains about this error, but the toplevel doesn't.

$ cat ungen.ml
open List
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
        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
         int
#

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.

Update

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 'a list.

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.

The expression:

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 oops above.

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.