Почему нам нужны типы сумм?

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

data Color = White | Black | Blue

мы имели бы

data White = White
data Black = Black
data Blue = Black
type Color = White :|: Black :|: Blue

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

show :: Color -> String
show White = "white"
show Black = "black"
show Blue = "blue"

Как вы можете видеть, в отличие от копродуктов это приводит к плоской структуре, поэтому вам не нужно иметь дело с инъекциями. И, в отличие от типов сумм, он позволяет случайным образом комбинировать типы, что приводит к большей гибкости и детализации:

type ColorsStartingWithB = Black :|: Blue

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

data Nil = Nil
data Cons a = Cons a (List a)
type List a = Cons a :|: Nil

Я знаю, что типы union присутствуют в TypeScript и, возможно, на других языках, но почему комитет Haskell выбрал ADT над ними?

Ответ 1

Тип суммы Haskell очень похож на ваш :|:.

Разница между двумя заключается в том, что тип сумм Haskell | является помеченным объединением, тогда как ваш тип суммы :|: не помечен.

Tagged означает, что каждый экземпляр уникален - вы можете отключить Int | Int от Int (на самом деле это выполняется для любого a):

data EitherIntInt = Left Int | Right Int

В этом случае: Either Int Int содержит больше информации, чем Int, потому что может быть Left и Right Int.

В вашем :|: вы не можете отличить эти два:

type EitherIntInt = Int :|: Int

Откуда вы знаете, было ли это левым или правым Int?

См. комментарии для расширенного обсуждения раздела ниже.

Тегированные союзы имеют еще одно преимущество: компилятор может проверить, выполнял ли вы, как программист, все случаи, зависящие от реализации для общих немаркированных союзов. Вы обрабатывали все случаи в Int :|: Int? Либо это изоморфно Int по определению, либо компилятор должен решить, какой Int (слева или справа) выбрать, что невозможно, если они неразличимы.

Рассмотрим еще один пример:

type (Integral a, Num b) => IntegralOrNum a b = a :|: b    -- untagged
data (Integral a, Num b) => IntegralOrNum a b = Either a b -- tagged

Что такое 5 :: IntegralOrNum Int Double в немаркированном союзе? Это как экземпляр Integral, так и Num, поэтому мы не можем решить наверняка и должны полагаться на детали реализации. С другой стороны, тегированный союз точно знает, что должен быть 5, потому что он заклеймен либо с помощью Left, либо Right.

Что касается именования: несвязанный союз в Haskell является типом объединения. ADT - это всего лишь средство их реализации.

Ответ 2

Я попытаюсь расширить категориальный аргумент, упомянутый @BenjaminHodgson.

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

Мы можем определить произведение в Hask как кортеж - категорически он соответствует определению произведения:

Произведением a и b является тип c, снабженный проекциями p и q такими, что p :: c -> a и q :: c -> b и для любого другого кандидата c', оснащенного p' и q' существует такой морфизм m :: c' -> c, что мы можем написать p' как p . m и q' как q . m.

Подробнее об этом читайте в Теория категорий Bartosz для программистов.

Теперь для каждой категории существует противоположная категория, которая имеет тот же морфизм, но меняет все стрелки. Таким образом, копроизведение:

Копродукт c of a и b - тип c, снабженный инъекциями i :: a -> c и j :: b -> c такими, что для всех остальных кандидатов c' с i' и j' существует такой морфизм m :: c -> c', что i' = m . i и j' = m . j.

Посмотрите, как выполняются тегированные и немаркированные соединения с учетом этого определения:

Немаркированный союз a и b - это тип a :|: b такой, что:

i :: a -> a :|: b определяется как i a = a и
j :: b -> a :|: b определяется как j b = b

Однако мы знаем, что a :|: a изоморфно a. Исходя из этого наблюдения, мы можем определить второго кандидата для продукта a :|: a :|: b, который оснащен точно такими же морфизмами. Поэтому нет единственного лучшего кандидата, так как морфизм m между a :|: a :|: b и a :|: b равен id. id является биекцией, из которой следует, что m является обратимым и "конвертирующим" типам в любом случае. Визуальное представление этого аргумента. Замените p на i и q на j.

Ограничьте себя Either, как вы можете убедиться:

i= Left и
j= Right

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

Объединение множества является частью дизъюнктного объединения, потому что мы можем определить его следующим образом:

data Left a = Left a
data Right b = Right b
type DisjUnion a b = Left a :|: Right b

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

Ответ 3

Это идея, о которой я много думал о себе: о языке с "первоклассной алгеброй типов". Совершенно очевидно, что мы могли бы сделать все так, как в Haskell. Конечно, если бы эти дизъюнкции были, как и альтернативы Хаскелла, мечеными союзами; то вы можете напрямую переписать любой ADT, чтобы использовать их. На самом деле GHC может сделать это за вас: если вы выведете экземпляр Generic, тип варианта будет представлен :+:, которая по существу просто Either.

Я не очень уверен, что и бездомные профсоюзы. До тех пор, пока вам потребуются различимые типы, участвующие в сумме, явное пометка в принципе не требуется. Тогда языку потребуется удобный способ сопоставления типов во время выполнения. Звучит очень похоже на то, что делают динамические языки - очевидно, что есть некоторые накладные расходы.
Самая большая проблема заключалась бы в том, что если типы с обеих сторон :|: должны быть неравными, вы теряете параметричность, которая является одной из лучших черт Haskell.

Ответ 4

Учитывая, что вы упоминаете TypeScript, поучительно взглянуть на то, что его документы должны говорить о своих типах объединения. Пример начинается с функции...

function padLeft(value: string, padding: any) { //etc.

... имеет недостаток:

Проблема с padLeft заключается в том, что ее параметр заполнения вводится как any. Это означает, что мы можем назвать это аргументом, который не является ни number, ни string

Затем предлагается одно правдоподобное решение и отклонено:

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

Скорее, руководство предлагает...

Вместо any мы можем использовать тип объединения для параметра padding:
function padLeft(value: string, padding: string | number) { // etc.

В сущности, понятие типа объединения описывается следующим образом:

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

Значение A string | number в TypeScript может быть либо типа string, либо типа number, поскольку string и number являются подтипами string | number (см. комментарий Алексиса Кинга к вопросу). Однако значение Either String Int в Haskell не является ни типом string, ни типом Int - его единственным, мономорфным, является тип Either String Int. Дальнейшие последствия этой разницы проявляются в оставшейся части обсуждения:

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

В примерно аналогичном сценарии Haskell, если у нас есть, скажем, Either Double Int, мы не можем применять непосредственно к нему (2*), хотя оба Double и Int имеют экземпляры Num. Скорее, необходимо что-то вроде bimap.

Что происходит, когда нам нужно знать, есть ли у нас Fish? [...] Нужно использовать утверждение типа:
let pet = getSmallPet();

if ((<Fish>pet).swim) {
    (<Fish>pet).swim();
}
else {
    (<Bird>pet).fly();
}

Такая сортировка типа "downcasting/runtime" не согласуется с тем, как обычно работает система типа Haskell, хотя она может быть реализовано с использованием той же системы типов (также с учетом ответа leftaroundabout). Напротив, во время выполнения нет ничего, чтобы выяснить тип Either Fish Bird: анализ случаев происходит на уровне значений, и нет необходимости разбираться с чем-то неудачным и производить Nothing (или, что еще хуже, null) из-за несоответствий типа времени выполнения.