Соответствие и равенство Карри Говарда

Question

Некоторое время назад я читал, что тип функции a -> b соответствует отношению a ≤ b, или это a ≥ b? Это имеет смысл для меня, потому что два типа изоморфны, если между ними имеется биекция (т. Е. (a ≈ b) ≡ (a -> b, b -> a)). Аналогичным образом, (a = b) ≡ (a ≤ b) ∧ (a ≥ b).

Я знаю, что это не соответствие Карри-Говарда-Ламбека (т. Е. Соответствие теории типов, логики и теории категорий). Это соответствие теории типов и чего-то еще. Я хочу узнать больше об этой переписке. Может ли кто-нибудь указать мне в правильном направлении?

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

Answer 1

Каждый предварительно заказанный набор образует категорию. Пусть (S, «) будет предустановленным набором. Определите категорию C, чьими объектами являются элементы S и с Hom(a, b), где проживает (a, b), если a « b и нежилой в противном случае. Определите композицию единственным возможным способом. Законы категории сразу следуют из транзитивности и рефлексивности предзаказа.

Решетка, в частности, образует категорию, допускающую конечные продукты и копроизведения. Ограниченная решетка образует единицу с начальным и конечным объектами.

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

Answer 2

(Это больше, чем комментарий ответа, но мне нужно больше пространства.)

Тип a -> b соответствует a <= b. Это полезно, например, говорить о фиксированных точках на уровне типа, которые необходимы для правильного определения рекурсивных типов (списков, деревьев, ...).

Напомним, как рекурсия решена без категорий. В теории домена, заданной функцией f :: a -> a, мы находим наименьшее значение x, удовлетворяющее f x = x (наименее фиксированная точка). Это оказывается также наименьшим x, удовлетворяющим f x <= x (наименьшая префиксная точка). После этого мы получим принцип индукции

f y <= y ==> fix f <= y 

, которые в основном говорится, что если мы имеем любой префикс точки y, то наименьшее (предварительно) неподвижная точка fix f должна быть меньше, чем y - на самом деле, это минимум!

Теперь давайте покроем некоторые породы категории над этим. Вывод становится стрелкой ->, а <= также становится ->. Мы получаем

(f y -> y) -> fix f -> y 

Выглядит, где я вижу это ...? Ах!

newtype Fix f = Fix { unFix :: f (Fix f) } 
cata :: Functor f => (f y -> y) -> Fix f -> y 
cata g = g . fmap (cata g) . unFix 

Следовательно, cata общий выпрямитель/катаморфизм просто категория-уполномочена версия старой доброй принципу индукции.

Обратите внимание, что точка доступа к домену y - объект в нашей категории (т. Е. Типы). Кроме того, функции f должны быть применимы к y, поэтому они не являются морфизмами в нашей категории (которые будут функцией значения:: A -> B, от некоторого типа до некоторого типа), но соответствуют функторам в категории типов (типы отображения типов :: * -> *).