overgeneralized curried fns

Question

module MapHelpers (Ord : Map.OrderedType) = struct
  include Map.Make (Ord)
  let add_all a b = fold add a b
end

works but the seemingly equivalent

module MapHelpers (Ord : Map.OrderedType) = struct
  include Map.Make (Ord)
  let add_all = fold add
end

fails to compile with

File "Foo.ml", line 2, characters 18-104:
Error: The type of this module,
       functor (Ord : Map.OrderedType) ->
         sig
           ...
           val add_all : '_a t -> '_a t -> '_a t
         end,
       contains type variables that cannot be generalized
Command exited with code 2.

and adding an explicit type annotation

: 'a . 'a t -> 'a t -> 'a t

causes compilation to fail earlier with

Error: This definition has type 'a t -> 'a t -> 'a t
       which is less general than 'a0. 'a0 t -> 'a0 t -> 'a0 t

Why does adding the explicit formals a b change the way these two modules are typed?

Westerly

You might want to read #4243177 . Caml used to implement “value restriction” and now implements “relaxed value restriction”, I think: math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf – Clypeus

@PascalCuoq, I see the "or when defining polymorphic functions that are not syntactically functions" – Westerly

Answer 1

This is a consequence of the value restriction, as described in the following FAQ item:

A function obtained through partial application is not polymorphic enough

The more common case to get a ``not polymorphic enough'' definition is when defining a function via partial application of a general polymorphic function. In Caml polymorphism is introduced only through the “let” construct, and results from application are weakly polymorph; hence the function resulting from the application is not polymorph. In this case, you recover a fully polymorphic definition by clearly exhibiting the functionality to the type-checker : define the function with an explicit functional abstraction, that is, add a function construct or an extra parameter (this rewriting is known as eta-expansion):

# let map_id = List.map (function x -> x) (* Result is weakly polymorphic *)
val map_id : '_a list -> '_a list = <fun>
# map_id [1;2]
- : int list = [1;2]
# map_id (* No longer polymorphic *)
- : int list -> int list = <fun>
# let map_id' l = List.map (function x -> x) l
val map_id' : 'a list -> 'a list = <fun>
# map_id' [1;2]
- : int list = [1;2]
# map_id' (* Still fully polymorphic *)
- : 'a list -> 'a list = <fun>

The two definitions are semantically equivalent, and the new one can be assigned a polymorphic type scheme, since it is no more a function application.

See also this discussion about what the _ in '_a indicates -- weak, non-polymorphic type variables.

Consuetudinary