Что есть алгебраические типы?

Алгебраические типы данных — это не особые типы данных, а способ построения новых как композиции из уже известных при помощи алгебраических операций.

Плавное погружение

Алгебраические типы данных — это не особые типы данных, а способ построения новых как композиции из уже известных при помощи алгебраических операций.

Тип данных можно описать рекурсивно: это множество значений, принадлежащих типу. Ключевое слово здесь — МНОЖЕСТВО.

Так, тип char — это целое положительное число или соответствующий ему символ последовательности ASCII. Например, 8 бит позволяют описать 256 возможных значений, иначе говоря, мощность (размер множества или в английской литературе cardinality) типа char = 256. Тип bool имеет мощность = 2, то есть переменная этого типа может принимать только два возможных значения: true либо false:

type bool = True | False

 Теперь возьмем, например, кортеж (кортеж — картезианское произведение множеств (Product types)) (tuple), состоящий из двух значений, одно из которых имеет тип char, а другое — bool. Сигнатура такого кортежа в OCaml выглядит так: (char * bool), что похоже на декартово произведение и в самом деле им является, поскольку мощность типа (char * bool) = (256 * 2) = 512.

Для другого примера возьмем опцию:

type `t option = Some `t | None

`t - это переменная типа, вместо которой может быть любой другой тип. Для такого варианта вариабельность будет |`t| + 1, поскольку None — это одно единственное значение. Если мы примем `t = char, то вариабельность типа char option будет: Some char + None = 256 + 1 = 257.

Итак, варианты — это сложение множеств (Sum types). Сама возможность так определять типы называется поддержкой алгебраических типов данных.

“Минус” и “поделить” в алгебре типов (немного тезисно)

Примеры кода приведены на OCaml-подобном псевдокоде.

Операция вычитания должна быть обратной операции сложения (ИЛИ, перечисление), что порождает таким sum-типы, как варианты:

type `a option = Some `a | None

Для `a = int (int 32) будет: 4_294_967_296 + 1 (None) = 4_294_967_297 возможных значений.

Следовательно, вычитание сводится к перечислению не того, что входит, но того, что исключается. То есть это некий sub-typing по принципу черного листа.

type some_int = int option - None - исключаем None (1)

Операция деления должна быть обратной операции умножения (И, декартово произведение, комбинация вариантов), что порождает product-типы, вроде кортежей или записей.

type 2dPoint = {x: float; y: float}

Поскольку умножение прибавляет множества:

let x = 0.0  или {x: float} (float)

{x: float; y: float} (float * float)

{x: float; y: float; z: float} (float * float * float)

То операция деления на типах должна их удалять:

{x: float; y: float; z: float} (float * float * float)

{x: float; y: float} (float * float)

{x: float} (float)

type 2dPoint = 3dPoint - 3dPoint#z

В случае с вычитанием мы имеем дело с антишаблоном “особый случай”, потому что вычитаемое — особый случай. По этой причине необходимость в такой операции будет свидетельствовать о плохой, "потекшей" абстракции.

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

Таким образом, вычитание и деление в алгебре типов скорее вредны, чем полезны, а потому мы их нигде не встречаем (по крайней мере, я не обнаруживал их реализации в тех языках, которые изучал/с которыми работал).

Зависимые (Dependent) типы

Зависимые типы — это примеры умножения на < 1, поскольку они представляют из себя композицию “И” из типов (предикаты относим к типам). При этом множество возможных значений сокращается. Если переменная типа int может принимать одно из 4_294_967_296 значений, то переменная типа even(int) будет иметь только 4_294_967_296 / 2 = 2_147_483_648 возможных значений.

P.S. Приглашаю Вас подписаться на мой Telegram канал о разработке и программировании IT-Rampage, где вы сможете найти еще больше подобных публикаций (правда, не так хорошо оформленных, как на Proglib).