Злоупотребление алгеброй алгебраических типов данных - почему это работает?

"Алгебраическое" выражение для алгебраических типов данных выглядит очень наводящим на размышления тому, кто имеет опыт работы в математике. Позвольте мне попытаться объяснить, что я имею в виду.

Определив основные типы

  • Товар •
  • союз +
  • одиночка X
  • Единица измерения 1

и используя стенографию X² за X•X а также 2X за X+X и так далее, мы можем затем определить алгебраические выражения, например, для связанных списков

data List a = Nil | Cons a (List a) ↔ L = 1 + X • L

и бинарные деревья:

data Tree a = Nil | Branch a (Tree a) (Tree a) ↔ T = 1 + X • T²

Теперь мой первый инстинкт математика - сходить с ума от этих выражений и попытаться найти L а также T, Я мог бы сделать это путем многократной замены, но, кажется, гораздо проще ужасно злоупотреблять обозначениями и делать вид, что я могу изменить их по своему желанию. Например, для связанного списка:

L = 1 + X • L

(1 - X) • L = 1

L = 1 / (1 - X) = 1 + X + X² + X³ + ...

где я использовал расширение степенной серии 1 / (1 - X) совершенно неоправданным способом получить интересный результат, а именно, что L тип либо Nilлибо содержит 1 элемент, либо содержит 2 элемента, либо 3 и т. д.

Будет интереснее, если мы сделаем это для бинарных деревьев:

T = 1 + X • T²

X • T² - T + 1 = 0

T = (1 - √(1 - 4 • X)) / (2 • X)

T = 1 + X + 2 • X² + 5 • X³ + 14 • X⁴ + ...

снова, используя расширение серии Power (сделано с Wolfram Alpha). Это выражает неочевидный (для меня) факт, что существует только одно двоичное дерево с 1 элементом, 2 двоичных дерева с двумя элементами (второй элемент может находиться слева или справа), 5 двоичных деревьев с тремя элементами и т. Д.,

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

И, возможно, более интересно, возможно ли расширить эти идеи? Существует ли теория алгебры типов, которая допускает, например, произвольные функции типов, или для типов требуется представление степенного ряда? Если вы можете определить класс функций, то имеет ли какое-либо значение композиция функций?

Источник

7 ответов

Решение

Отказ от ответственности: многое из этого не совсем правильно работает, когда вы принимаете во внимание ⊥, поэтому я буду просто игнорировать это ради простоты.

Несколько начальных точек:

  • Обратите внимание, что "объединение", вероятно, не является лучшим термином для A+B здесь - это, в частности, непересекающееся объединение двух типов, потому что две стороны различаются, даже если их типы одинаковы. Для чего это стоит, более распространенный термин просто "тип суммы".

  • Синглтон-типы - это, по сути, все типы юнитов. Они ведут себя одинаково при алгебраических манипуляциях, и, что более важно, объем присутствующей информации все еще сохраняется.

  • Вы, вероятно, хотите нулевой тип, а также. Там нет стандартного, но самое распространенное имя Void, Нет значений, тип которых равен нулю, так же как есть одно значение, тип которого равен единице.

Здесь все еще не хватает одной важной операции, но я вернусь к этому через минуту.

Как вы, наверное, заметили, Haskell имеет тенденцию заимствовать понятия из теории категорий, и все вышеперечисленное имеет очень простую интерпретацию как таковую:

  • Для объектов A и B в Hask их произведение A×B является уникальным (с точностью до изоморфизма) типом, который допускает две проекции fst: A×B → A и snd: A×B → B, где заданы любой тип C и функции f.: C → A, g: C → B вы можете определить сопряжение f &&& g: C → A×B так, чтобы fst ∘ (f &&& g) = f и аналогично для g. Параметричность гарантирует универсальные свойства автоматически, и мой менее тонкий выбор имен должен дать вам идею. (&&&) оператор определяется в Control.Arrow, Кстати.

  • Двойственным из вышеперечисленного является побочный продукт A+B с инъекциями inl: A → A+B и inr: B → A+B, где для любого типа C и функций f: A → C, g: B → C вы можете определить сопряжение f ||| g: A+B → C такое, что имеют место очевидные эквивалентности. Опять же, параметричность гарантирует большинство сложных деталей автоматически. В этом случае стандартные инъекции просто Left а также Right и сопряжение является функцией either,

Многие из свойств типа продукта и суммы могут быть получены из вышеупомянутого. Обратите внимание, что любой одноэлементный тип является терминальным объектом Hask, а любой пустой тип является начальным объектом.

Возвращаясь к вышеупомянутой отсутствующей операции, в декартовой закрытой категории у вас есть экспоненциальные объекты, которые соответствуют стрелкам категории. Наши стрелки являются функциями, наши объекты являются типами с видом * и тип A -> B действительно ведет себя как B A в контексте алгебраического манипулирования типами. Если неясно, почему это должно выполняться, рассмотрите тип Bool -> A, Имея только два возможных входа, функция этого типа изоморфна двум значениям типа A т.е. (A, A), За Maybe Bool -> A у нас есть три возможных входа и так далее. Кроме того, обратите внимание, что если мы перефразируем приведенное выше определение сопряжения для использования алгебраической записи, мы получим тождество C A × C B = C A+B.

Что касается того, почему все это имеет смысл - и, в частности, почему использование расширения степенных рядов оправдано, - обратите внимание, что большая часть вышеперечисленного относится к "обитателям" типа (т. Е. К различным значениям, имеющим этот тип) в порядке продемонстрировать алгебраическое поведение. Чтобы сделать эту перспективу явной:

  • Тип продукта (A, B) представляет значение каждый из A а также B взяты самостоятельно. Так что для любого фиксированного значения a :: A есть одно значение типа (A, B) на каждого жителя B, Это, конечно, декартово произведение, а число жителей типа продукта является произведением числа жителей факторов.

  • Тип суммы Either A B представляет значение из любого A или же B с выделенными левой и правой ветвями. Как упоминалось ранее, это несвязанный союз, и число жителей типа суммы является суммой числа жителей слагаемых.

  • Экспоненциальный тип B -> A представляет отображение из значений типа B к значениям типа A, Для любого фиксированного аргумента b :: B, любое значение A может быть назначен на него; значение типа B -> A выбирает одно такое сопоставление для каждого ввода, что эквивалентно произведению как можно большего количества копий A как B имеет жителей, отсюда возведение в степень.

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

С другой стороны, приведенные выше конструкции тратят много времени на подсчет жителей, и перечисление возможных значений типа является здесь полезной концепцией. Это быстро приводит нас к перечислительной комбинаторике, и если вы обратитесь к связанной статье в Википедии, вы обнаружите, что первое, что она делает, - это определение "пар" и "объединений" в том же смысле, что и для типов товаров и сумм посредством генерируя функции, затем делает то же самое для "последовательностей", которые идентичны спискам в Haskell, используя точно ту же технику, что и вы.

Изменить: О, и вот быстрый бонус, который, я думаю, демонстрирует суть поразительно. Вы упомянули в комментарии, что для типа дерева T = 1 + T^2 Вы можете получить личность T^6 = 1, что явно не так. Тем не мение, T^7 = T действительно, и биекция между деревьями и семью корнями деревьев может быть построена непосредственно, ср. Андреас Бласс "Семь деревьев в одном".

Правка ×2: В отношении конструкции "производного типа", упомянутой в других ответах, вам также может понравиться эта статья того же автора, которая в дальнейшем опирается на эту идею, включая понятия деления и другие интересные вещи.

Источник

Бинарные деревья определяются по уравнению T=1+XT^2 в полукольце типов. По конструкции, T=(1-sqrt(1-4X))/(2X) определяется тем же уравнением в полукольце комплексных чисел. Итак, учитывая, что мы решаем одно и то же уравнение в одном и том же классе алгебраической структуры, на самом деле не должно удивлять, что мы видим некоторое сходство.

Суть в том, что когда мы размышляем о полиномах в полукольце комплексных чисел, мы обычно используем тот факт, что комплексные числа образуют кольцо или даже поле, поэтому мы используем такие операции, как вычитание, которые не применяются к полуколецам. Но мы часто можем исключить вычитания из наших аргументов, если у нас есть правило, которое позволяет нам отменять обе части уравнения. Такого рода вещи доказали Фиоре и Ленстер, показывающие, что многие аргументы о кольцах можно перенести на полукольца.

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

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

То, что я нахожу совершенно невероятным, - то, что вы обнаружили, может быть расширено до исчисления. Теоремы об исчислении можно перенести на полукольцо типов. Фактически, даже аргументы о конечных разностях могут быть перенесены, и вы обнаружите, что классические теоремы из численного анализа имеют интерпретации в теории типов.

Повеселись!

Источник

Серия исчисления и маклаурина с типами

Вот еще одно небольшое дополнение - комбинаторное понимание того, почему коэффициенты в разложении рядов должны "работать", в частности, сосредоточение внимания на рядах, которые могут быть получены с использованием подхода Тейлора-Маклорина из исчисления. NB: пример расширения серии, который вы приводите для типа манипулируемого списка, - это серия Макларина.

Поскольку другие ответы и комментарии касаются поведения выражений алгебраических типов (сумм, произведений и показателей степени), этот ответ исключит эти детали и сосредоточится на типе "исчисление".

В этом ответе вы можете заметить кавычки, делающие тяжелую работу. Есть две причины:

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

Определение серии Маклаурин

Ряд Маклаурина функции f : ℝ → ℝ определяется как

f(0) + f'(0)X + (1/2)f''(0)X² + ... + (1/n!)f⁽ⁿ⁾(0)Xⁿ + ...

где f⁽ⁿ⁾ означает n производная от f,

Чтобы иметь возможность понять серию Maclaurin как интерпретируемую с типами, нам нужно понять, как мы можем интерпретировать три вещи в контексте типов:

  • производная (возможно, множественная)
  • применяя функцию к 0
  • условия как (1/n!)

и оказывается, что эти концепции из анализа имеют подходящих аналогов в мире типов.

Что я подразумеваю под "подходящим партнером"? Он должен иметь вид изоморфизма - если мы сможем сохранить истину в обоих направлениях, факты, выводимые в одном контексте, могут быть перенесены в другой.

Исчисление с типами

Так что же означает производная выражения типа? Оказывается, что для большого и корректного ("дифференцируемого") класса выражений типов и функторов существует естественная операция, которая ведет себя достаточно схожим образом, чтобы быть подходящей интерпретацией!

Чтобы испортить изюминку, операция, аналогичная дифференциации, заключается в создании "контекстов с одним отверстием". Это отличное место для дальнейшего рассмотрения этого конкретного вопроса, но основная концепция контекста с одной дырой (da/dx является то, что он представляет собой результат извлечения одного подпункта определенного типа (x) из термина (типа a), сохраняя всю другую информацию, в том числе необходимую для определения исходного местоположения подпункта. Например, один из способов представления контекста с одним отверстием для списка - два списка: один для элементов, которые были до извлеченного, и один для элементов, следующих за.

Мотивация для идентификации этой операции с дифференцированием исходит из следующих наблюдений. Мы пишем da/dx означать тип контекста с одним отверстием для типа a с отверстием типа x,

d1/dx = 0
dx/dx = 1
d(a + b)/dx = da/dx + db/dx
d(a × b)/dx = a × db/dx + b × da/dx
d(g(f(x))/dx = d(g(y))/dy[f(x)/a] × df(x)/dx

Вот, 1 а также 0 представляют типы с ровно одним и ровно нулевым населением, соответственно, и + а также × представлять сумму и типы продуктов, как обычно. f а также g используются для представления функций типа или формирователей выражений типа, и [f(x)/a] означает операцию замены f(x) для каждого a в предыдущем выражении.

Это может быть написано в бессмысленном стиле, написание f' означать производную функцию типа функции f, таким образом:

(x ↦ 1)' = x ↦ 0
(x ↦ x)' = x ↦ 1
(f + g)' = f' + g'
(f × g)' = f × g' + g × f'
(g ∘ f)' = (g' ∘ f) × f'

который может быть предпочтительным.

Обратите внимание, что равенства можно сделать строгими и точными, если мы определим производные с использованием классов изоморфизма типов и функторов.

Теперь отметим, в частности, что правила в исчислении, относящиеся к алгебраическим операциям сложения, умножения и композиции (часто называемые правилами сумм, произведений и цепочек), отражаются именно операцией "сделать дыру". Кроме того, базовые случаи "сделать дыру" в постоянном выражении или термин x само по себе также ведет себя как дифференцирование, поэтому по индукции мы получаем дифференцирующее поведение для всех выражений алгебраического типа.

Теперь мы можем интерпретировать дифференциацию, что делает n "производная" от выражения типа, dⁿe/dxⁿ имею в виду? Это тип, представляющий n контексты места: термины, которые, когда "заполнены" n условия типа x дать e, Есть еще одно ключевое наблюдение, связанное с (1/n!) позже

Инвариантная часть функтора типа: применение функции к 0

У нас уже есть интерпретация для 0 в мире типов: пустой тип без членов. Что значит с комбинаторной точки зрения применить к нему функцию типа? В более конкретном плане, предполагая, f это функция типа, что делает f(0) выглядит как? Ну, у нас, конечно, нет доступа к чему-либо типа 0 так что любые конструкции f(x) которые требуют x недоступны Остаются те термины, которые доступны при их отсутствии, которые мы можем назвать "инвариантной" или "константной" частью типа.

Для явного примера возьмите Maybe функтор, который может быть представлен алгебраически как x ↦ 1 + x, Когда мы применяем это к 0, мы получаем 1 + 0 - это так же, как 1: единственное возможное значение None значение. Для списка, аналогично, мы получаем только термин, соответствующий пустому списку.

Когда мы возвращаем его и интерпретируем тип f(0) как число, которое можно рассматривать как число типов термина f(x) (для любого x) можно получить без доступа к x то есть количество "пустых" терминов.

Собираем все вместе: полная интерпретация серии Маклаурин

Боюсь, я не могу придумать подходящего прямого толкования (1/n!) как тип.

Если мы рассмотрим, однако, тип f⁽ⁿ⁾(0) в свете вышесказанного мы видим, что это можно интерпретировать как тип n контексты для термина типа f(x) которые еще не содержат x то есть, когда мы "интегрируем" их n раз, результирующий термин имеет точно nx с, не больше, не меньше. Тогда интерпретация типа f⁽ⁿ⁾(0) как число (как в коэффициентах ряда Маклаурина f) это просто подсчет сколько таких пустых n Местные контексты существуют. Мы почти у цели!

Но где же (1/n!) завершить? Изучение процесса типа "дифференцирование" показывает нам, что при многократном применении он сохраняет "порядок", в котором извлекаются подтермы. Например, рассмотрим термин (x₀, x₁) типа x × x и операция "сделать дыру" в нем дважды. Мы получаем обе последовательности

(x₀, x₁)  ↝  (_₀, x₁)  ↝  (_₀, _₁)
(x₀, x₁)  ↝  (x₀, _₀)  ↝  (_₁, _₀)
(where _ represents a 'hole')

хотя оба происходят от одного и того же термина, потому что есть 2! = 2 способы взять два элемента из двух, сохраняя порядок. В общем, есть n! способы взять n элементы из n, Таким образом, для того, чтобы получить количество конфигураций типа функтора, которые имеют n элементы, мы должны посчитать тип f⁽ⁿ⁾(0) и разделить на n! точно так же, как в коэффициентах ряда Маклаурина.

Таким образом, деление на n! оказывается интерпретируемым просто как сам по себе.

Заключительные мысли: "рекурсивные" определения и аналитичность

Сначала несколько замечаний:

  • если функция f: ℝ → ℝ имеет производную, эта производная единственна
  • аналогично, если функция f: ℝ → ℝ является аналитической, она имеет ровно один соответствующий ряд полиномов

Поскольку у нас есть правило цепочки, мы можем использовать неявное дифференцирование, если формализуем производные типа как классы изоморфизма. Но неявное дифференцирование не требует каких-либо инопланетных маневров, таких как вычитание или деление! Таким образом, мы можем использовать его для анализа определений рекурсивных типов. Чтобы взять ваш пример списка, у нас есть

L(X) ≅ 1 + X × L(X)
L'(X) = X × L'(X) + L(X)

и тогда мы можем оценить

L'(0) = L(0) = 1

получить коэффициент X¹ в серии Маклаурин.

Но поскольку мы уверены, что эти выражения действительно строго "дифференцируемы", хотя бы неявно, и поскольку мы имеем соответствие с функциями ℝ → ℝ, где производные, безусловно, уникальны, мы можем быть уверены, что даже если мы получим значения, используя незаконные операции, результат действителен.

Теперь, аналогично, чтобы использовать второе наблюдение, из-за соответствия (это гомоморфизм?) Функциям ℝ → ℝ, мы знаем, что, если мы удовлетворены тем, что функция имеет ряд Маклаурина, если мы можем найти любой ряд в все, принципы, изложенные выше, могут быть применены, чтобы сделать его строгим.

Что касается вашего вопроса о композиции функций, я полагаю, что правило цепочки дает частичный ответ.

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

Теперь, конечно, это только один способ выяснить, что здесь происходит, и, возможно, есть много других способов.

Резюме: TL;DR

  • тип "дифференциация" соответствует " делать дыру ".
  • применяя функтор к 0 дает нам "пустые" термины для этого функтора.
  • Поэтому степенные ряды Макларина (отчасти) строго соответствуют перечислению числа членов типа функтора с определенным числом элементов.
  • неявная дифференциация делает это более водонепроницаемым.
  • уникальность производных и уникальность степенных рядов означает, что мы можем выдумать детали, и это работает.
Источник

Кажется, что все, что вы делаете, - это расширение отношения повторения.

L = 1 + X • L
L = 1 + X • (1 + X • (1 + X • (1 + X • ...)))
  = 1 + X + X^2 + X^3 + X^4 ...

T = 1 + X • T^2
L = 1 + X • (1 + X • (1 + X • (1 + X • ...^2)^2)^2)^2
  = 1 + X + 2 • X^2 + 5 • X^3 + 14 • X^4 + ...

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

Источник

У меня нет полного ответа, но эти манипуляции имеют тенденцию "просто работать". Соответствующей статьей может быть " Объекты категорий как комплексные числа" Фьоре и Ленстера - я сталкивался с этим во время чтения блога sigfpe по соответствующей теме; остальная часть этого блога - золотая жила для подобных идей и стоит проверить!

Кстати, вы также можете различать типы данных - это даст вам подходящую молнию для этого типа данных!

Источник

Алгебра коммуникативных процессов (ACP) имеет дело с подобными выражениями для процессов. Он предлагает сложение и умножение в качестве операторов выбора и последовательности со связанными нейтральными элементами. На основании этого есть операторы для других конструкций, таких как параллелизм и нарушение. См. http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes. В Интернете также есть статья под названием "Краткая история алгебры процессов".

Я работаю над расширением языков программирования с помощью ACP. В апреле прошлого года я представил исследовательский документ на Scala Days 2012, доступный по адресу http://code.google.com/p/subscript/

На конференции я продемонстрировал отладчик, выполняющий параллельную рекурсивную спецификацию пакета:

Сумка = A; (Сумка & а)

где А и стенд для ввода и вывода действий; точка с запятой и знак амперсанда означают последовательность и параллелизм. Смотрите видео на SkillsMatter, доступное по предыдущей ссылке.

Спецификация сумки более сопоставима с

L = 1 + X•L

было бы

B = 1 + X & B

ACP определяет параллелизм с точки зрения выбора и последовательности с использованием аксиом; см. статью в Википедии. Интересно, что за аналогия с сумкой?

L = 1 / (1-X)

Программирование в стиле ACP удобно для анализаторов текста и контроллеров графического интерфейса. Технические характеристики, такие как

searchCommand = нажал (searchButton) + ключ (Enter)

cancelCommand = clicked (cancelButton) + ключ (Escape)

можно записать более кратко, сделав два уточнения "нажатыми" и "ключами" неявными (например, что Scala позволяет с функциями). Следовательно, мы можем написать:

searchCommand = searchButton + Enter

cancelCommand = cancelButton + Escape

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

Процессы получают таким образом данные в качестве компаньонов; таким образом я ввожу термин "алгебра предметов".

Источник

Теория зависимых типов и "произвольные" функции типов

Мой первый ответ на этот вопрос был высоким по понятиям и низким по деталям и отражал подвопрос "что происходит?"; этот ответ будет таким же, но сфокусирован на вопросе: "можем ли мы получить функции произвольного типа?".

Одним из расширений алгебраических операций суммы и произведения являются так называемые "большие операторы", которые представляют сумму и произведение последовательности (или, в более общем смысле, сумму и произведение функции над областью), обычно записываемой Σ а также Π соответственно. Смотрите сигма нотации.

Итак, сумма

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),

Запись: я буду использовать

∀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ⁿ в Хаскеле, где 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 к вышеуказанному типу естественно изоморфен функтору List.)

Последний фрагмент головоломки для "произвольных" функций - это как

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

как требуется.

  1. Многие теории требуют, чтобы члены * являются простыми представителями типов, и операция предоставляется как явное отображение из терминов типа*к их связанным типам. Другие теории допускают, чтобы сами буквальные типы были сущностями уровня термина.

"Произвольные" функции?

Теперь у нас есть аппарат для выражения общего общего степенного ряда в виде типа!

Сериал

Σ[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 может быть чем угодно, учитывая язык Тьюринга, полный с зависимыми типами, мы можем представить любую аналитическую функцию с натуральными числовыми коэффициентами.

Я не исследовал взаимодействие этого, например, с делом, представленным в вопросе о List X ≅ 1/(1 - X) или какой возможный смысл могут иметь такие отрицательные и нецелые "типы" в этом контексте.

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

Источник
Другие вопросы по тегам