Арифметика типов

[Mysterious Light]

Подкиньте, пожалуйста, литературу по типовой арифметике — формальной системе, в которой имеются сложение (альтернатива), умножение (декартово произведение), возведение в степень (тип функции) и рекурсивные типы.

Кроме этого, хотелось бы уметь в рамках такой системы доказывать, что тип data T a b = T1 a | T2 b (T a b) (нотация Haskell), он же $t = a + b t$, он же $t = \operatorname{Fix} \, (\Lambda x. a+bx)$, если последнее допускается делать, эквивалентен типу data T a b = T a [b], он же $t = a \operatorname{List}(b)$, где $\operatorname{List}(b) = 1 + b \operatorname{List}(b)$.

Ещё вопрос: благоразумно ли полагать, что тип data R = R R, он же $r = \operatorname{Fix}(\Lambda x. x)$, эквивалентен типу data Void = Void, он же синглтон $1$, или эти два типа принципиально различны по своей структуре?

[Mysterious Light]

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

(В принципе, я могу кое-что придумать сам)

Алфавит: алфавит типовых переменных $T$, $1+\times\to\sim$ и скобочки.
Грамматика: формулы (F) и равенства (E), например, в БНФ

$$F ::= T | F\to F | F+F | F\times F, \qquad E::=F\sim F$$

Аксиомы:

$$F\sim F, \quad A+B\sim B+A, \quad (A+B)+C\sim A+(B+C),$$$$1\times A \sim A, \quad A\times B\sim B\times A, \quad (A\times B)\times C \sim A\times (B\times C), \quad A\times (B+C)\sim A\times B + A\times C$$

и т.п.
Правила:

$$\frac{A\sim B\quad B\sim C}{A\sim C} \quad \frac{A\sim B}{A+C\sim B+C} \quad \frac{A+C\sim B+C}{A\sim B} \quad \frac{A\sim B}{A\times C\sim B\times C} \quad \frac{A\times C\sim B\times C}{A\sim B} \quad$$

Этого достаточно, чтобы более-менее свободно доказывать простенькие равенства. В частности, некоторые правила являются обратными другим, что основывается на том, что сложение и умножение на фиксированный (непустой) тип в определённом смысле инъективно.

Однако, проблема заключается в следующем:
Введём доп. символ $N$ и аксиому $N\sim 1+N$, описывающие тип натуральных чисел. Также введём $L$ и аксиому $L\sim a + L$, где $a$ — некоторая выделенная буква. Используя этот набор аксиом и правил, нельзя вывести $L\sim a\times N$, что очень хотелось бы.
Я экспериментирую с правилом такого вида:

$$\frac{a\sim A \quad B \sim A[a:=B]}{a\sim B}$$

где $a$ — буква, а $A$ и $B$ — формулы. Такое правило позволит доказать вышеуказанное равенство, но оно мне всё-равно не нравится, да и плохо обобщается, если вводить операторы над типами, вроде бы.

Однако, хотелось бы почитать мысли умных людей по этой же теме.

[Xaositect]

А как мы можем это отношение эквивалентности, которое мы хотим построить, определить через обычные понятия теории типов? Просто если рассматривать существование взаимно обратных функций $f\colon A\to B$ и $g\colon B\to A$, то для любых конкретных типов, если они бесконечны, вроде бы можно такое построить, но это как-то скучно.

Mysterious Light в сообщении #893650 писал(а):

Ещё вопрос: благоразумно ли полагать, что тип data R = R R, он же $r = \operatorname{Fix}(\Lambda x. x)$, эквивалентен типу data Void = Void, он же синглтон $1$, или эти два типа принципиально различны по своей структуре?

В неленивом языке он эквивалентет пустому типу $0$.

[Mysterious Light]

Xaositect в сообщении #897082 писал(а):

А как мы можем это отношение эквивалентности, которое мы хотим построить, определить через обычные понятия теории типов? Просто если рассматривать существование взаимно обратных функций $f\colon A\to B$ и $g\colon B\to A$, то для любых конкретных типов, если они бесконечны, вроде бы можно такое построить, но это как-то скучно.

Признаюсь, я сам не имею четкого представления, как его нужно понимать. Для начала можно взять то, что Вы предложили, а именно изоморфность в категории типов и $\lambda$-термов между ними.
Я не понял, почему всякие два бесконечных типа будут эквивалентны по Вашему мнению. Например, будет ли тип бинарного дерева $T_2(a) = a + (T_2(a))^2$ эквивалентен списку $L(a)=a+a\times L(a)$ для конкретного $a$? Или я Вас неправильно понял, или Вы утверждаете, что можно построить взаимооднозначное соответствие бин. дерева и списка.

Всё-таки хочется сделать акцент на некоторой натуральности таких изоморфизмов, хотя я не представляю, что именно это означает. Законы, приведённые в раннем сообщении, обосновываются обобщёнными (generic; при неявной типизации это обобщение получается само собой; при явной, стало быть, нужно абстрагироваться по всем задействованным типам) комбинаторами. Например, $\operatorname{rev} = \Lambda A\Lambda B \lambda p. \operatorname{pair}(\pi_{\rm right} p)(\pi_{\rm left} p) \; : \; \forall A\forall B. \, A\times B\to B\times A$, где $\pi_{\rm left/right}$ означает проекцию, удовлетворяет $\operatorname{rev}_{BA}\circ\operatorname{rev}_{AB}=id_{A\times B}$ и не опирается на внутреннее устройство типов $A$ и $B$, будучи натуральным преобразованием пары в пару.

Xaositect в сообщении #897082 писал(а):

Mysterious Light в сообщении #893650 писал(а):

Ещё вопрос: благоразумно ли полагать, что тип data R = R R, он же $r = \operatorname{Fix}(\Lambda x. x)$, эквивалентен типу data Void = Void, он же синглтон $1$, или эти два типа принципиально различны по своей структуре?

В неленивом языке он эквивалентет пустому типу $0$.

Логично, в неленивых языках нельзя построить экземпляр такого типа, поскольку сразу же впадаем в бесконечную рекурсию. Это же происходит, если рассматривать любые типы с потенциально бесконечными экземплярами (они называются коданными?). Однако, в леневых языках подобное определение

(upd)

Сначала хотел сказать, что то же самое, что определение типа с единственным полем-ссылкой на себя в любом языке

class R {
    public R r;
    public R() { this.r = this; }
}

Однако этот тип не соответствует ленивому data R = R R, потому что в последнем наблюдается конструктор с одним аргументом, чего нет в приведённом коде.
Можно использовать ссылки-замыкания вместо прямых ссылок, подобно тому, как реализовано в GHC хранение ленивых данных, но мы придём к тому же понятию ленивого типа.

задаёт тип, который, как мне кажется, имеет один экземпляр.

(Оффтоп)

точнее, один класс эквивалентности структурно подобных экземпляров, если так можно неформально выразиться;
это примечание нужно, чтобы исключить из рассмотрения возможность в некоторых языках дублировать/клонировать объекты или вызывать один конструктор несколько раз на одних аргументах.

Как только разрешатся вопросы из первой части, этот момент разрешится сам сабой внутри построенной системы, которая скажет, как расценивать такой тип.
Пока что этот вопрос скорее интересующий меня оффтоп.

Я описал свои соображения, основанные на том, что читал и знаю. Подскажете, что ещё можно посмотреть?

[Xaositect]

Mysterious Light в сообщении #897097 писал(а):

Я не понял, почему всякие два бесконечных типа будут эквивалентны по Вашему мнению. Например, будет ли тип бинарного дерева $T_2(a) = a + (T_2(a))^2$ эквивалентен списку $L(a)=a+a\times L(a)$ для конкретного $a$? Или я Вас неправильно понял, или Вы утверждаете, что можно построить взаимооднозначное соответствие бин. дерева и списка.

Для конкретного алгебраического $a$, мне кажется, можно. Можно же построить функции, которые однозначно нумеруют, например, $L(2)$ или $T_2(2)$ натуральными числами.

Mysterious Light в сообщении #897097 писал(а):

Логично, в неленивых языках нельзя построить экземпляр такого типа, поскольку сразу же впадаем в бесконечную рекурсию. Это же происходит, если рассматривать любые типы с потенциально бесконечными экземплярами (они называются коданными?). Однако, в леневых языках подобное определение или, что то же самое, определение типа с единственным полем-ссылкой на себя в любом языке задаёт тип, который, как мне кажется, имеет один экземпляр.
точнее, один класс эквивалентности структурно подобных экземпляров, если так можно неформально выразиться;

Ну, если взять тот же Haskell, то там получится $\perp$ (незавершающееся вычисление, undefined), $R{\perp}$, $R(R{\perp})$ и т.п.

Цитата:

Я описал свои соображения, основанные на том, что читал и знаю. Подскажете, что ещё можно посмотреть?

Не знаю, я читал только базовые книги типа Барендрегта и разные блоги по категории типов Haskell. Ничего такого я там не видел. Ну то есть есть https://chris-taylor.github.io/blog/201 ... ata-types/ , но это в другую сторону.

Mysterious Light в сообщении #896661 писал(а):

Введём доп. символ $N$ и аксиому $N\sim 1+N$, описывающие тип натуральных чисел. Также введём $L$ и аксиому $L\sim a + L$, где $a$ — некоторая выделенная буква. Используя этот набор аксиом и правил, нельзя вывести $L\sim a\times N$, что очень хотелось бы.

А это, кстати, понятно почему. Одна аксиома $N\sim 1 + N$ или $L\sim a + L$ не задает тип однозначно. С помощью Выших аксиом мы можем доказать, что $a\times N$ удовлетворяет соотношению $X = a + X$, но не можем отождествить его с $L$. Я вообще плохо представляю, как выразить минимальность рекурсивного типа, используя только равенства.

-- Пн авг 18, 2014 18:21:15 --

Есть еще Homotopy type theory, там это как раз можно выразить как равенство типов, но там все сложно, одними аксиомами с равенством не обойдешься.

[Mysterious Light]

Между конечными деревьями и конечными списками можно построить взаимооднозначное соответствие. Однако, потенциально бесконечные объекты уже не будут сопоставляться, вроде бы. Даже если вовлечь экспоненты, вроде $\operatorname{Nat}\to 2$, задача построения биекции в разы усложнится.

Xaositect в сообщении #897099 писал(а):

Ну, если взять тот же Haskell, то там получится $\perp$ (незавершающееся вычисление, undefined), $R{\perp}$, $R(R{\perp})$ и т.п.

В Haskell $\bot$ в принципе является экземпляром некоторого типа, тем не менее, несколько ущербным, как бы так выразиться по-лучше. В вопросах вычислимости/невычислимости я не разбираюсь, но на интуитивном уровне понимаю так:
Можно написать несколько функций так, что на аргументах $\bot, R\bot, R(R\bot)$ и $\operatorname{fix} R$ они будут по-разному реагировать (имеется в виду, возвращать $\bot$ или возвращать нормальное значение).

Xaositect в сообщении #897099 писал(а):

Не знаю, я читал только базовые книги типа Барендрегта и разные блоги по категории типов Haskell. Ничего такого я там не видел. Ну то есть есть https://chris-taylor.github.io/blog/201 ... ata-types/ , но это в другую сторону.

Интересная ссылка. В начале автор делает некоторые рассуждения, как бы вводя алгебру, причём делает некоторые «дикие» шаги, вроде вычитания и деления. Как раз из этих общих рассуждений я и исходил, но интересует формализация, которая бы позволила автоматически выводить равенства, строго и формально.
Интересная ссылка на «Семь деревьев в одном».
В конце описываются производные типов. Кстати, не далее, как 2 недели назад, попалась статья Conor McBride The Derivative of a Regular Type is its Type of One-Hole Contexts, где автор пробует формализовать однодырочный контекст и производную.
upd. Что интересно, в этой статье автор использует нотацию $\mu y. \, T$ для обозначения рекурсивного типа $F$, удовлетворяющего $F = T[y:=F]$. То есть он не вводит операторы над типами и оператор Fix, а как бы упрощённо вводит рекурсию в систему типов.

Xaositect в сообщении #897099 писал(а):

Есть еще Homotopy type theory, там это как раз можно выразить как равенство типов, но там все сложно, одними аксиомами с равенством не обойдешься.

Спасибо, посмотрю.

Xaositect в сообщении #897099 писал(а):

Одна аксиома $N\sim 1 + N$ или $L\sim a + L$ не задает тип однозначно. С помощью Выших аксиом мы можем доказать, что $a\times N$ удовлетворяет соотношению $X = a + X$, но не можем отождествить его с $L$. Я вообще плохо представляю, как выразить минимальность рекурсивного типа, используя только равенства.

Да, из $X = a + X$ и $L = a + L$ нельзя на основании имеющихся аксиом отождествить $X$ и $L$. Поэтому система должна располагать каким-то механизмом, который позволил бы делать такие заключения. В данном случае это мне кажется правильным.
Или, например, из $X = a \times X + b$ и $L = a \times L + b$ отождествлять $X$ и $L$ при $a\neq 0$.
А вот из $a\times X = b\times X$ и $a\times L = b\times L$ отождествление уже не уместно, разве что только при $a=b\neq 0$ (можно сократить). Хотя здесь всё только на словах.

В целом, думаю, Вы поняли суть моего вопроса. Особо меня интересует случай системы с операторами над типами.

[Xaositect]

Mysterious Light в сообщении #897126 писал(а):

Между конечными деревьями и конечными списками можно построить взаимооднозначное соответствие. Однако, потенциально бесконечные объекты уже не будут сопоставляться, вроде бы. Даже если вовлечь экспоненты, вроде $\operatorname{Nat}\to 2$, задача построения биекции в разы усложнится.

Да, так не получается.

Давайте попробуем сформулировать задачу формально.
У нас есть система типов, включающая суммы и произведения, можно определять конструкторы типов, например $Pair = \Lambda x. x + x$, а также рекурсивные типы $\mu x. F(x)$ и/или корекурсивные типы $\nu x. F(x)$. Вот эти $F$ - это и есть конструкторы типов, возможно их там надо ограничить только ковариантными функторами.
Эта система вложена в систему типов, в которой разрешены еще полиморфные типы $\forall x. F(x)$. Два типа $F(A,B,\dots)$ и $G(A, B, \dots)$ со свободными переменными $A, B, \dots$ назовем эквивалентными, если существуют полиморфные функции $\forall A \forall B . F(A, B,\dots) \to G(A, B, \dots)$ и наоборот, задающие изоморфизм.
Надо как-то попроще задать это отношение эквивалентности, не упоминая эти полиморфные функции и эту внешнюю систему типов, в которую они входят.

Надо подумать над этим.

[Xaositect]

Я тут подумал, что похоже $a\times \mu x. 1 + b\times x = \mu x . a + b\times x$ это скорее всего почти единственное соотношение,в котором и в левой, и в правой части есть один рекурсивный тип.
Если мы рассмотрим тип $\mu x. P(x)$, где $P(x)$ - некоторый многочлен, то это получается деревья, у которых каждой степени вершины соответствует некоторый тип, который в вершине этой степени может находиться и однозначно этим набором типов определяется. А кроме списков, все остальные деревья могут иметь произвольное количество вершин любой степени и из них ничего вынести не получится.
Осталось понять, как такие деревья преобразуются при сложении, умножении и композиции.

-- Пн авг 25, 2014 19:10:47 --

Еще нагуглил книгу по теме: R. Di Cosmo "Isomorphisms of Types: from $\lambda$-calculus to information retrieval and language design". Пока не читал.

[Joker_vD]

Если я не ошибаюсь, рекурсивные типы можно представлять как финальные алгебры в подходящей замкнутой декартовой категории (closed-cartesian categories, CCC, их вообще принято использовать для моделирования систем типов).

Возможно, T. Hagino "A typed lambda calculus with categorical type constructors" будет интересен? Статьи по сравнению индуктивних типов с коиндуктивными?

[Joker_vD]

Собственно, B. Jacobs, J. Rutten "A Tutorial on (Co)Algebras and (Co)Induction". Берем полиномиальный функтор $T(X)$ (например, $T(X)=1+(A\times X)$), для него определяем $T$-алгебры, т.е. пары $(U, a)$, где $a\colon T(U)\to U$. Вводим понятие морфизмов $T$-алгебр $a\colon T(U)\to U$ и $b\colon T(V)\to V$ как функции $f\colon U\to V$ такой, что $f\circ a = b \circ T(f)$:

$$\xymatrix{T(U) \ar[r]^{T(f)} \ar[d]_{a}& T(V) \ar[d]_{b} \\ U \ar[r]_f & V}$$

Определяем начальную $T$-алгебру $a\colon T(U)\colon U$ как такую $T$-алгебру, что для каждой $T$-алгебры $b\colon T(V)\to V$ найдется единственный морфизм $f\colon U\to V$, который делает диаграмму выше коммутативной.

Так вот, у начальной $T$-алгебры $a\colon T(U)\to U$ вот эта вот функция $a$ является изоморфизмом объектов $T(U)$ и $U$, т.е. начальная $T$-алгебра является неподвижной точкой функтора $T$. В случае функтора $T(X)=1+(A\times X)$ его начальной алгеброй является пара $(A^{\star},[\mathrm{nil},\mathrm{cons}])$, где $A^{\star}=\bigcup\limits_{n\in\mathbb N}A^n$ — звезда Клини $A$, $\mathrm{nil}\colon 1\to A^{\star}$, $\mathrm{cons}\colon A\times A^{\star}\to A^{\star}$ — конструкторы списков, а $[\mathrm{nil},\mathrm{cons}]\colon 1+A\times A^{\star}\to A^{\star}$ — их прямая сумма.

[Mysterious Light]

Joker_vD
Спасибо, весьма интересная ссылка на B. Jacobs, J. Rutten "A Tutorial on (Co)Algebras and (Co)Induction". Я с алгеброй не дружу, а тут такое интересное применение более обобщенного понятия. Я только половину прочитал, но уже впечатлён теоремой о том, что инициальная $T$-аглебра является изоморфизмом в исходной категории, очень красивое и лёгкое доказательство. И вывод из теоремы красивый: это неподвижная точка эндофунктора.
Однако, некоторые моменты мне остались непонятны. Понятно, что основной акцент авторы делали на подачу материала и мало затрагивали собственно теоретико-категорные понятия. По контексту понятно, что речь идёт о категории множеств, но всё легко обобщается до типов. Какие требования к категории авторы подразумевают? Наличие простеньких (ко)пределов?

Есть только проблема, что определение не предполагает какого-либо метода для конструирования подобных алгебр. Об этом говориться в самой статье и даются ссылки на попытки в частном случае дать конструктивную алгебраическую формулу. Хотя мне думается, что для типов будут свойственны свои особенности, которых нет у множеств. В общем, этот момент тёмный для меня.

Другие статьи посмотрю позже.

(Оффтоп)

Joker_vD писал(а):

замкнутой декартовой категории (closed-cartesian categories, CCC, их вообще принято использовать для моделирования систем типов).

Хочу кое-что уточнить:
в книги Голдблатта Топосы... понятие д.з.к. включает в себя конечную полноту, которой категория типов не обладает, поскольку не имеет всех обратных образов (pullback), википедия и некоторые другие источники этого не требуют.
Как более общепринято? Или этот вопрос из ряда «является ли 0 натуральным числом»?