Каков формализм доказательства утверждений о единственности функций с определенными сигнатурами?

Question

Предположим, мне нужна функция типа

f: ((A, B) -> C) -> A -> B -> C

Я часто слышал утверждение, что f имеет только одну реализацию, а именно «функцию карри», т.е. g => a => b => g(a, b)

Если принять это за чистую монету, то на самом деле это не так, я всегда могу определить, что f действует иначе, чем это, в особых случаях, например.Я могу сказать, что это g => a => b => g(a, b) кроме случаев, когда A = B и тогда я определяю это как g => a => b => g(b, a).

Тем не менее, интуитивно достаточно ясно, что подразумевается под «имеет только одну реализацию».

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

Я предполагаю, что это теория категорий?Вышеупомянутое немного похоже на идею естественной трансформации, но я не вижу подробностей.

Answer 1

Я уверен, что здесь есть связь с теорией категорий, но на самом деле вы можете сделать это с помощью (как я считаю) более простого инструмента:параметричность.

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

Это предотвращает именно реализацию «особого случая», которую вы описываете в своем вопросе.Также стоит отметить, что все эти реализации экстенсионально равный:они могут выглядеть по-разному, но дают одинаковые результаты при равных затратах.напримервы можете заменить любой термин $т$ с $(\lambda x \ldotp x) t $ и получим эквивалентную функцию.

Утверждения о функциях только из их типа обычно называются свободная теорема, названный в честь статьи, в которой была представлена ​​идея: Теоремы бесплатно Фил Уодлер.Если вас интересует эта область, я настоятельно рекомендую эту статью, поскольку она является хорошим введением в предмет.

Идея, стоящая за этим, на самом деле уходит корнями гораздо дальше, чем эта статья, к работе Джона Рейнольдса с Системой F и «теоремой абстракции», но потребовалось некоторое время, прежде чем идея стала популярной.

На самом деле вы можете генерировать бесплатные теоремы на http://free-theorems.nomeata.de/, хотя, возможно, потребуется немного поработать, чтобы получить полезную информацию из теорем, которые они там приводят.

Если вас интересует параметричность, используемая для доказательства чего-то, кроме свободных теорем, например типобезопасности, тогда Диссертация Амаль Ахмеда это лучшее введение, которое я видел.Она действительно хорошо справляется с описанием семантических типов:Тип программы на самом деле является свойством того, как она работает и что она производит, а то, что мы называем «типами», является синтаксической аппроксимацией этих более общих семантических типов.