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

[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

[migmit.livejournal.com]

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

Если C имеет только одно значение, то справа стоит единственный элемент, а слева - целое A. Так что и не получится.

[thedeemon.livejournal.com]

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

[sassa-nf.livejournal.com]

а как тип id6 должен выглядеть? я могу построить id6: (((x:A) -> B x) -> C) -> (x:A) -> (B x -> C)

id6 f = \x => g where
  g b = f (\y => b)

что только что было доказано изоморфно искомому?

[sassa-nf.livejournal.com]

а, это не одно и то же. сгодится только если (B x) одинаковое во всех местах в типе id6.

[thedeemon.livejournal.com]

Нужен
(((x:A) -> B x) -> C) -> (x:A ** (B x -> C))
Т.е. результатом должна быть зависимая пара, а не функция.

[migmit.livejournal.com]

Гррр. Ещё раз: "Так что и не получится".

[sassa-nf.livejournal.com]

ну по id3 это не должно иметь значения?..

[dima-starosud.livejournal.com]

В обратную сторону для любых A B C доказать нельзя, контрпример:
A - не населенный;
C - населенный;
B - любой;
Тогда функция с типом ((∀x:A . B(x)) => C) существует, но значение с типом (∃x:A . (B(x) => C)) построить нельзя, поскольку нельзя найти x:A.
Т.е. если просто, выходит True => False

[thedeemon.livejournal.com]

Я знаю, что не получится, но потому что там "C имеет только одно значение". Там функция же, а не одно значение.

[thedeemon.livejournal.com]

не понял вопроса

[sassa-nf.livejournal.com]

нужен CPT?

id6 f = ( x ** g ) where
  g b = f g'
  g' x = b

чтобы ( x ** g ), x и b были из одного closure. (то есть, это ерунда, а не код, но идея такова)

Или это не CPT называется?

[thedeemon.livejournal.com]

Ага.

Я, кстати, уже после того, как код для этого поста написал, увидел аналогичный пост у вас в блоге, только там Агда.

[migmit.livejournal.com]

Закусывать надо.

C, по условию, произвольный тип. Значит, в частности, должно работать в случае, когда C имеет лишь одно значение.

[thedeemon.livejournal.com]

Пойду закусывать. Действительно неправильно ваш первый коммент прочитал.

[thedeemon.livejournal.com]

Надо подумать. Только рядом вон уже показали по всякому, что ничего не должно получаться.

[dima-starosud.livejournal.com]

А что значит "слева С, а справа целое А"?
(∃x:A . (B(x) => C)) - это целое А?

[sassa-nf.livejournal.com]

Вот, или вот так

id6 f = ( x ** g ) where
  g b = f (\x => b)

Чтобы "вычислить" witness, нужно вызвать f, но "выскочить" из него, как только f передаёт готовый x (и continuation (B x->C)); чтобы g могло "вычислить" C, нужно в continuation вбросить proof, который должен "поступить" в g извне.

На пальцах - Я вам дам witness, а вы мне дайте proof, тогда я вам дам C. То есть, механизм доказательства оказыватся "снаружи" id6.

[sassa-nf.livejournal.com]

А как быть с continuation passing? Или оно не описывается этой теорией?

(вызвать f, выскочить из него, когда известно x - это witness; далее, когда в proof "вбросят" B x, вернуться в f и узнать C - т.о. способ связи x:A и (B x) полностью снаружи id6)

[sassa-nf.livejournal.com]

да оно получаться, наверное, и не должно. Например, нигде не сказано, что f "вызывает" свою функцию только один раз, хотя вполне может производить какое-то одно C.

[thedeemon.livejournal.com]

Чтобы вызвать f, нужно где-то взять для нее аргумент - функцию, умеющую из x делать В х. Таковую взять уже неоткуда, а иную тип f не позволяет принять..

Если попытаться вывернуть все наизнанку с CPT, типы же поменяются, мы уже другое утверждение будем доказывать.

[sassa-nf.livejournal.com]

Как неоткуда? Current continuation и есть эта функция (x:A ** (B x -> C)) (т.е. функция "дай мне x:A и куда вбрасывать (B x)your continuation")

Другое дело, что поскольку связь между x:A и (B x) - снаружи, то сама функция ничего не доказывает - доказательство-то возможности построить (B x) снаружи.


Типы от CPT поменяются, но должна же где-то быть теорема об изоморфизме. Или её нету?

[sassa-nf.livejournal.com]

или так: если CPT строит не изоморфное доказательство, то на каком основании мы им пользуемся вообще где-то?

[sassa-nf.livejournal.com]

...which means

id6 = call-cc

[thedeemon.livejournal.com]

Че-то я торможу. Можно подробнее?
Вон нам дали функцию f типа ((x:A) -> B x) -> C. Она хочет аргумент типа (x:A) -> B x. Наши действия?

Про изоморфизм CPT вопрос хороший, нужно изучить.

[dima-starosud.livejournal.com]

И что лучше? *спрашиваю не холивара ради =)
Посоветуйте, пожалуйста, что-то маленькое почитать, чтобы все стало достаточно ясно о Идрис.