Как определяется двойственность типов?

В рекурсивных типах Wadler бесплатно! [1], он продемонстрировал два типа и , и утверждал, что они двойственны . В частности, он указал, что тип является не двойственным прежним. Кажется, что рассматриваемая двойственность отличается от дуальности Де Моргана в логике. Интересно, как определяется двойственность типов, особенно для трех упомянутых типов, почему второй является двойственным по отношению к первому, а третий - нет. Благодарю. $\forall X . (F(X) \rightarrow X) \rightarrow X$ $\exists X . (X \rightarrow F(X)) \times X$ $\exists X . X \rightarrow (X \rightarrow F(X))$

[1] http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt

lo.logic type-theory день
источник

Я не собираюсь здесь сильно помогать, но это звучит как теория.

Энтони

Ответы:

В этом контексте двойственность означает взятие наименьшей фиксированной точки в одном случае и наибольшей фиксированной точки в другом. Мы должны попытаться понять, в каком смысле и являются "наименее" и "наибольшим" решением рекурсивного уравнения . $L = \forall X . (F(X) \to X) \to X$ $G = \exists X . (X \to F(X)) \times X$ $F(X) \cong X$

Прежде всего, и действительно являются фиксированными точками (при определенных технических предположениях, которые ограничивают природу ), потому что сравнение отображает и заданное и являются изоморфизмами. Обратите внимание, что мы использовали тот факт, что является функтором, т. Е. Монотонным, когда применяем его к функциям. $L$ $G$ $F$ $v : F(L) \to L$ $w : G \to F(G)$

v x X g = g (F (λ h : L . h X g) x)

$v \, x \, X \, g = g \, (F (\lambda h : L \,.\, h \,X\, g)\, x)$

w (X, (f, x)) = F (λ y : X . (X, (f, y))) (f x)

$w (X, (f, x)) = F (\lambda y : X \,.\, (X, (f, y))) \, (f x)$

F

$F$

Пусть любого решения с посредническим изоморфизмом . Тогда у нас есть канонические карты определяемые как и Следовательно, является наименьшим, потому что мы можем отобразить из него любое другое решение, а является наибольшим, потому что мы можем отобразить из любого другого решения его. Мы могли бы сделать все это более точным, говоря о начальных алгебрах и конечных коалгебрах, но я хочу, чтобы мой ответ был коротким и приятным, и Коди все равно объяснил алгебры. $Y$ $F(Y) \cong Y$ $u : F(Y) \to Y$

α : L \to Y and β : Y \to G

$\alpha : L \to Y \text{ and } \beta : Y\to G$

α f = f Y u

$\alpha \, f = f\, Y\, u$

β y = (Y, (u^{- 1}, y)) .

$\beta \, y = (Y, (u^{-1}, y)).$

L

$L$

G

$G$

На практике наименьшее количество решений - это нетерпеливые типы данных, а наибольшие решения - это ленивые типы данных. Например, если , то в первом случае мы получаем конечные списки «s и во втором конечных и бесконечных списков » с. $F(X) = 1 + A \times X$ $A$ $A$

Андрей Бауэр
источник

В моем ответе отсутствует доказательство того, что и являются фиксированными точками (при некоторых предположениях о , которые могут остаться неустановленными). Как записать карты сравнения и ?

L

$L$

G

$G$

F

$F$

F (L) \to L

$F(L) \to L$

G \to F (G)

$G \to F(G)$

Андрей Бауэр

Хорошо, нашел карты и с Coq.

v

$v$

w

$w$

Андрей Бауэр

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

w

$w$

w^{'} (X, (f, x)) = F (λ y : X . (X, (f, x))) (f x)

$w' (X, (f, x)) = F (\lambda y : X \,.\, (X, (f, x))) \, (f x)$

Андрей Бауэр

Я предполагаю, что вы доказали, что w'это изоморфизм, но дает ли он действительную коалгебру? (Я предполагаю, что так и должно быть, но я могу ошибаться ...) Не похоже, что квадрат будет добираться.

CA McCann

В своей заметке: homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/… Вадлер дает первую версию. Однако он пишет это немного по-другому: w (X, (f, x)) = F (развернуть X k) (fx). Это делает структуру коалгебры более четкой и почти сразу же дает коммутацию соответствующих морфизмов керкурсинга. Как говорит Camcann, я думаю, что ваша другая версия не делает эти квадраты коммутирующими.

Коди

$I$ $\cal C$ $F:{\cal C}\rightarrow{\cal C}$ $F$

$A$ $\cal C$ $α : F (A) \to A$ $\alpha:F(A)\rightarrow A$
как стрелки: квадраты

$I$ $F$ $I$

$in:F(I) \rightarrow I$
$F$ $(A,\alpha)$ $fold: I\rightarrow A$

$I=\forall X.(F(X)\rightarrow X)\rightarrow X$ $fold$

f o l d = λ i : I . i A α : I \to A

$fold=\lambda i:I. i\ A\ \alpha : I\rightarrow A$

i n

$in$

F

$F$ , что можно рассматривать как требование позитивности.

$F$ $F$

$Z$ $\cal C$ $ω : Z \to F (Z)$ $\omega: Z\rightarrow F(Z)$
$F$ $\alpha$ $\beta$

$T$

$out:T\rightarrow F(T)$
$F$ $Z$ $cofold: Z\rightarrow T$

$T=\exists X.(X\rightarrow F(X))\times X$

c o f o l d = λ z : Z . (Z, ω, z) : Z \to T

$cofold = \lambda z:Z.(Z,\omega,z) : Z\rightarrow T$

T = \exists X . X \to (X \to F (X))

$T=\exists X.X\rightarrow (X\rightarrow F(X))$

Коди
источник

$\lambda$ $\pi$

Когда вы переводите (декомпозируете) типы в исчисление процессов, двойственность становится простой: входные данные двойственны выходным, и наоборот . В дуальности больше нет (много).

$\pi$ $\alpha = (Bool, Int)^{\uparrow}$ $\alpha$ $\alpha$ $x$ $\overline{x}\langle false,7\rangle$ $\overline{\alpha}$ $(v, w)$ $v$ $w$ $\overline{\alpha}$ $(bool,int)^{\downarrow}$ $\overline{\alpha}$ $x$ $c(v,w).0$

$\beta = (int, (int)^{\uparrow})^{\downarrow}$ $(v, w)$ $v$ $w$ $\overline{\beta} =(int, (int)^{\downarrow})^{\uparrow}$ $\alpha$ $\overline{\alpha}$ $P$ $\alpha$ $x$ $Q$ $\overline{\alpha}$ $x$ $P$ $Q$ $\beta$ $\overline{\beta}$

$\forall X.(X,(X)^{\uparrow})^{\downarrow}$ $(v, w)$ $v$ $X$ $w$ $X$ $x$

x (v w) . \bar{w} v

$x(vw).\overline{w}v$

\forall X . (X, (X)^{↑})^{↓}

$\forall X.(X,(X)^{\uparrow})^{\downarrow}$

Что означает универсальная количественная оценка на уровне процесса? Существует прямая интерпретация: если данные типизируются переменной типа, они не могут быть использованы как объект вывода, только как объект. Поэтому мы не можем проверить эти данные, мы можем только передать их или забыть.

$\forall X.(X,(X)^{\uparrow})^{\downarrow}$ $\exists X.(X,(X)^{\downarrow})^{\uparrow}$

Теория этого была детально разработана в [1, 2, 3] и некоторых других, более труднодоступных работах, и очень точно связана с поляризованной линейной логикой и ее понятием двойственности в 4 .

$\lambda$ $\lambda$ $\pi$ $\lambda$ $\pi$ $\lambda$

$\pi$

4 К. Хонда и др. Точное соответствие между типизированным пи-исчислением и поляризованными сетями доказательств .

5 Р. Мильнер, Функции как процессы .

Мартин Бергер
источник

re: Ваша точка зрения о количестве жителей типа ∀X. (X, (X) ↑) ↓. Существует ли аналог «свободных теорем» для пи-исчисления? Если да, где это обсуждается?

Доминик Маллиган

Здравствуйте @DominicMulligan, да, есть «свободные теоремы», и мы немного исследовали это в [1, 2]. Я думаю, что в этом направлении можно сказать гораздо больше.

Мартин Бергер

@MartinBerger: Можете ли вы использовать параметричность, чтобы выяснить, каково «правильное» понятие эквивалентности процесса для типизированного пи-исчисления? Например, в Системе F параметрическое логическое отношение соответствует контекстуальной эквивалентности. По аналогии, я ожидал бы, что любое понятие эквивалентности процесса соответствует параметрическому логическому отношению для пи-исчисления, чтобы быть особенно интересным.

Нил Кришнасвами

π

$\pi$

Характеристики, основанные на бисимуляции, полезны для практических рассуждений, потому что они не требуют замыкания во всех контекстах.

Мартин Бергер