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

[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]

а, тьфу, это 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 всегда истинно.

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

[sassa-nf.livejournal.com]

"А вот для непустого В(х) и пустого С у нас такой функции нет."

Как нет? \x -> undefined

Раз undefined можно композировать с функцией любого типа, то должно бы годиться и для пустого типа C. Или я заблуждаюсь?

[thedeemon.livejournal.com]

А, я наврал про undefined, у нее другой тип. Нам нужна функция, делающая из В(х) пустой С, но у того нет конструкторов, его создать невозможно. undefined у нас нет, это не хаскель.

[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.