Почему типы суммы называются типами суммы?

В процессе изучения Haskell я читал об алгебраических типах данных, типах сумм и типах произведений. Хотя типы произведения аналогичны декартову произведению, и слово «произведение» сразу же приобрело для меня смысл, я не понимаю, почему типы суммы (вариантные типы, также известные как объединение с тегами, также известные как размеченное объединение, или непересекающееся объединение) называются sum типы.

Википедия говорит:

Тип суммы соответствует интуиционистской логической дизъюнкции при соответствии Карри–Ховарда.

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

 OR |   | +
-----------
0 0 | 0 | 0 
0 1 | 1 | 1
1 0 | 1 | 1
1 1 | 1 | 0 (mismatch here)

Но не очень подходит из-за 1+1.

Я нашел различные объяснения того, что такое типы произведения и суммы, и я думаю, что понял. Тип суммы — это либо одно, ИЛИ другое.

Но почему именно он называется типом суммы? Просто потому, что принято использовать символ + для оператора ИЛИ? Или потому, что «типы сумм двойственны типам продуктов»?

(Опять же, если я не пропустил что-то важное, пожалуйста, не объясняйте тип суммы/произведения. Я думаю, что понял концепцию. Я только хочу знать, почему он называется типом sum.)


person problemofficer    schedule 14.11.2017    source источник
comment
Суммирование типов также можно назвать слиянием типов (первоначальная идея К.ХАРИСАИ).   -  person bsound    schedule 18.02.2021


Ответы (1)


Он называется типом суммы, потому что количество значений A + B является суммой количества значений A и B.

person SLaks    schedule 14.11.2017
comment
Оооо, это имеет смысл. - person problemofficer; 14.11.2017
comment
В более общем смысле дизъюнкция множеств является суммированием множеств. Точно так же набор значений компонентов типов продуктов (т.е. структур) является набором продуктов значений их типов компонентов. - person FeepingCreature; 17.05.2018