Ограничение стоимости

Question

В OCaml вы не можете обобщить частично примененную функцию карри ("ограничение значения").

Какова цель ограничения стоимости? Что бы неприятного случилось, если бы его не было?

Answer 1

Без ограничения значения или других механизмов, ограничивающих обобщение, эта программа будет принята системой типов:

let r = (fun x -> ref x) [];; (* this is the line where the value restriction would trigger *)

> r : 'a list ref

r := [ 1 ];;

let cond = (!r = [ "foo" ]);;

Переменная r будет иметь тип 'a list refЭто означает, что его содержимое можно сравнить с [ "foo" ] хотя он содержал список целых чисел.

Смотрите докторскую диссертацию Ксавье Леруа для большей мотивации (ref это не единственная конструкция, которую можно захотеть добавить к чистому лямбда-исчислению, которое вводит проблему), и обзор систем, которые существовали на момент его диссертации (включая его).

Answer 2

Вот ответ, который я дал некоторое время назад о F#; проблема точно такая же с OCaml. Проблема в том, что без него мы сможем создать ссылки, указывающие на неверный тип данных:

let f : 'a -> 'a option =
    let r = ref None in
    fun x ->
        let old = !r in
        r := Some x;
        old

f 3           // r := Some 3; returns None : int option
f "t"         // r := Some "t"; returns Some 3 : string option!!!

Answer 3

Есть хорошее описание weakly polymorphism здесь (побочные эффекты и слабый полиморфизм).

В общем, давайте посмотрим на функцию ниже (кэшируем первое в истории значение, которое она видит):

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

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

---

Однако предположим, что ограничения по стоимости не было.

Тогда его тип становится val remember : 'a -> 'a = <fun>,

---

Если я сейчас сделаю let () = remember 1, 1 записано внутри cache, право?

Если я позвоню во второй раз, let x = 3 + remember 2, это должно работать, потому что 3 целое число, remember возвращает тот же тип, что и его аргумент. я даю 2 вот так remember также возвращает целое число (но значение равно 1, как мы уже помнили один раз). Это должно пройти проверку типа.

---

Что делать, если я позвоню в третий раз let y = 3.0 + remember 2.0? Будет ли это работать снова?

В соответствии с типом запоминания и причиной моего второго звонка, это также должно работать, потому что я даю float rememberи он должен вернуть float.

Но потому что в первый раз он уже хранится 1 (целое число) внутри, он вернет 1, которое является целым числом. Так что проверка типа не удастся, верно?

---

Мы можем видеть, что без ограничения значения или слабого полиморфизма, из-за того, что допускается изменчивость, у всей проверки типов возникнут проблемы. В вышеописанном глупом случае вам необходимо постоянно проверять или отслеживать исходный тип вручную. remember сохраняются.