Владимир Мельник 17 сентября 2019

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

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

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

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

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

Так, тип 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).

МЕРОПРИЯТИЯ

Комментарии

ВАКАНСИИ

Добавить вакансию
Backend Lead (Python, Django)
по итогам собеседования
AppSec Business Partner
по итогам собеседования
DevOps
от 350000 RUB

ЛУЧШИЕ СТАТЬИ ПО ТЕМЕ