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

[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

[dima-starosud.livejournal.com]

Вас смущает, что на всех (х:А) есть только одно (B(x) => C)? Но это не страшно, рассмотрите например (∃x:A . True): берете любое (х:А) и единственный экземпляр из True и составляете пару - никаких проблем.

*(но так штука в обратную сторону конечно же не доказывается)

[migmit.livejournal.com]

Вам тоже надо закусывать. Вы зачем-то решили доказать моё утверждение, что между A и (∃x:A . (B(x) => C)) нет никакой разницы.

[dima-starosud.livejournal.com]

...а вам бы четче выражать свои мысли.

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

Еще раз, пожалуйста, поясните что вы хотели сказать этой фразой.

[migmit.livejournal.com]

Скажите, что именно можно было неправильно понять?

1) Процитирована формула (∃x:A . (B(x) => C)) => ((∀x:A . B(x)) => C) и фраза, говорящая, что, якобы, наоборот тоже верно. Таким образом в этой формуле явно выделены (топикстартером) две части: левая (∃x:A . (B(x) => C)) и правая ((∀x:A . B(x)) => C).

2) Моё утверждение содержит посылку: допустим, что C — тип, имеющий лишь одно значение. Надеюсь, не надо обосновывать существование таких типов.

3) Из этой посылки выводятся два заключения:

3.1) Правая часть (т.е., (∀x:A . B(x)) => C) также является типом, имеющим лишь один элемент.

3.2) Левая часть (∃x:A . (B(x) => C)), по существу, совпадает с A (изоморфна). Одну из половинок изоморфизма вы, собственно, и построили.

4) Из 3.1 и 3.2 делается вывод, что построить функцию из правой части в левую не получится. Собственно, в процитированном мною топикстартер отмечает, что у него не получилось её построить, я же обосновываю, почему и не получится.

Объясните, пожалуйста, что здесь можно понять другим способом, и каким именно?

[thedeemon.livejournal.com]

Так реально понятнее.

[migmit.livejournal.com]

Вполне допускаю, но как ещё можно было понять первый вариант?

[dima-starosud.livejournal.com]

Из ваших рассуждений, я так понимаю, можно заменить (для простоты и без убытка):
(∃x:A . (B(x) => C)) на A
(∀x:A . B(x)) => C) на C
Вы утверждаете, что нельзя построить функцию f : C => A, потому что в С одно значение, а в А может быть много?
Но это не так (т.е. для почти всех А можно), но нельзя построить только тогда, когда А пустое.
Или я опять не так понял?

[migmit.livejournal.com]

> можно заменить (для простоты и без убытка):
> (∃x:A . (B(x) => C)) на A

Да, если C содержит только одно значение.

> (∀x:A . B(x)) => C) на C

Да, если C содержит только одно значение.

> Вы утверждаете, что нельзя построить функцию f : C => A, потому что в С одно значение, а в А может быть много?

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

В частности — потому, что в A может вообще не быть элементов, да.

[dima-starosud.livejournal.com]

Теперь, все ясно, спасибо =)

*еще я понял почему я не сразу понял:
> Иначе говоря, невозможно предъявить универсальный способ выбрать элемент откуда угодно.
Это, вообще говоря, очень слабое утверждение, оно меня и смутило, по-этому я и засомневался в правильности ваших доводов.
*(я понимаю, что мы тут в интуиционизме, но ничто же не мешает смотреть шире)

[thedeemon.livejournal.com]

Нужно же не любую функцию, а чтобы ее композиция с обратной давала id, нам нужен изоморфизм же. Т.е. она не должна терять информацию, и не должна придумывать ее из неоткуда.

[dima-starosud.livejournal.com]

хм... а как же proof irrelevance?
может быть я что-то в топике упустил, но зачем изоморфизм?

[thedeemon.livejournal.com]

Типы эквивалентны, когда между ними есть изоморфизмы. Есть другие предложения?

[dima-starosud.livejournal.com]

*(тут очень разные и несвязные мысли - пункты)
1. Понятно, но это относится к изначальной задаче (эквивалентность (∃x:A . (B(x) => C)) и ((∀x:A . B(x)) => C)).
Я думал вы имеете ввиду построение функции (C => A) как отдельную задачу, тогда не имеет значение какая именно функция, но лишь ее существование.

2. Насчет изоморфизмов: задача доказательства эквивалентности типов и задача доказательства эквивалентности задач доказательства населенности типов - это разные вещи.
Тут второе (по Карри-Говарду): т.е. доказать, что из того что тип Т1 населен выводится что Т2 тоже населен. Пример Bool и Int - справились без изоморфизма:
f1 : Bool => Int
f1 _ = 1
f2 : Int => Bool
f1 _ = true

3. Для доказательства эквивалентности типов существование обратной функции не обязательно, пример тип целых и тип рациональных - мы знаем что они эквивалентны. Допустим то, что с целых в рациональные мы уже нашли функцию f1, а с рациональных в целые возьмем таким образом:
f2 : Q => Z
f2 x = [x] -- [_] - дробная часть.
Эта функция не имеет обратной, но хорошо вписывается в доказательство: из f1 и f2 получаем эквивалентность Q и Z.

[thedeemon.livejournal.com]

3. Я пока не вижу, как эти две функции нам дают эквивалентность. Как вы ее определяете?

[dima-starosud.livejournal.com]

*(там ошибка, я имел ввиду целая часть, а не дробная, но я думаю, вы правильно поняли)

Определение функции для целой части не имеет значения. Я имел ввиду теорему Кантора — Бернштейна (http://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D0%B0%D0%BD%D1%82%D0%BE%D1%80%D0%B0_%E2%80%94_%D0%91%D0%B5%D1%80%D0%BD%D1%88%D1%82%D0%B5%D0%B9%D0%BD%D0%B0), которая для доказательства эквивалентности множеств оперирует инъекциями, а не биекциями.

[thedeemon.livejournal.com]

Мне интересно ваше определение эквивалентности типов.
Инъекции тут я тоже не вижу. f2 2.5 и f2 2.4 отобразятся в один элемент, такая функция не инъективна.

Опять же, применимость этой теоремы к типам, а не множествам, вызывает большие сомнения.

[sassa-nf.livejournal.com]

"(∃x:A . (B(x) => C)), по существу, совпадает с A"

а почему A? я думал B(x)?

[thedeemon.livejournal.com]

Если С == () (одноэлементный тип), то
(B(x)->C) == (),
(∃x:A . (B(x) => C)) == (∃x:A . ()) == (A, ()) == A

[sassa-nf.livejournal.com]

а, тьфу, это C -> B(x) был бы размером с B(x).

А как здесь интерпретировать вариант, когда B(x) - пустой тип? Это же означало бы "¬∃x:A . (B(x) => C)" (в "обычной" логике, да?)

[thedeemon.livejournal.com]

Из лжи следует все что угодно. В стандартной библиотеке даже функция для этого есть:
FalseElim : _|_ -> a
Таким образом, предъявить функцию типа B(x) => C не проблема, и туплов таких понастроить можно для любого х. Как правильно их интерпретировать, сейчас сходу не скажу. Отрицание было бы, если бы мы могли из этой пары получить значение типа B(x) (или _|_, что то же самое).

[sassa-nf.livejournal.com]

у меня в голове пока не упаковалось.

в чём же тогда разница между ∃ x:A . B(x) => C и ∀ x:A . B(x) => C? Из лжи-то следует что угодно, да, но ведь тогда B(x) => C истинно для всех x:A...

[thedeemon.livejournal.com]

Когда ∀x:A . B(x) => C это тип (x:A) -> (B(x) -> C). Exists - пара, forall - функция. Тип такой функции говорит: из любого х:А мы можем построить то-то, и конкретное значение такого типа, функция, показывает, как именно конструктивно там все строится.

[sassa-nf.livejournal.com]

Не, не понятно. (про реализацию функции как значение такого типа понятно)

1. Утверждение B(x) => C означает.... что мы всегда можем построить некое c:C, если дано b:B(x). Плюс если B(x) - пустое, то это не отрицает утверждения (т.е. из лжи следует что угодно).


2. Утверждение ∃x:A . B(x) => C означает .... что оно истинно, если существует x:A, для которого B(x) => C можно построить. Но поскольку B(x) => C построить можно всегда, включая случай, когда B(x) - пустой тип, то это означает, что утверждение эквивалентно ∀x:A . B(x) => C.

Видимо, мой вопрос можно перефразировать так: эта эквивалентность утверждений существует для любого B(x)=>C? Например, включая B(x)=>C(x)? А в чём разница между этим и просто B(x), который был бы равен ()=>B(x)?


3. Ну и как выглядит реализация B(x) => C, если B(x) - пустой тип. Напрашивается функция undefined, ибо единственная стрелка из инициального объекта; но тогда что такого сообщает нам утверждение ∃x:A . B(x) => C? Я как-то расчитывал увидеть "железное доказательство, что эта ф-ция не undefined", а выходит не совсем так.

[thedeemon.livejournal.com]

Пока мы не представим доказательство для B(x) => C, конкретную функцию такого типа, это утвердждение не доказано. Для пустого B(x) у нас есть такая функция - FalseElim, она же undefined в хаскеле. А вот для непустого В(х) и пустого С у нас такой функции нет. Т.е. нельзя утверждать, что утверждение B(x) => C всегда истинно.

И следует отойти от понятий "истинно / не истинно", а использовать "доказано / не доказано".

[thedeemon.livejournal.com]

Фишка в том, что это получится уже просто тупл типа (А, True), который эквивалентен просто А, изоморфизмы между ними элементарнейшие. (считая True типом-синглтоном, как это кажется сделано в агде, но не в идрисе)