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

[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

[sassa-nf.livejournal.com]

ага, тогда выходит ∃x:A . (B(x)=>C) == ∀x:A . (B(x)=>C) для любых C, у которых есть конструктор значений, не зависящий от x.

[thedeemon.livejournal.com]

У нас нет операции "тогда выходит". Предъявите доказательство, тогда выйдет. :) Для некоторых В(х), например пустых, доказательство строится несложно. А вот для произвольных - нет.

[sassa-nf.livejournal.com]

ага, нутк, вот я и говорю, что если у C есть конструктор, не зависящий от x, то такую функцию всегда можно построить. Думаю, это можно даже перефразировать "когда C = C'+1". Ибо с произвольными B(x) можно делать одну общую вещь: игнорировать.

upd. даже не так, а "C есть конструктор типа, не зависящий от x:A, и у него есть конструктор значений, не зависящий от y:B(x)"

[thedeemon.livejournal.com]

Неа, даже если он не зависит от х, он может иметь параметры, которые нам может быть неоткуда взять. Вот если бы у нас была на входе функция типа () -> C, ее можно было бы использовать для создания значения типа С. А в общем случае ничего такого нет. Если мы хотим доказать В => C для любых непустых В и С, нам нужно предъявить конкретную функцию-доказательство, работающую с любыми В и С. Не отдельную функцию для каждого С, а одну на всех. Такую взять негде.

[sassa-nf.livejournal.com]

совершенно согласен. я ж и попытался получить, что вывод о равенстве ∃ и ∀ годится только для случаев, когда C=C'+1, т.е. не для всех C.