Последние месяцы я вкладывал почти всё мое писательское время в «Логику для программистов», и мой мозг уже почти превратился в книгу. Поверьте мне, вы не хотите читать две тысячи слов ворчания на LaTeX. Однако я провел последнюю неделю в кроличьей норе истории, и я просто обязан поделиться тем, что я нашёл.

Всё началось со статьи «Алгебраические типы данных на самом деле не такие страшные (eng. Algebraic Types are not Scary, Actually)». Она разбирает АлгТД¹ в деталях, но вот краткий обзор:

• Типы-произведения — штуки вроде (Int, Bool) или Dog(name: Str, owner: Person, age: Int). У них есть значение для каждого поля. Почти все современные языки программирования имеют типы-произведения, обычно называя их чем-то вроде «структуры» (structs) или «записи» (records) или «объекты-значения» (value objects) и так далее.

• Типы-суммы — объединения с метками (tagged unions) — штуки вроде Int + Nothing, Result + ErrorType или Address + Number + Email. По сути, это выбор из нескольких опций (прим. пер.: во многих языках можно увидеть | вместо +). «Метка» (tag) означает, что мы не исключаем одинаковые значения, например: Bool + Bool имеет 4 разных значения (левое True, правое True, левое False, правое False). Типы-суммы довольно редко встречаются в современных языках вне функционального программирования и мест вроде Rust.

Может возникнуть такой вопрос: откуда они вообще получили такие имена? Обычно объясняется, что эти имена происходят от их мощности (количества возможных значений). Допустим, если — мощность типа , то и . Проделайте мысленный эксперимент с типами Bool + Weekday и (Bool, Weekday), если вы не уверены (Weekday принимает значение одного из семи дней недели).

Но может же быть наоборот, что имена происходят от факта, что суммы и произведения типов ведут себя так же, как и суммы и произведения чисел! Я думаю, что это довольно известный факт, но он не слишком часто встречается в введениях в АлгТД. Например, сложение чисел ассоциативно, а значит . Применительно к типам, это может сказать нам, что Int + (String + Null) изоморфно () с (Int + String) + Null: мы можем свободно преобразовывать значения между этими двумя типами без потери какой-либо важной информации.

Более интересным примером является то, что АлгТД следуют и распределительному закону умножения . Если у нас есть значение типа Account(name: Str, contact: (Email + Phone)), мы можем преобразовать его в тип Account(name: Str, contact: Email) + Account(name: Str, contact: Phone).

Это меня и заинтересовало: какое свойство АлгТД дало имя типам «суммам» и «произведениям», а какие свойства были открыты впоследствии? По мере того, как я исследовал эту тему, я всё больше погружался в раннюю историю алгебраических типов данных.

Ищем источник

Обычно поиск источника термина — это кошмар, но так как это «абстрактный академический нонсенс», то всё релевантное наверняка есть в каком-то исследовании или научной работе. Я люблю пользоваться этими двумя техниками поиска:

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

2. Сходить в ACM Digital Library, найти термин и прочитать все работы, начиная с самой старой.² Обычно комбинирование этих техник дает наилучший результат. Так я, в конце концов, пришёл к статье Джона Маккарти (создателя LISP) «Базис математической теории вычислений» (eng. A Basis for a Mathematical Theory of Computation), изданной в 1961. Насколько я могу судить, это самое первое упоминание АлгТД в какой-либо форме.

Статья Маккарти

Начнем с того, что в статье не используется ни слово «тип» (в понимании computer science), ни «алгебра» вообще. Однако она затрагивает «способ задания пространств данных в терминах данных базовых пространств», и одно из этих пространств — « из значений истинности, элементы которого могут быть только (truth, истина) или (false, ложь)». Вы, наверно, уже узнали за этой формулировкой знакомый всем boolean. Тем не менее, Маккарти был точно знаком с типами, будучи в составе комитета АЛГОЛ-60, поэтому я думаю, что он специально избегает слова «тип» здесь.

Вся статья описывает простую математическую модель программных функций и их свойств. В разделе 2.6 он определяет два способа создания новых пространств из уже существующих:

Декартово произведение двух множеств и — множество всех упорядоченных пар таких, что и . Если и — конечные множества и и — соответственно количества их элементов, то .

Неудивительно, что тип-произведение назван так из-за декартова произведения. Например, запись (record) Dog(name: Str, owner: Person, age: Int) — размеченная (tagged) версия декартова произведения . Здесь же мы видим и сходство с нашими формулами .

Прямое объединение (direct union) двух множеств и — объединение двух непересекающихся множеств, один из которых 1 в 1 соотносится с , а другой — с . Если и — конечные множества и и — соответственно количества их элементов, то , даже если их элементы пересекаются. Элементы могут быт записаны, как элементы и , подписанные тем множеством, откуда они были взяты. Например, или .

Насколько я могу судить, термин «прямое объединение» был введен Маккарти, но он точь-в-точь соотносится с дизъюнктивным объединением. Маккарти позже обращается к этим двум терминам как к «прямой сумме (direct sum) и декартову произведению». Он не называет их «типы-суммы и типы-произведения», но я думаю, можно поверить в то, что они были названы из-за их соответствия этим операциям. Я не буду закапываться в историю этих названий, но я предположу, что они были названы по аналогии с арифметическими суммой и произведением.

Вскоре после определения прямой суммы и декартова произведения³ Маккарти определяет изоморфизмы между пространствами данных:

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

Он продолжает тем, что показывает некоторое количество изоморфизмов, включая распределяющее , которое я нашел довольно красивым. Все эти свойства «алгебраических типов данных» были известны с самого начала, несмотря на то что их так еще не называли.

Это пошло отсюда?

Пока я проводил свое исследование, я нашел интересную заметку «Некоторые наблюдения насчет больших затрат на программирование» (eng. Some Observations Concerning Large Programming Efforts) (1964). Автор представил, по сути, Agile manifesto за 50 лет до Agile manifesto! Никто эту заметку, правда, не цитировал и автор больше ничего не публиковал. Этим я хочу сказать, что не важно, был ли ты первым, у кого появилась определённая идея, если её никто не слышал.

Итак, давайте вернёмся к отслеживанию пути алгебраических типов. В 1964 Маккарти публикует «Определение новых типов данных в ALGOL x» (eng. Definition of new data types in ALGOL x)⁴. Там он предлагает добавление двух новых типов — «декартовый» и «объединение» — в следующую версию ALGOL. Стоит заметить, что здесь впервые мы видим размеченные (tagged) АлгТД, где и сумма, и произведение имеют строковые метки (теги). ALGOL-68 затем реализует оба, но придет в тупик и не окажет заметного воздействия на современные языки программирования.

Исследование Хоара

Хоар, скорее всего, независимо от Маккарти пришел к идее типов-сумм и типов-произведений. Во «Вкладе в разработку ALGOL» (eng. A contribution to the development of ALGOL) (1966) он предлагает записи (records) помеченные как «классы» и ключевое слово union для объединения классов в один супертип. Тем не менее, он не дает никаких алгебраических свойств записям и объединениям. К моменту «Заметок о структуризации данных» (eng. Notes on Data Structuring) его терминология сдвигается и начинает совпадать с терминологией Маккарти:

Типы, в которых мы заинтересованы, уже известны математикам; например, декартовы произведения, дискриминантные объединения, множества, функции, последовательности и рекурсивные структуры.

Что «декартовы произведения», что «дискриминантные объединения» у него размечены (tagged), что соответствует тому, как мы используем алгебраические типы сегодня. Так как он больше обеспокоен хранением данных, он не описывает алгебраических свойств, но упоминает мощности в обсуждении о том, как хранить такие типы наиболее эффективно.

Если программист попытается конвертировать дискриминантное объединение обратно к типу, из которого оно не происходило, это будет серьёзной ошибкой, которая может привести к бессмысленным результатам. Эта ошибка может быть найдена только с помощью проверок во время выполнения, которая проверяет тег поля каждый раз, когда такая конверсия происходит. Такая проверка занимает время, а в случае ошибки, она еще и неудобна. Поэтому мы ищем техники нотации, которые смогут нам гарантировать, что эта ошибка никогда не произойдет во время выполнения; и гарантия должна даваться только по тексту программы, не зная о том, какие конкретно значения обрабатываются. Такая гарантия может быть дана автоматическим компилятором, при наличии такового.

Это еще и первый раз, когда мы можем увидеть, что тип-сумма называется «дискриминантным объединением».⁵ Барбара Лисков использует этот термин, чтобы определить тип-сумму oneof в CLU, а Никлаус Вирт использует его в объяснении, почему в Pascal нету типов-сумм. По этой причине, я подозреваю, что мир императивного программирования узнал про типы-суммы изначально из лекции Хоара, а на Хоара повлияла статья Маккарти.⁶

После этого момента типы-суммы исчезают из императивного программирования. В императивных языках конца XX века доминировало влияние Pascal и C. В Pascal не было типов-сумм, потому что Вирт считал их менее гибкими, чем не размеченные (untagged) объединения. В C, возможно, нет типов-сумм, потому что его создатели заимствовали систему типов из языка PL/I от IBM. В PL/I, впервые выпущенном в 1964 году, были типы-произведения (которые там назывались structs), но объединения были только не размеченные (untagged). Современные императивные языки, в свою очередь, заимствовали типы-суммы из мира функционального программирования, что возвращает нас к статье «Доказательство свойств программ методом структурной индукции» (eng. Proving properties of programs by structural induction»).

Статья Бёрстолла

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

Статья посвящена доказательству свойств рекурсивных типов, например, списков и деревьев. Вот как он определяет список:

Я предлагаю, чтобы каждая конструкция операции вводила новый тип и чтобы дизъюнкции этих типов также были типами (примерно следуя Лэндину 1964) …
… cons имеет атом и список, nil не имеет компонентов, а list — это cons или nil.

Бёрстолл говорит, что заимствовал эту нотацию из работы П. Дж. Лэндина «Механическое вычисление выражений» (eng. The Mechanical Evaluation of Expressions) (1964). Использование Лэндина, похоже, не совсем соответствует типам-суммам — неясно, был ли у него механизм для различения типов, если их значения пересекались. Скорее, мне кажется, что Бёрстолл «следовал» представлениям Лэндина о записи рекурсивных определений. Впрочем, это трудно сказать наверняка, и я легко могу ошибаться.

Случай с ISWIM

Бёрстолл также цитирует работу Лэндина «Следующие 700 языков программирования» (eng. The Next 700 Programming Languages) (1966), в которой был предложен влиятельный язык ISWIM. Согласно статье «Некоторая история функциональных языков программирования» (eng. Some History of Functional Programming Languages) (2012), это был первый язык, в котором появились алгебраические типы данных:

В статье об ISWIM также впервые появляются определения алгебраических типов, используемые для описания структур. Это делается на словах, но идея «суммы произведений» там явно прослеживается.

Однако я не думаю, что это верно. Во-первых, ISWIM был лишь предложенным языком, а до реализации дело не дошло. Если мы считаем и предложения языков, то Маккарти опередил его на два года, а Хоар/Вирт — на пару месяцев. Но кроме того, я вообще не думаю, что в ISWIM были определены типы-суммы! Это более слабое убеждение, но у меня есть на то три причины:

1. Я перечитал статью шесть раз и не могу понять, где он использует «сумму произведений». Возможно, авторы «Некоторой истории функциональных языков программирования» ссылаются на определение amessage у Лэндина, но я думаю, что этот раздел посвящен структуре программы на ISWIM, а не структурам данных внутри нее.

2. Я прочитал спецификации двух реализаций ISWIM, PAL и POP-2, и ни в одной из них нет «сумм произведений».

3. В «Некоторой истории функциональных языков программирования» позже говорится, что статья Бёрстолла «расширила ISWIM определениями алгебраических типов, но всё ещё описанными на словах», что подразумевает, что в ISWIM их изначально не было.

Ни одна из этих причин не является сверхсильной, и я готов признать свою неправоту.

Однако у Бёрстолла типы-суммы всё же есть, что мы видим в его определении дерева. Дерево — это «узел (node), или верхушка (tip), или пустое дерево (niltree)», но верхушка «содержит элемент», а не является элементом. Позже он приводит следующий псевдокод:

cases t:
    niltree(): nil()
    tip(i): i::nil()
    node(t1, i1, i2): concat(flatten(t1), flatten(t2))

Бёрстолл также говорит, что его идеи «основаны на работе Джона Маккарти», ссылаясь на его статью о математической теории. Не исключено, что Бёрстолл был вдохновлен понятием прямого объединения Маккарти.

На 2025 год эта статья была процитирована более 500 раз. Позже Бёрстолл внесёт ещё больший вклад, но это случится в 1980 году, так что сначала нам нужно рассмотреть ML.

Статья Милнера

До сих пор мы видели определения алгебраических типов данных и частое использование «декартова произведения», но не сами термины «тип-сумма» и «тип-произведение». Насколько я могу судить, они пришли из языка ML Робина Милнера, как было описано в «Теории полиморфизма типов в программировании» (eng. A Theory of Type Polymorphism in Programming) (1977):

Полностью определённые типы (т.е. монотипы) в ML строятся из множества базовых типов (int, bool и т. д.) с помощью бинарных инфиксных операторов (декартово произведение), (дизъюнктная сумма) и (функциональный тип), а также унарного постфиксного оператора .

В этой статье стоит отметить несколько моментов. Во-первых, конечно, она описывает конструирование типов с помощью «дизъюнктивной суммы» и использует символ . Во-вторых, она не обосновывает и не даёт определения «дизъюнктивной суммы», в отличие от Хоара и Маккарти. К этому моменту это, возможно, уже было общеизвестным фактом для аудитории Милнера. Наконец, в статье утверждается, что суммы и произведения были реализованы в ML как минимум за два года до её публикации.

У нас нет полной спецификации самых старых версий ML, но есть исходный код выпущенного прувера LCF, для которого ML и был разработан. Вот фрагмент из files.ml:

let instintype insttylist ty = inst ty whererec inst ty =
     fst(revassoc ty insttylist)
     ?(failwith phylumoftype ty
    ??``consttype vartype`` ty
    ??``funtype`` mkfuntype((inst # inst)(destfuntype ty))
+   ??``sumtype`` mksumtype((inst # inst)(destsumtype ty))
+   ??``prodtype`` mkprodtype((inst # inst)(destprodtype ty))
      )  ;;

Ага, вот они: типы «сумма» и «произведение»! Однако они не размеченные (untagged). В статье Ли-яо Ся «Откуда пошло название «алгебраический тип данных»?» отмечается, что «ранние версии не предоставляли типов данных (см. первую версию Edinburgh LCF)», что я понимаю как отсутствие размеченных (tagged) алгебраических типов; в ML было ключевое слово abstype для именования сконструированных типов. Можно было определить EmailOrAddress как Str + Str, но нельзя было назвать левый Str »email».

В «Теории полиморфизма типов» не цитируются ни статья Маккарти, ни работы Хоара или Бёрстолла, поэтому неясно, повлияли ли они на Милнера, или он разработал АлгТД независимо. Некоторым косвенным доказательством является следующая работа «Метаязык для интерактивных доказательств в LCF» (eng. A Metalanguage for Interactive Proof in LCF) (1978), где он благодарит всех троих за их вклад:

Мы в долгу перед Даной Скоттом за предоставление значительной части теоретической основы нашей работы, перед Джоном Маккарти за поддержку предшественника этого проекта в Стэнфорде, перед Ричардом Вейраухом, который внёс большой вклад в этот проект, перед Тони Хоаром и Джерри Шварцем за помощь с понятием абстрактных типов в ML, перед Аврой Кон за помощь на заключительных этапах проектирования с помощью экспериментов, перед Родом Бёрстоллом и многими коллегами в Эдинбурге за обсуждения.

Хорошо, осталось всего три языка.

Hope, VAX ML и Miranda

Примерно в это же время Бёрстолл применял теорию категорий для спецификации программного обеспечения, что в конечном итоге привело его к разработке языка HOPE. »HOPE: An experimental applicative language» (1980) знаменует собой первое введение размеченных (tagged) объединений в функциональное программирование, но не размеченных произведений:

Чтобы определить тип «дерево чисел», мы могли бы написать:

data numtree == empty ++ tip(num) ++ node(numtree#numtree)

(знак # обозначает декартово произведение типов.)

Кроме того, в статье представлены две важные идеи. Первая — компилятор может выполнять исчерпывающую проверку того, что все взаимоисключающие варианты в типе-сумме обработаны:

Каждый тип данных будет иметь набор непересекающихся подтипов, каждый с собственной функцией-конструктором; например, списки создаются с помощью cons или nil. Должно быть просто делать анализ по случаям для этих конструкторов, и компилятору должно быть легко проверять, является ли этот анализ исчерпывающим. Это позволяет избежать таких ошибок, как, например, забытая проверка на пустой список.

Вдобавок к этому, статья предлагает, что использование типов-сумм может быть значительно упрощено благодаря pattern matching. Это не первое появление структурного pattern matching в языке (Prolog получил его первый), но это его первое появление в функциональном программировании.

Примерно в то же время, что и HOPE, ученик Бёрстолла, Лука Карделли⁷, работал над портированием ML на VAX и Unix, в процессе добавив типы записей (record) и вариантов (variant). Насколько я могу судить, это был первый случай, когда и размеченные суммы, и размеченные произведения присутствовали в функциональном языке программирования.

Все эти идеи позже будут включены в Standard ML, закрепив то, что сегодня считается ключевыми чертами алгебраических типов: теги, исчерпывающая проверка компилятором и pattern matching.

Наконец, снова ссылаясь на Ся, «Miranda: нестрогий функциональный язык с полиморфными типами» (eng. Miranda: A non-strict functional language with polymorphic types) (1985) — это первая статья, в которой действительно используется термин «алгебраический тип данных». Я настоятельно рекомендую прочитать пост Ся для получения дополнительной информации.

Довольно шаткое заключение

• Маккарти первым предлагает концепции и свойства алгебраических типов данных в своей статье, хотя и не называет их так.

• Это, по крайней мере, в какой-то степени влияет на Тони Хоара и Рода Бёрстолла, которые пишут собственные влиятельные работы.

• АлгТД реализуются в ALGOL-68, CLU и ML. Неясно, знал ли Милнер о теориях Маккарти, но я бы рискнул предположить, что скорее да, чем нет.

• Pascal и C мешают типам-суммам закрепиться в императивном программировании.

• Бёрстолл и Лука Карделли дополняют основные возможности АлгТД, делая их краеугольным камнем в типизированном ФП.

Итак, это лучшее, что у меня получилось сделать с моими ресурсами и временем. Спасибо за прочтение!

Оригинал статьи.

¹: Алгебраические типы данных ещё сокращают и как АТД, но так же сокращают и Абстрактные типы данных. В этой статье для ясности используется АлгТД.

²: Kagi делает это очень простым: у меня есть кастомный bang для поиска.

³: Для фанатов ранней теории языков программирования там есть много других весёлых вещей. Например, он представляет знаменитое "power series" определение типа последовательности, описывая сначала и затем "формально решая для S, получая , которые мы можем развернуть в геометрической последовательности, чтобы получить "

⁴: Тони Финч прислал её мне. Спасибо!

⁵: Это может быть также и первым появлением примера с колодой карт. Хоар описывает его как type pokercard = (normal: (s: suit; r: rank), wild: (joker 1, joker 2)). Да, , — сумма, а ; — произведение.

⁶: С другой стороны, Вирт был соавтором во "Вкладе в разработку АЛГОЛ", а значит он, скорее всего, имел представление о их значении, может быть просто не о формальной модели.

⁷: Научным руководителем Карделли был Гордон Плоткин, а его научным руководителем был Бёрстолл. Мир тесен!