Какова теоретико-категориальная основа требования о том, что функция идентификатора Haskell должна возвращать то же значение, что и переданное?

id должен быть морфизмом идентичности для любого данного типа Haskell. Морфизм идентификации для типа A в Hask - это функция типа A -> A, но это не просто любая функция типа A -> A; он должен подчиняться законам категорий.

В частности, это должно быть левое и правое тождество для композиции с морфизмами к / от объекта A. Если idA является идентифицирующим морфизмом для объекта A, это означает, что для любого объекта B и морфизма f :: A -> B, f . idA должен быть точно таким же, как f, и для любого объекта C и морфизма g :: C -> A ifA . g должен быть точно таким же, как g.

Мы можем проверить ваше утверждение о том, что любая функция типа A -> A может быть идентификатором A, выбрав конкретный случай. Давайте возьмем (+1) :: Integer -> Integer в качестве идентификатора для Integer и рассмотрим функцию (*2) :: Integer -> Integer. Очевидно, что (*2) . (+1), (+1) . (*2) и просто (*2) - это одно и то же, поэтому мы показали - подождите, это совсем не одна и та же функция.

Заметьте, я не привел здесь равенство значений Haskell. Я говорю о равенстве морфизмов в категории Hask; а равенство морфизмов наверняка находится в области теории категорий, поскольку без нее законы категорий о морфизме тождества бессмысленны.

Ключевым моментом, который меня смутил в какой-то момент, является то, что, хотя нет смысла рассматривать два разных объекта с одним и тем же типом (поскольку объекты являются типами, когда мы говорим о Hask), вы можете иметь два разных морфизма с одним и тем же типом. Теория категорий действительно допускает наличие нескольких различных морфизмов между двумя объектами A и B (и допускает наличие морфизмов от объекта к самому себе, которые не морфизмами идентичности, и отличаются друг от друга). Морфизмы не определяются чисто их «конечными точками».

Законы об идентичности на самом деле представляют собой довольно строгие требования и должны сильно намекать на то, что не всякая старая A -> A функция подойдет для idA. Существует четкая интуиция, что для возможности компоновки с произвольными другими морфизмами, не изменяя их, морфизм идентичности должен «ничего не делать» (что бы это ни значило для рассматриваемой категории).

В Hask, где мы знаем, что морфизмы - это функции, есть довольно очевидная интерпретация «ничего не делать»; функция, которая просто возвращает свой ввод. Должно быть ясно, что это действительно работает для законов категорий:

f . id = f
id . f = f

А также, если предлагаемый морфизм идентичности, который делает что-то иное, кроме как возвращает свои входные данные без изменений (существуют некоторые x такие, что badId x не x), то вы можете опровергнуть законы категорий, пытаясь составить с id !

(badId . id) x
badId (id x)
badId x

badId x не x, по предположению, поэтому badId . id не может быть равно id (который определяется id x = x). Так что badId - это не левая идентичность композиции.

Я не уверен, что правильно понял суть вашего вопроса.

Но идентичность в категориях должна удовлетворять

id . f = f
g . id = g

для любых f,g правильных типов. Итак, id - это не просто случайная функция A -> A, это функция, удовлетворяющая вышеуказанным требованиям.

Обратите внимание, что в Hask это для любого значения a :: A

id . (const a) = const a

следовательно

id (const a ()) = const a ()

следовательно

id a = a

Итак, id - это действительно то, что мы ожидаем.

Кажется, у вас есть несколько распространенных заблуждений о категории Hask и категориях в целом, но, возможно, все они сводятся к сути

1. В категории Hask объекты относятся к типам Haskell, а морфизмы - к функциям Haskell. Ценности не играют роли в Hask.

В этом нет никакого смысла. Морфизмы в Hask - это функции, а функции - это значения, так что в этом смысле значения уже играют роль в Hask.

Два морфизма f и g от A до B в Hask равны тогда и только тогда, когда функции f, g :: A -> B равны, что, в свою очередь, выполняется тогда и только тогда, когда для каждого значения a :: A значения f a и g a равны. Итак, расширив это определение, мы видим, что значения, которые не обязательно являются функциями (например, a :: A), также играют определенную роль в Hask.

Унитальная и ассоциативная аксиомы для Hask в этом смысле являются равенствами функций, поэтому им есть что сказать об уровне ценности!

Априори значения нефункционального типа не появляются явно в перечне (объекты, морфизмы, идентичности, правила композиции, унитальные и ассоциативные свойства), которые составляют категорию Hask. Но на самом деле значение a :: A может быть закодировано в Hask как морфизм const a :: () -> A, а разные значения a :: A соответствуют разным морфизмам от () до A. Это факт, используемый в вычислениях chi, показывающий, что у нас нет другого выбора для функции идентичности на объект A в Hask помимо знакомого id :: A -> A; id a = a.