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

Question

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

Answer 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' подразумевает cmp_v (f u) (f u') (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 и функции чистой идентичности.Так что история гораздо более тонкая в присутствии местного государства.

Answer 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.

Answer 3

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

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

Answer 4

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

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

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