OCaml: Есть ли функция с типом 'a ->' a, отличная от функции идентификации?

Ответ 1

Как вы определяете функции идентификации? Если вы рассматриваете только синтаксис, существуют разные функции идентификации, которые имеют правильный тип:

let f x = x
let f2 x = (fun y -> y) x
let f3 x = (fun y -> y) (fun y -> y) x
let f4 x = (fun y -> (fun y -> y) y) x
let f5 x = (fun y z -> z) x x
let f6 x = if false then x else x

Есть еще более странные функции:

let f7 x = if Random.bool() then x else x
let f8 x = if Sys.argv < 5 then x else x

Если вы ограничиваете себя чистым подмножеством OCaml (который исключает f7 и f8), все функции, которые вы можете построить, проверяют наблюдательное уравнение, которое в определенном смысле гарантирует, что то, что они вычисляют, является личным: для всех значений f : 'a -> 'a, имеем, что f x = x

Это уравнение не зависит от конкретной функции, оно однозначно определяется типом. Существует несколько теорем (в разных контекстах), которые формализуют неофициальную идею о том, что "полиморфная функция не может изменять параметр полиморфного типа, а только передавать ее". См., Например, статью Филиппа Вадлера, Теоремы бесплатно!.

Хорошая вещь с этими теоремами заключается в том, что они относятся не только к случаю 'a -> 'a, что не так интересно. Вы можете получить теорему из типа ('a -> 'a -> bool) -> 'a list -> 'a list функции сортировки, которая гласит, что ее приложение коммутирует с отображением монотонной функции. Более формально, если у вас есть какая-либо функция s с таким типом, то для всех типов u, v, функции cmp_u : u -> u -> bool, cmp_v : v -> v -> bool, f : u -> v и список li : u list, а если cmp_u u u' t213 > (f монотонно), вы имеете:

map f (s cmp_u li) = s cmp_v (map f li)

Это действительно так, когда s - это точно функция сортировки, но мне кажется впечатляюще доказать, что она верна для любой функции s с тем же типом.

Как только вы разрешаете исключение, либо расходящимся (циклически бесконечно, как и с помощью функции let rec f x = f x, указанной выше), либо путем выделения исключений, конечно, вы можете иметь что угодно: вы можете построить функцию типа 'a -> 'b, и типы больше ничего не означают. Использование Obj.magic : 'a -> 'b имеет тот же эффект.

Есть более здравые способы потерять эквивалентность идентичности: вы можете работать внутри непустой среды с предопределенными значениями, доступными из функции. Рассмотрим, например, следующую функцию:

let counter = ref 0
let f x = incr counter; x

Вы все еще являетесь тем свойством, что для всех x, f x = x: если вы рассматриваете только возвращаемое значение, ваша функция по-прежнему ведет себя как идентификатор. Но как только вы рассматриваете побочные эффекты, вы больше не эквивалентны (без побочных эффектов): если я знаю counter, я могу написать разделительную функцию, которая возвращает true при задании этой функции f, и вернет false для чистых функций идентификации.

let separate g =
  let before = !counter in
  g ();
  !counter = before + 1

Если счетчик скрыт (например, сигнатурой модуля или просто let f = let counter = ... in fun x -> ...), и никакая другая функция не может его наблюдать, мы снова не можем отличить f и чистые функции идентификации. Таким образом, история гораздо более тонкая в присутствии локального государства.

Ответ 2

let rec f x = f (f x)

Эта функция никогда не заканчивается, но имеет тип 'a -> 'a.

Если мы разрешаем только полные функции, вопрос становится более интересным. Без использования злых трюков невозможно написать полную функцию типа 'a -> 'a, но злые трюки забавны так:

let f (x:'a):'a = Obj.magic 42

Obj.magic - злая мерзость типа 'a -> 'b, которая позволяет всем видам махинаций обходить систему типов.

С другой стороны, считается, что он не является полным либо потому, что он будет сбой при использовании с коробками.

Итак, реальный ответ: функция тождества является единственной полной функцией типа 'a -> 'a.

Ответ 3

Выбрасывание исключения также может дать вам тип 'a -> 'a:

# let f (x:'a) : 'a = raise (Failure "aaa");;
val f : 'a -> 'a = <fun>

Ответ 4

Если вы ограничиваете себя "разумным" сильно нормируемым типизированным λ-исчислением, то существует единственная функция типа ∀α α → α, которая является тождественной функцией. Вы можете доказать это, исследуя возможные нормальные формы члена этого типа.

Philip Wadler 1989 статья "Теоремы бесплатно" объясняет, как функции, имеющие полиморфные типы, обязательно удовлетворяют некоторым теоремам (например, карта-подобная функция коммутирует с состав).

Однако есть некоторые неинтуитивные проблемы, когда речь идет о большом полиморфизме. Например, существует стандартный трюк для кодирования индуктивных типов и рекурсии с импрессивным полиморфизмом путем представления индуктивного объекта (например, списка) с использованием его функции-реципиента. В некоторых случаях существуют термины, принадлежащие типу функции-рекурсора, которые не являются функциями-реципиентами; есть пример в § 4.3.1 Кристина Паулин кандидатская диссертация.