каково теоретическое определение функции в Haskell

Question

Я хотел бы увидеть, с точки зрения основ, то, что в Haskell называется функциями.

Смотрите, категорически, есть "вещи", которые объединяются ассоциативно, с функцией тождества, и этого было бы достаточно теоретически.

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

Если мы применим этот подход к Haskell, то я вижу, что категория Hask - это просто подкатегория Sets, что для меня выглядит странно.

Я бы предпочел расширить понятие функции для применения к тому, что мы имеем в Haskell.

Здесь в комментариях этот вопрос коснулся касательно, но не очень глубоко. Я хотел бы услышать четкое утверждение, вроде «но на самом деле они все множества» или «нет, мы не имеем ничего общего с теорией множеств».

Есть идеи? Соображения?

Answer 1

Это очень сложная тема. Чтобы сделать его простым и управляемым, мы часто срезаем углы и часто «лжем».

Haskell, как и все языки программирования, имеет собственный синтаксис и правила оценки ( операционная семантика ). Однако размышления о языке программирования только в эксплуатационных терминах могут быть довольно ограничивающими и обременительными. Когда мы вызываем функцию factorial, мы не заботимся о том, как она реализована, или о точном количестве шагов оценки, необходимых для получения ее результата.

Для преодоления этой денотационной семантики было предложено, где синтаксис интерпретируется по частям в некоторой «математической» модели. Возможно, что многие разные программы (синтаксические выражения) отображаются в одной и той же интерпретации («семантика»).

Насколько я знаю, денотационная семантика для всего языка Хаскелла никогда не определялась. Тем не менее, существуют модели для фрагментов Haskell. Эти модели обычно являются категориями.

Вот несколько примеров.

Если мы (в значительной степени!) Ограничим Хаскелл конечным, просто типизированным ядром, то все, что нам нужно, - это (би-) декартова замкнутая категория, и категории множеств достаточно с ее произведениями, копроизведениями и экспонентами.

Однако Haskell не заканчивается и имеет общую рекурсию, поэтому нам нужны фиксированные точки. Обычно это решается путем перехода к категории полных частичных заказов (обычно между омега-CPO или DCPO).

Тогда нам нужны фиксированные точки уровня типа, поэтому нам нужно рассмотреть категорию с начальными F-алгебрами (по крайней мере, для функторов с хорошим поведением F). Это серьезно усложняет ситуацию.

Мы еще не добавили полиморфизм! Это особенно сложно, поскольку Рейнольдс доказал, что полиморфизм не может быть наивно смоделирован с помощью множеств («полиморфизм не является теоретико-множественным» является основной справочной статьей). Таким образом, теперь у нас есть модели PER и когерентные модели (обе являются категориями), так как некоторые пытаются предоставить семантику полиморфизму.

Тогда нам нужны классы типов, GADT, более высокие ранги, более высокие виды, ...

На практике нам не нужен этот уровень сложности. При программировании мы обычно имеем дело с ограниченным количеством функций, поэтому мы «лжем» себе и часто притворяемся, что все работает как набор или достаточно близко. Затем мы добавим сложность обратно, если это действительно необходимо.