Теория зависимого типа и функции произвольного типа
Мой первый ответ на этот вопрос был высоким на концепциях и низким уровнем детализации и отражал подвопрос «что происходит?»; этот ответ будет таким же, но сфокусирован на вопросе: «можем ли мы получить функции произвольного типа?».
Одним из расширений алгебраических операций суммы и произведения являются так называемые «большие операторы», которые представляют сумму и произведение последовательности (или, в более общем случае, сумму и произведение функции над областью), обычно записываемой Σ
и Π
соответственно. См. Сигма нотация .
Итак, сумма
a₀ + a₁X + a₂X² + ...
может быть написано
Σ[i ∈ ℕ]aᵢXⁱ
где a
- это, например, некоторая последовательность действительных чисел. Продукт будет представлен аналогично с Π
вместо Σ
.
Когда вы смотрите с расстояния, выражение такого типа очень похоже на «произвольную» функцию в X
; конечно, мы ограничены выразимыми рядами и связанными с ними аналитическими функциями. Это кандидат на представление в теории типов? Определенно!
Класс теорий типов, которые имеют непосредственные представления этих выражений, является классом теорий «зависимых» типов: теорий с зависимыми типами. Естественно, у нас есть термины, зависящие от терминов, и в таких языках, как Haskell, с функциями типов и определением типов, терминами и типами в зависимости от типов. В зависимом окружении у нас также есть типы в зависимости от условий. Haskell не является языком с зависимой типизацией, хотя многие свойства зависимых типов можно смоделировать , немного помучив язык .
Карри-Ховард и зависимые типы
«Изоморфизм Карри-Говарда» начал свою жизнь как наблюдение того, что термины и правила оценки типов лямбда-исчисления с простыми типами в точности соответствуют естественному дедукции (сформулированной Генценом), примененной к интуиционистской логике высказываний, причем типы принимают место предложений и термины, заменяющие доказательства, несмотря на то, что оба они были изобретены / открыты независимо друг от друга. С тех пор это стало огромным источником вдохновения для теоретиков типов. Одна из наиболее очевидных вещей, которую следует рассмотреть, - может ли и как это соответствие для логики высказываний быть распространено на логики предикатов или логики более высокого порядка. Теории зависимого типа изначально возникли на этом пути исследования.
Для ознакомления с изоморфизмом Карри-Ховарда для простейшего типа лямбда-исчисления см. здесь . Например, если мы хотим доказать A ∧ B
, мы должны доказать A
и доказать B
; комбинированное доказательство - это просто пара доказательств: по одному на каждое соединение.
При естественном удержании:
Γ ⊢ A Γ ⊢ B
Γ ⊢ A ∧ B
и в простом наборе лямбда-исчисления:
Γ ⊢ a : A Γ ⊢ b : B
Γ ⊢ (a, b) : A × B
Аналогичные соответствия существуют для ∨
и типов сумм, →
и типов функций, а также различных правил исключения.
Недоказуемое (интуитивно ложное) суждение соответствует необитаемому типу.
Имея в виду аналогию типов как логических суждений, мы можем начать думать о том, как моделировать предикаты в мире типов. Есть много способов, которыми это было формализовано (см. это введение к Интуиционистской Теории Типа Мартина-Лёфа для широко используемого стандарта), но абстрактный подход обычно отмечает, что предикат подобен предложению со свободным термином переменные или, альтернативно, функция, принимающая термины в суждения. Если мы допустим, чтобы выражения типов содержали термины, то обработка в стиле лямбда-исчисления сразу же представилась бы возможностью!
Учитывая только конструктивные доказательства, что составляет доказательство ∀x ∈ X.P(x)
? Мы можем думать об этом как о функции доказательства, переводя члены (x
) в доказательства их соответствующих предложений (P(x)
). Таким образом, члены (доказательства) типа (предложения) ∀x : X.P(x)
являются «зависимыми функциями», которые для каждого x
в X
дают член типа P(x)
.
А как насчет ∃x ∈ X.P(x)
?Нам нужен любой член X
, x
вместе с доказательством P(x)
.Таким образом, члены (доказательства) типа (предложения) ∃x : X.P(x)
являются «зависимыми парами»: выделенный термин x
в X
вместе с термином типа P(x)
.
Обозначения: Iбудет использовать
∀x ∈ X...
для фактических утверждений о членах класса X
и
∀x : X...
для выражений типа, соответствующих универсальному количественному определению над типом X
.Аналогично для ∃
.
Комбинаторные соображения: произведения и суммы
Так же как соответствие типов Карри-Ховарда с предложениями, мы имеем комбинаторное соответствие алгебраических типов с числами и функциями,что является основным пунктом этого вопроса.К счастью, это может быть расширено до зависимых типов, описанных выше!
Я буду использовать обозначение модуля
|A|
, чтобы представить «размер» типа A
, чтобы сделать явнымсоответствие, изложенное в вопросе, между типами и числами.Обратите внимание, что это понятие вне теории;Я не утверждаю, что в языке должен быть какой-либо такой оператор.
Давайте посчитаем возможные (полностью сокращенные, канонические) члены типа
∀x : X.P(x)
, который является типом зависимогофункции, принимающие термины x
типа X
в термины типа P(x)
.Каждая такая функция должна иметь выход для каждого члена X
, и этот вывод должен быть определенного типа.Таким образом, для каждого x
в X
это дает |P(x)|
«вариантов» вывода.
Изюминка -
|∀x : X.P(x)| = Π[x : X]|P(x)|
, что, конечно, не имеет большого значенияимеет смысл, если X
равно IO ()
, но применимо к алгебраическим типам.
Аналогично, термин типа
∃x : X.P(x)
является типом пар (x, p)
с p : P(x)
, поэтому с учетом любого x
в X
мы можем построить подходящую пару с любым членом P(x)
, что дает |P(x)|
'выборы'.
Следовательно,
|∃x : X.P(x)| = Σ[x : X]|P(x)|
с такими же оговорками.
Это оправдывает общее обозначение зависимых типов в теориях, использующих символы Π
и Σ
, и на самом деле многие теории стирают различие между «для всех» и «продуктом» имежду «есть» и «сумма» из-за вышеупомянутых соответствий.
Мы приближаемся!
Векторы: представляющие зависимые кортежи
Можем ли мы теперь кодироватьчисловые выражения типа
Σ[n ∈ ℕ]Xⁿ
как выражения типа?
Не совсем.Хотя мы можем неофициально рассмотреть значение таких выражений, как Xⁿ
в Haskell, где X
- это тип, а n
- натуральное число, это злоупотребление нотацией;это выражение типа, содержащее число: отчетливо не допустимое выражение.
С другой стороны, с зависимыми типами на рисунке, типы, содержащие числа, - это как раз точка;на самом деле, зависимые кортежи или «векторы» являются очень часто цитируемым примером того, как зависимые типы могут обеспечить прагматическую безопасность на уровне типов для таких операций, как доступ к списку .Вектор - это просто список вместе с информацией на уровне типов относительно его длины: именно то, что мы ищем для выражений типа, таких как Xⁿ
.
Для продолжительности этого ответа пусть
Vec X n
будет типом длины- n
векторов значений X
-типа.
Технически n
здесь, вместо фактического натурального числа, представление всистема натурального числа.Мы можем представить натуральные числа (Nat
) в стиле Пеано как ноль (0
) или преемник (S
) другого натурального числа, а для n ∈ ℕ
я пишу ˻n˼
, чтобы обозначить термин в Nat
, что представляет n
.Например, ˻3˼
равно S (S (S 0))
.
Тогда у нас есть
|Vec X ˻n˼| = |X|ⁿ
для любых типов n ∈ ℕ
.
Nat: продвижение ℕ терминов в типы
Теперь мы можем кодировать выражения вроде
Σ[n ∈ ℕ]Xⁿ
как типы. Это конкретное выражение приведет к типу, который, конечно, изоморфен типу списков X
, как указано в вопросе. (Не только это, но и с точки зрения теории категорий, функция типа - которая является функтором - перевод X
к указанному выше типу естественно изоморфна в Список функтор.)
Последний фрагмент головоломки для «произвольных» функций - как кодировать, для
f : ℕ → ℕ
выражения типа
Σ[n ∈ ℕ]f(n)Xⁿ
, чтобы мы могли применять произвольные коэффициенты к степенному ряду.
Мы уже понимаем соответствие алгебраических типов числам, что позволяет нам сопоставлять типы с числами и функции типов с числовыми функциями. Мы также можем пойти другим путем! - если взять натуральное число, то, очевидно, существует определимый алгебраический тип с таким количеством членов-членов, независимо от того, есть у нас зависимые типы или нет. Мы можем легко доказать это вне теории типов по индукции. Нам нужен способ отображения натуральных чисел на типы, внутри системы.
Приятное осознание состоит в том, что, как только у нас появляются зависимые типы, доказательство по индукции и построение по рекурсии становятся очень похожими - на самом деле, это одно и то же во многих теориях. Поскольку мы можем по индукции доказать, что существуют типы, которые удовлетворяют нашим потребностям, разве мы не можем их построить?
Существует несколько способов представления типов на уровне терминов. Я буду использовать здесь воображаемую запись Хаскеллиша с *
для вселенной типов, которая обычно считается типом в зависимом окружении. 1
Аналогично, существует также, по крайней мере, столько способов записать 'ℕ
-элиминацию', сколько существует зависимых теорий типов. Я буду использовать Haskellish для сопоставления с образцом.
Нам нужно отображение α
от Nat
до *
, со свойством
∀n ∈ ℕ.|α ˻n˼| = n.
Достаточно следующего псевдоопределения.
data Zero -- empty type
data Successor a = Z | Suc a -- Successor ≅ Maybe
α : Nat -> *
α 0 = Zero
α (S n) = Successor (α n)
Итак, мы видим, что действие α
отражает поведение преемника S
, что делает его своего рода гомоморфизмом. Successor
- это функция типа, которая «добавляет единицу» к числу членов типа; |Successor a| = 1 + |a|
для любого a
с заданным размером.
Например α ˻4˼
(что α (S (S (S (S 0))))
), это
Successor (Successor (Successor (Successor Zero)))
и условия этого типа
Z
Suc Z
Suc (Suc Z)
Suc (Suc (Suc Z))
дает нам ровно четыре элемента: |α ˻4˼| = 4
.
Аналогично, для любого n ∈ ℕ
у нас есть
|α ˻n˼| = n
по мере необходимости.
- Многие теории требуют, чтобы члены
*
были просто представителями типов, а операция предоставляется в виде явного отображения терминов типа *
в связанные с ними типы. Другие теории допускают, чтобы сами литеральные типы были сущностями уровня термина.
'Произвольные' функции?
Теперь у нас есть аппарат для выражения общего общего степенного ряда как типа!
Серия
Σ[n ∈ ℕ]f(n)Xⁿ
становится типом
∃n : Nat.α (˻f˼ n) × (Vec X n)
, где ˻f˼ : Nat → Nat
- некоторое подходящее представление на языке функции f
. Мы можем видеть это следующим образом.
|∃n : Nat.α (˻f˼ n) × (Vec X n)|
= Σ[n : Nat]|α (˻f˼ n) × (Vec X n)| (property of ∃ types)
= Σ[n ∈ ℕ]|α (˻f˼ ˻n˼) × (Vec X ˻n˼)| (switching Nat for ℕ)
= Σ[n ∈ ℕ]|α ˻f(n)˼ × (Vec X ˻n˼)| (applying ˻f˼ to ˻n˼)
= Σ[n ∈ ℕ]|α ˻f(n)˼||Vec X ˻n˼| (splitting product)
= Σ[n ∈ ℕ]f(n)|X|ⁿ (properties of α and Vec)
Насколько это «произвольно»? Этот метод ограничен не только целыми коэффициентами, но и натуральными числами. Кроме того, f
может быть чем угодно, учитывая, что Turing Complete с зависимыми типами, мы можем представить любую аналитическую функцию с натуральными числовыми коэффициентами.
Я не исследовал взаимодействие этого, например, со случаем, приведенным в вопросе List X ≅ 1/(1 - X)
, или каков возможный смысл таких отрицательных и нецелочисленных «типов» в этом контексте.
Надеюсь, этот ответ каким-то образом исследует, как далеко мы можем зайти с функциями произвольного типа.