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

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от некоторого типа к некоторому типу), но соответствуют функторам внутри категории типов (отображение типов на типы :: * -> *).