Зависимые пары, карринг и Карри-Говард

[thedeemon]

Все мы помним про карринг, позволяющий функцию, принимающую пару аргументов, заменить на функцию от одного аргумента, возвращающую функцию от второго, которая уже возвращает нужный результат. Типы ((a,b) -> c) и (a -> b -> c) эквивалентны, т.к. мы можем описать две функции от одного к другому и обратно, композиция которых равна id, т.е. построить изоморфизмы. Запишем их на хаскелеподобном языке Идрис:

id1 : ((a,b) -> c) -> (a -> b -> c)
id1 f = \a => \b => f (a,b)

id2 : (a -> b -> c) -> ((a,b) -> c)
id2 f = \pair => f (fst pair) (snd pair)

В хаскеле они есть в стандартной библиотеке под именами curry и uncurry. Теперь вспомним соответствие Карри-Говарда, связывающее типы с утверждениями, а значения с доказательствами. Произведение типов (тупл, product type) там превращается в конъюнкцию, функциональный тип - в следствие. Фактически, выше мы доказали утверждение
((A & B) => C) == (A => (B => C))

Теперь перенесемся в мир зависимых типов, взяв тот же язык Идрис. Одним из базовых элементов, появляющихся с зависимыми типами, является зависимая пара - обобщение произведения типов, также известное как зависимая сумма (dependent sum):
Σ(x:A),P(x)
Это тип пары элементов, где тип второго элемента зависит от значения первого элемента. Далее для порядка будем типы обозначать большими буквами, а значения маленькими. В идрисе зависимая пара определа так:

data Exists : (A : Type) -> (P : A -> Type) -> Type where
  Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A P

Слово Exists, как и знак Σ, появилось тут неслучайно. Логическая интепретация такой пары звучит как "существует такой x, для которого выполнено утверждение Р(х)". Сам Σ-тип становится утверждением о том, что это дело существует, а значения этого типа, пары конкретных значений, становятся доказательствами. В них первый элемент называется witness, свидетель, т.к. это конкретный пример того значения х, про которое мы утверждаем, что оно существует, а второй элемент называется proof, т.к. он служит доказательством выполненности утверждения Р для этого х. Для таких пар в идрисе есть специальный синтаксис:
(a ** b)
Аналогами функций fst и snd, извлекающих первый и второй элементы пары, служат функции getWitness и getProof:

getWitness : {P : a -> Type} -> Exists a P -> a
getWitness (a ** v) = a

getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
getProof (a ** v) = v

Теперь давайте возьмем описанные в начале поста изоморфизмы про обычные пары, и запишем их для зависимых пар:

using (A : Type, B : A->Type, C : Type)
  id3 : ((x:A ** B x) -> C) -> ((x:A) -> B x -> C)
  id3 f = \a => \b => f (a ** b)

  id4 : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)
  id4 f = \p => f (getWitness p) (getProof p)

Тела функций те же самые, просто операции с туплами поменялись на операции с зависимыми парами. Что же нам говорят типы? Что мы доказали следующее утверждение:
((∃x:A . B(x)) => C) == (∀x:A . (B(x) => C))
Это то, что позволяет в языках вроде хаскеля и окамла записывать экзистенциальные типы, обходясь без ключевого слова exists, а лишь квантором всеобщности forall.

Еще один морфизм на ту же тему:

  id5: (x:A ** (B x -> C)) -> (((x:A) -> B x) -> C)
  id5 p = \f => (getProof p) (f (getWitness p)) 

Он показывает, что
(∃x:A . (B(x) => C)) => ((∀x:A . B(x)) => C)
Говорят, что в обратную сторону тоже верно, но у меня такую функцию построить не получилось.

Comments

[thesz.livejournal.com]

Type case. Препятствует type erasure.

Хотя Брэди и написал диссертацию по устранению вычислений в области типов, но всё равно я type case не очень доверяю.

[migmit.livejournal.com]

Type erasure — это из-за которого в жабе абстракции текут?

[thesz.livejournal.com]

Нет.

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.8284

На самом деле, это мешает оптимизациям. Ещё про это Lennart Augustsson писал, в его статье про Cayenne.

[dima-starosud.livejournal.com]

Не только вы (https://lists.chalmers.se/pipermail/agda/2013/004941.html).