Сверхгенерализованный карри фнс

Question

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

работает, но, казалось бы, эквивалентно

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

не компилируется с

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.

и добавление явной аннотации типа

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

приводит к сбою компиляции ранее с

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

Почему добавление явных формалей a b изменить способ ввода этих двух модулей?

Answer 1

Это является следствием ограничения значения, как описано в следующем разделе часто задаваемых вопросов:

Функция, полученная в результате частичного применения, недостаточно полиморфна

Более распространенным случаем получения "недостаточно полиморфного" определения является определение функции посредством частичного применения общей полиморфной функции. В Caml полиморфизм вводится только через конструкцию "let", а результаты от применения являются слабо полиморфными; следовательно, функция, полученная в результате применения, не является полиморфной. В этом случае вы восстанавливаете полностью полиморфное определение, четко демонстрируя функциональность для средства проверки типов: определите функцию с явной функциональной абстракцией, то есть добавьте функциональную конструкцию или дополнительный параметр (это переписывание известно как eta-расширение):

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

Эти два определения семантически эквивалентны, и новому может быть назначена схема полиморфного типа, поскольку она больше не является функциональным приложением.

Смотрите также это обсуждение о том, что _ в '_a указывает - слабые переменные неполиморфного типа.