Почему функция с полиморфным типом `forall t: Type, t-> t` должна быть тождественной функцией?

Я новичок в теории языка программирования. Я смотрел несколько онлайн-лекций, в которых преподаватель утверждал, что функция с полиморфным типом была forall t: Type, t->tбы идентичностью, но не объяснял почему. Может кто-нибудь объяснить мне, почему? Может быть, доказательство претензии из первых принципов.

Первое, что нужно отметить, это то, что это не обязательно так. Например, в зависимости от языка функция с этим типом, помимо функции идентичности, может: 1 null) выполнять цикл навсегда, 2) изменять какое-либо состояние, 3) возвращать , 4) генерировать исключение, 5) выполнять некоторые операции ввода-вывода, 6) разветвить поток, чтобы сделать что-то еще, 7) сделать call/ccмахинации, 8) использовать что-то вроде Java Object.hashCode, 9) использовать отражение, чтобы определить, является ли тип целым числом, и увеличить его, если так, 10) использовать отражение для анализа стека вызовов и сделать что-то на основе контекста, в котором это называется, 11) возможно, много других вещей и, конечно, произвольных комбинаций вышеперечисленного.

Таким образом, свойство, которое приводит к этому, параметричность, является свойством языка в целом, и существуют его более сильные и более слабые варианты. Для многих из формальных исчислений, изученных в теории типов, ни одно из вышеупомянутых поведений не может произойти. Например, для Системы F / чистого полиморфного лямбда-исчисления, где параметрическость была впервые изучена, ни одно из вышеупомянутых поведений выше не может иметь место. Он просто не имеет исключений, изменяемое состояние, null, call/cc, I / O, отражение, и это сильно нормализации , поэтому он не может быть зациклен навсегда. Как отметил Жиль в комментарии, в статье Теоремы бесплатно!Фил Вадлер является хорошим введением в эту тему, и его ссылки пойдут дальше в теорию, в частности, технику логических отношений. В этой ссылке также перечислены некоторые другие работы Вадлера на тему параметричности.

Поскольку параметричность является свойством языка, для его доказательства требуется сначала формальное формулирование языка, а затем довольно сложный аргумент. Неофициальный аргумент для этого конкретного случая, предполагающий, что мы находимся в полиморфном лямбда-исчислении, состоит в том, что, поскольку мы ничего не знаем о, tмы не можем выполнять какие-либо операции с вводом (например, мы не можем увеличить его, потому что не знаем, является ли он число) или создайте значение этого типа (для всех, что мы знаем t= Void, тип без значений вообще). Единственный способ получить значение типа t- это вернуть тот, который нам дан. Другие виды поведения невозможны. Один из способов убедиться в этом - использовать строгую нормализацию и показать, что существует только один термин нормальной формы этого типа.

Доказательство претензии довольно сложное, но если вы действительно этого хотите, вы можете проверить оригинальную статью Рейнольдса на эту тему.

Ключевая идея состоит в том, что оно справедливо для параметрически полиморфных функций, где тело полиморфной функции одинаково для всех мономорфных экземпляров функции. В такой системе нельзя делать никаких предположений о типе параметра полиморфного типа, и если единственное значение в области видимости имеет универсальный тип, то тут нет ничего общего с его возвратом или передачей другим функциям, которые вы ' мы определили, что, в свою очередь, ничего не можем сделать, кроме как вернуть или передать его ... и т.д. Таким образом, в конце концов, все, что вы можете сделать, это несколько цепочек функций идентификации перед возвратом параметра.

Со всеми предостережениями, которые упоминает Дерек, и игнорируя парадоксы, возникающие в результате использования теории множеств, позвольте мне набросать доказательство в духе Рейнольдса / Вадлера.

Функция типа:

f :: forall t . t -> t

семейство функций проиндексированных по типу t .$f_t$$t$

Идея состоит в том, что для формального определения полиморфных функций мы должны рассматривать типы не как наборы значений, а как отношения. Основные типы, например, Intвызывают отношения равенства - например, два Intзначения связаны, если они равны. Функции связаны, если они отображают связанные значения на связанные значения. Интересный случай - полиморфные функции. Они сопоставляют связанные типы с соответствующими значениями.

$f$$g$

forall t . t -> t

$s$$t$$f$$s$$f_s$$s \to s$$t$$g_t$$t \to t$$f$$g$$f_s$$g_t$

fst$f_s$$f_t$

()()t()t((), c)ct$f_{(\,)}$$f_t$$f_{(\,)}$()()$f_t$cc()c$f_t$$id_t$tfid

Вы можете найти более подробную информацию в моем блоге .

РЕДАКТИРОВАТЬ: комментарий выше предоставил недостающую часть. Некоторые люди преднамеренно играют с языками, не требующими полного обучения. Мне явно наплевать на такие языки. Действительно полезный не полный по языку язык - безумно сложная вещь для разработки. Все остальное расширяется на том, что происходит, пытаясь применить эти теоремы к полному языку.

Ложь!

function f(a): forall t: Type, t->t
    function g(a): forall t: Type, t->t
       return (a is g) ? f : a
    return a is f ? g : a

где isоператор сравнивает две переменные для ссылочной идентичности. То есть они содержат одинаковое значение. Не эквивалентное значение, то же значение. Функции fи gэквивалентны по определению, но они не совпадают.

Если эта функция передается сама, она возвращает что-то еще; в противном случае он возвращает свои данные. Нечто другое имеет тот же тип, что и сам, поэтому его можно заменить. Другими словами, fэто не личность, потому что f(f)возвращается g, тогда как личность вернется f.

Для выполнения теоремы она должна предполагать смешную способность уменьшать

function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(1000, <0, a>)[1]¹

Если вы хотите предположить, что вы можете предположить, что гораздо более простой вывод типа может быть обработан.

Если мы попытаемся ограничить область до тех пор, пока теорема не будет выполнена, мы в конечном итоге вынуждены ограничить ее ужасно далеко.

• Чистый функционал (нет изменяемого состояния, нет ввода-вывода). ОК, я могу жить с этим. Много времени мы хотим запустить доказательства над функциями.
• Пустая стандартная библиотека. Мех.
• Нет raiseи нет exit. Теперь мы начинаем ограничиваться.
• Нет нижнего типа.
• В языке есть правило, которое позволяет компилятору свернуть бесконечную рекурсию, предполагая, что она должна завершиться. Компилятору разрешено отклонять тривиальную бесконечную рекурсию.
• Компилятору разрешается сбой, если он представлен чем-то, что не может быть доказано в любом случае. Теперь стандартная библиотека не может принимать функции в качестве аргументов. Бу.
• Существует нет nil. Это начинает становиться проблематичным. У нас закончились способы борьбы с 1/0.
• Язык не может делать выводы типа ветви и не имеет переопределения, когда программист может доказать вывод типа, который язык не может. Это довольно плохо.

Существование обоих последних двух ограничений нанесло ущерб языку. Пока Тьюринг еще не завершен, единственный способ получить работу общего назначения - это симулировать внутреннюю платформу, которая интерпретирует язык с более слабыми требованиями.

¹ Если вы думаете, что компилятор может вывести это, попробуйте этот

function fermat(z) : int -> int
    function pow(x, p)
        return p = 0 ? 1 : x * pow(x, p - 1)
    function f2(x, y, z) : int, int, int -> <int, int>
        left = pow(x, 5) + pow(y, 5)
        right = pow(z, 5)
        return left = right
            ? <x, y>
            : pow(x, 5) < right
                ? f2(x + 1, y, z)
                : pow(y, 5) < right
                    ? f2(2, y + 1, z)
                    : f2(2, 2, z + 1)
    return f2(2, 2, z)
function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(fermat(3)[0], <0, a>)[1]

² Доказательство того, что компилятор не может этого сделать, зависит от ослепления. Мы можем использовать несколько библиотек, чтобы компилятор не мог видеть цикл одновременно. Кроме того, мы всегда можем создать что-то, где программа будет работать, но не может быть скомпилирована, потому что компилятор не может выполнить индукцию в доступной памяти.

Кто-то думает, что вы можете получить этот return nil без произвольных обобщенных типов, возвращающих nil. Это платит противное наказание, за которое я не видел ни одного эффективного языка, который мог бы заплатить.

function f(a, b, c): t: Type: t[],int,int->t
    return a[b/c]

не должен компилироваться. Основная проблема заключается в том, что индексирование массивов во время выполнения больше не работает.