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

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

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

• Товар •
• союз +
• одиночка 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 двоичных деревьев с тремя элементами и т. Д. ,

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

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

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

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

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

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

• Вы, вероятно, хотите нулевой тип, а также. Haskell предоставляет это как 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 :: 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)определяется тем же уравнением в полукольце комплексных чисел. Итак, учитывая, что мы решаем одно и то же уравнение в одном и том же классе алгебраической структуры, на самом деле не должно удивлять, что мы видим некоторое сходство.

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

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

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

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

Радоваться, веселиться!

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

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 = clicked (searchButton) + клавиша (Enter)

cancelCommand = clicked (cancelButton) + клавиша (Escape)

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

searchCommand = searchButton + Enter

cancelCommand = cancelButton + Escape

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

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

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

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

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

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

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

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

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

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

где f⁽ⁿ⁾означает nпроизводную от f.

Чтобы понять смысл ряда Маклаурина как интерпретируемого с типами, нам нужно понять, как мы можем интерпретировать три вещи в контексте типов:

• производная (возможно, множественная)
• применяя функцию к 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раз результирующий член имеет ровно n x s, не больше, не меньше. Тогда интерпретация типа 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дает нам «пустые» термины для этого функтора.
• Поэтому степенные ряды Маклорина (отчасти) строго соответствуют перечислению числа членов типа функтора с определенным числом элементов.
• неявная дифференциация делает это более водонепроницаемым.
• уникальность производных и уникальность степенных рядов означает, что мы можем выдумать детали, и это работает.

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

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

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

Итак, сумма

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ⁿв Haskell, где Xэто тип и nнатуральное число, это злоупотребление нотацией; это выражение типа, содержащее число: явно не является допустимым выражением.

С другой стороны, с зависимыми типами на картинке, типы, содержащие числа, это как раз и есть точка; на самом деле, зависимые кортежи или «векторы» являются очень часто цитируемым примером того, как зависимые типы могут обеспечить прагматическую безопасность на уровне типов для таких операций, как доступ к списку . Вектор - это просто список вместе с информацией на уровне типов относительно его длины: именно то, что нам нужно для подобных выражений типа Xⁿ.

Для продолжительности этого ответа, пусть

Vec X n

быть типом nвекторов Xдлины значений -type.

Технически 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ⁿ

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

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

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

Существует несколько способов представления типов на уровне терминов. Я буду использовать здесь воображаемую нотацию по Хаскеллу *для вселенной типов, которая обычно считается типом в зависимом окружении. ¹

Аналогичным образом, существует также как минимум столько же способов обозначения « ℕисключения», сколько существует теорий зависимых типов. Я буду использовать 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)том, какой возможный смысл могут иметь такие отрицательные и нецелые «типы» в этом контексте.

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