Overgeneralized curried fns

Question

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

works, but seemingly equivalent

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

cannot 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 explicit type annotation

 : 'a . 'at -> 'at -> 'at 

causes compilation to fail with

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

Why does adding explicit ab forms change the way you enter these two modules?

Answer 1

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

The function obtained using the partial application is not polymorphic enough

A more common case to get the definition of `` not polymorphic enough '' is to define a function by partially applying a common polymorphic function. In Caml, polymorphism is introduced only through the let construct, and the application results are slightly polymorphic; therefore, the function obtained as a result of the application is not polymorphic. In this case, you restore the completely polymorphic definition, clearly demonstrating the functionality for type checking: define a function with an explicit functional abstraction, that is, add a function construct or an additional parameter (this rewriting is called eta extension):

 # 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> 

Two definitions are semantically equivalent, and a polymorphic type scheme can be assigned to a new one, since it is no longer a functional application.

See also this discussion of what _ points to in '_a - weak variables of non-polymorphic type.