Слабый полиморфизм в OCaml

Меня немного смущает слабый полиморфизм в OCaml.

См. Следующий фрагмент, в котором я определяю функцию remember:

let remember x =
   let cache = ref None in
      match !cache with
       | Some y -> y
       | None -> cache := Some x; x
;;

Компилятор может определить полиморфный тип 'a -> 'a, а cache используется локально.

Но когда я изменил приведенный выше код на

let remember =
   let cache = ref None in
    (fun x ->  match !cache with
         | Some y -> y
         | None -> cache := Some x; x)
;;

компилятор определяет слабо полиморфный тип '_a -> '_a, кроме того, похоже, что cache используется совместно при вызовах remember.

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

Более того, если я снова поменяю код

let remember x =
   let cache = ref None in
    (fun z ->  match !cache with
         | Some y -> z
         | None -> cache := Some x; x)
;;

компилятор определяет полиморфный тип 'a -> 'a -> 'a, и cache используется локально. Почему это так?


functional-programming ocaml ml value-restriction
person innovation_cat    schedule 29.07.2013    source источник

Ответы (3)


arrow_upward
8
arrow_downward 

let remember =
 let cache = ref None in
  (fun x ->  match !cache with
       | Some y -> y
       | None -> cache := Some x; x)
;;

Здесь cache закрывается возвращенной функцией. Но в тот момент, когда мы объявляем cache, у нас нет информации о том, каким будет тип; он будет определяться независимо от типа x и создания cache при определении remember.

Но поскольку это закрытие, мы можем сделать что-то вроде этого:

> remember 1
  1

Теперь ясно, что cache : int option ref, поскольку мы на самом деле что-то в нем сохранили. Поскольку существует только один cache, remember может хранить только один тип.

В следующем вы закрываете более двух вещей, x и cache. Поскольку мы создаем новый cache ref при каждом вызове remember, тип снова может быть полностью полиморфным. Причина, по которой тип не является слабо полиморфным, заключается в том, что мы знаем, что собираемся сохранить в нем x, и у нас есть тип xs в то время, когда создается cache.

person Daniel Gratzer    schedule 29.07.2013
comment
Я предполагаю, что вы имели в виду, что cache имеет тип int option ref, а не ref (None int). - person Virgile; 29.07.2013

arrow_upward
6
arrow_downward

Похоже, это связано с ограничением стоимости. Ограничение полного значения (как в SML) полностью отклонит ваш код. Слабо полиморфные типы описаны в статье Жака Гаррига «Ослабление ограничения значений», на которую я, по общему признанию, наткнулся только что после прочтения вашего вопроса:

http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf < / а>

Тот факт, что cache используется в разных вызовах, должен быть очевиден, если у вас есть правильная ментальная модель того, что означает код ML. Вы определяете два значения: remember и cache. Вложенность просто делает область cache частной для блока.

person t0yv0    schedule 29.07.2013

arrow_upward
1
arrow_downward 

let remember x =
   let cache = ref None in
      match !cache with
       | Some y -> y
       | None -> cache := Some x; x


let remember x =
   let cache = ref None in
    (fun z ->  match !cache with
         | Some y -> z
         | None -> cache := Some x; x)

В двух вышеупомянутых версиях remember является "прямой" функцией, каждый раз, когда вы вызываете ее как remember 1, она инициализирует cache значением ref None, не так ли? Так что на самом деле он ничего не запоминает, cache не распределяется между какими-либо remember вызовами.

В другой версии:

let remember =
   let cache = ref None in
    (fun x ->  match !cache with
         | Some y -> y
         | None -> cache := Some x; x)

это отличается. remember, безусловно, по-прежнему является функцией, однако реальная часть, определяющая ее содержимое, - это (fun x -> match ...). Он включает cache, и кеш инициализируется один раз и будет только один раз. Итак, cache распределяется между будущими remember вызовами.

person Jackson Tale    schedule 11.10.2014
comment
Ваша «другая версия» просто решает код, который заставлял меня думать большую часть вчерашнего дня! - person daruma; 15.05.2020