[Перевод] Простые алгебраические типы данных

Это шестая статья из цикла «Теория категорий для программистов». Предыдущие статьи уже публиковались на Хабре:
0. Теория категорий для программистов: предисловие
1. Категория: суть композиции
2. Типы и функции
3. Категории, большие и малые
4. Категории Клейсли
5. Произведения и копроизведения

В предыдущей статье были рассмотрены базовые операции над типами: произведение и копроизведение. Теперь покажем, что комбинирование этих механизмов позволяет построить многие из повседневных структур данных. Такое построение имеет существенное прикладное значение. Например, если мы умеем проверять на равенство базовые типы данных, а также знаем, как свести равенство произведения и копроизведения к равенстве компонент, то операторы равенства для составных типов можно вывести автоматически. В Haskell для обширного подмножества составных типов автоматически выводятся операторы равенства и сравнения, конвертация в строку и обратно и многие другие операции.

Рассмотрим подробнее место произведения и копроизведения типов в программировании.

Произведение типов

Каноническая реализация произведения типов в языках программирования — это пара. В Haskell пара является примитивным конструктором типов, а в C++ это относительно сложный шаблон из стандартной библиотеки.

Строго говоря, произведение типов не коммутативно: нельзя подставить пару типа (Int, Bool) вместо (Bool, Int), хотя они и содержат одни и те же данные. Однако произведение коммутативно с точностью до изоморфизма, задаваемого функцией swap, которая обратна самой себе:

swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)

Можно рассматривать такие пары как различные форматы хранения одной и той же информации, как big endian и little endian.
Вкладывая одни пары в другие, можно скомбинировать в произведение сколько угодно типов. То же самое можно получить проще, если заметить, что вложенные пары эквивалентны кортежам. Это следствие того, что различные порядки вложения пар изоморфны между собой. Есть два возможных порядка комбинирования в произведение трех типов a, b и c (в заданной последовательности). А именно,

((a, b), c)

или

(a, (b, c))

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

alpha :: ((a, b), c) -> (a, (b, c))
alpha ((x, y), z) = (x, (y, z))

А вот обратная к ней:

alpha_inv :: (a, (b, c)) -> ((a, b), c)
alpha_inv  (x, (y, z)) = ((x, y), z)

Итак, имеет место изоморфизм типов; это просто разные способы переупаковки одних и тех же данных.

Рассматривая произведение типов как бинарную операцию, мы видим, что изоморфизм выше очень похож на ассоциативный закон в моноидах:

(a * b) * c = a * (b * c)

Единственная разница в том, что в моноиде оба произведения абсолютно совпадают, а для типов — равны с точностью до изоморфизма.

Если счесть это различие несущественным, то можно продлить аналогию с моноидами далее и показать, что синглтон () является нейтральным элементом относительно умножения типов, так же как 1 нейтральна относительно умножения чисел. Действительно, присоединение () к элементу типа a не добавляет никакой информации. Тип

(a, ())

изоморфен a, где изоморфизм задается функциями

rho :: (a, ()) -> a
rho (x, ()) = x

rho_inv :: a -> (a, ())
rho_inv x = (x, ())

Наши наблюдения можно формализовать в виде утверждения, что категория множеств Set является моноидальной, т. е. категорией, которая является еще и моноидом относительно умножения объектов (в данном случае — относительно декартова произведения). Ниже будет дано строгое определение.

В Haskell доступен более общий способ задания произведений, особенно удобный, как мы вскоре убедимся, когда они сочетаются с суммами типов. Воспользуемся именованными конструкторами с несколькими аргументами. Например, альтернативное определение пары выглядит так:

data Pair a b = P a b

Здесь Pair a b — это имя конструктора типов, параметризованное двумя другими типами a и b, а P — имя конструктора данных. Мы определяем конкретный тип, передавая в конструктор типов Pair два типа, и создаем пару этого типа, передавая соответствующе типизированные значения в конструктор P. Например, определим переменную stmt как пару из String и Bool:

stmt :: Pair String Bool
stmt = P "This statement is" False

Первая строка — это декларация типа. Она состоит из конструктора типов Pair с String и Bool вместо a и b. Вторая строка определяет значение переменной, полученное применением конструктора данных P к конкретным строке и логическому значению. Еще раз: конструкторы типов используются для конструирования типов, конструкторы данных — для конструирования значений.

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

data Pair a b = Pair a b

Если посмотреть на встроенный тип пары с ленинским прищуром, то она признается, что на самом деле является вариацией на тему последней декларации, только конструктор Pair заменен на бинарный оператор (,). Можно использовать (,) так же, как и любой другой именованный конструктор, в префиксной нотации:

stmt = (,) "This statement is" False

Аналогично (,,) конструирует тройки и т. д.

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

data Stmt = Stmt String Bool

представляет собой произведение String и Bool, но обладает собственным именем и конструктором. Преимущество такого определения в том, что можно завести много типов с одним и тем же содержимым, но различной семантикой и функциональностью, которые система типов не позволит смешивать между собой.

Программирование на кортежах и многоаргументных конструкторах часто ведет к неразберихе и ошибкам, потому что надо все время отслеживать, какой компонент за что отвечает. Было бы лучше иметь возможность давать компонентам имена собственные. Произведение типов с именованными полями называется записью в Haskell и struct в C.

Записи

Рассмотрим простой пример. Будем описывать химические элементы единой структурой, состоящей из двух строк (латинского названия и символа) и целого числа, соответствующего атомной массе. Для этого можно воспользоваться кортежем (String, String, Int) и все время держать в голове, какой компонент за что отвечает. Для извлечения компонент из кортежа будем применять сопоставление с образцом. Следующая функция проверяет, является ли символ химического элемента префиксом его латинского названия (например, He — префикс Helium):

startsWithSymbol :: (String, String, Int) -> Bool
startsWithSymbol (name, symbol, _) = isPrefixOf symbol name

В таком коде легко ошибиться, его трудно читать и поддерживать. Гораздо лучше определить вместо кортежа запись:

data Element = Element { name         :: String
                       , symbol       :: String
                       , atomicNumber :: Int }

Эти представления изоморфны, в чем можно убедиться при помощи следующих взаимнообратных преобразований:

tupleToElem :: (String, String, Int) -> Element
tupleToElem (n, s, a) = Element { name = n
                                , symbol = s
                                , atomicNumber = a }

elemToTuple :: Element -> (String, String, Int)
elemToTuple e = (name e, symbol e, atomicNumber e)

Заметим, что имена полей записи одновременно являются и функциями-аксессорами. Например, atomicNumber e возвращает поле atomicNumber записи e. Таким образом функция atomicNumber имеет тип:

atomicNumber :: Element -> Int

С использованием записей типа Element функция startsWithSymbol становится более читаемой:

startsWithSymbol :: Element -> Bool
startsWithSymbol e = isPrefixOf (symbol e) (name e)

В Haskell можно провернуть трюк, превращающий функцию isPrefixOf в инфиксный оператор, обрамив ее обратными апострофами. Это делает код более читаемым:

startsWithSymbol e = symbol e `isPrefixOf` name e

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

Сумма типов

Аналогично тому, как произведение в категории множеств индуцирует произведения типов, копроизведение порождает суммы типов. Каноническая реализация суммы типов в Haskell такова:

data Either a b = Left a | Right b

Как и пары, Either-ы коммутативны (с точностью до изоморфизма), могут быть вложенными, причем порядок вложения не важен (с точностью до изоморфизма). Например, сумма трех типов выглядит так:

data OneOfThree a b c = Sinistral a | Medial b | Dextral c

Оказывается, что Set образует (симметричную) моноидальную категорию относительно операции копроизведения. Место бинарной операции занимает дизъюнктная сумма, а нейтральным элементом является инициальный объект. В терминах типов Either — моноидальная операция, а ненаселенный тип Void — нейтральный элемент ее. Считайте, что Either — это сложение, а Void — это нуль. Действительно, добавление Void к сумме типов не изменяет множество значений типа. Например,

Either a Void

изоморфно a. Действительно, поскольку тип Void не населен, то нет никакого способа построить Right-значение. Значит, единственными обитателями Either a Void являются Left-значения, которые являются просто оберткой над значением типа a. Символически это может быть записано как a + 0 = a.

Суммы типов очень часто встречаются в Haskell. В C++ их аналоги (объединения или варианты) используются существенно реже по ряду причин.

Во-первых, простейшие суммы типов — это перечисления, которые реализованы в C++ при помощи enum. Эквивалентом

data Color = Red | Green | Blue

в C++ будет

enum { Red, Green, Blue };

Еще более простая сумма типов

data Bool = True | False

в C++ является примитивным типом bool.

Далее, суммы типов, кодирующие наличие или отсутствие значения, реализуются в C++ при помощи различных трюков с "невозможными" значениями, такими как пустые строки, отрицательные числа, нулевые указатели и т. д. В Haskell явная, намеренная опциональность значения записывается при помощи Maybe:

data Maybe a = Nothing | Just a

Тип Maybe является суммой двух типов. Мысленно превратим его конструкторы в отдельные типы. Первый примет вид:

data NothingType = Nothing

Это перечисление с единственным значением Nothing. Другими словами, это синглтон, эквивалентный типу (). Вторая часть

data JustType a = Just a

представляет собой обертку над типом a. Мы могли бы записать Maybe как

data Maybe a = Either () a

Более сложные суммы типов фабрикуются в C++ при помощи указателей. Указатель может быть либо нулевым, либо указывать на значение определенного типа. Например, в Haskell список определен как (рекурсивная) сумма типов:

List a = Nil | Cons a (List a)

В C++ этот же тип записывается так:

template<class A>
class List {
    Node<A> * _head;
public:
    List() : _head(nullptr) {}  // Nil
    List(A a, List<A> l)        // Cons
      : _head(new Node<A>(a, l))
    {}
};

Нулевой указатель здесь кодирует пустой список.

Заметим, что конструкторы Nil and Cons из Haskell превратились в два перегруженных конструктора класса List с аналогичными аргументами: без аргументов в случае Nil, значение и список для Cons. Класс List не нуждается в метке, которая бы отличала компоненты суммы типов; вместо этого он использует специальное значение nullptr для _head, чтобы представить Nil.

Важное различие между типами в Haskell и в C++ состоит в том, что в Haskell структуры данных иммутабельны. Если объект был создан при помощи определенного конструктора, то он навсегда запомнит, какой конструктор и с какими аргументами использовался. Так экземпляр класса Maybe, созданный как Just "energy", никогда не обернется Nothing. Аналогично пустой список навсегда останется пустым, а трехэлементный список всегда будет хранить одни и те же три элемента.

Иммутабельность делает конструкторы обратимыми: объект всегда можно разобрать на составные части, использованные при его создании. Такая деконструкция выполняется путем сопоставления с образцом, в качестве которого выступает тот или иной конструктор. Аргументы конструктора замещаются именами переменных (или другими образцами).

У типа List два конструктора, так что деконструкция произвольного List состоит из двух соответствующих сопоставлений с образцом. Первый образец совпадает с пустым списком Nil, второй — со списком, созданным при помощи Cons. Для примера определим простую функцию:

maybeTail :: List a -> Maybe (List a)
maybeTail Nil = Nothing
maybeTail (Cons _ t) = Just t

Первая часть определения maybeTail использует конструктор Nil как образец для сопоставления и возвращает Nothing. Вторая часть использует в качестве образца конструктор Cons. Первый аргумент образца представлен прочерком, поскольку нас не интересует содержащееся в нем значение. Второй аргумент Cons связывается с переменной t (здесь и далее мы будем говорить о переменных, хотя, строго говоря, они неизменны: единожды связанная со значением переменная никогда не меняется). Значение функции на этом образце равно Just t. Итак, в зависимости от способа создания значения типа List, оно совпадет с одним из образцов. Если оно было создано при помощи Cons, то функция получит оба использованных при этом аргумента (первый из которых будет проигнорирован).

Более сложные суммы типов реализуются в C++ иерархией полиморфных классов. Семейство классов с общим прародителем можно трактовать как сумму типов, в которой неявной меткой компоненты служит таблица виртуальных функций. То, чему в Haskell служит сопоставлением с образцом, реализуется в C++ вызовом функции диспетчеризации.

Читатель редко встретится в C++ с использованием union в качестве суммы типов из-за его чрезмерной ограниченности. В union нельзя поместить даже std::string, потому что у этого класса есть конструктор копирования.

Алгебра типов

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

Подведем итоги вышеизложенного. Мы рассмотрели две коммутативные моноидальные структуры, лежащие в основе системы типов. Это сумма типов с нейтральным элементом Void и произведение типов с нейтральным элементом (). Их удобно представлять себе как сложение и умножение. В таком случае Void соответствует нулю, а () — единице.

Посмотрим, как далеко простирается эта аналогия. Например, верно ли, что умножение на ноль дает ноль? Другими словами, изоморфно ли любое произведение на Void типу Void?

Существуют ли пары, состоящие из, скажем, Int и Void? Для создания пары нужны оба значения. Значение типа Int — это не проблема, а вот с Void есть загвоздка: этот тип не населен (не существует ни одного значения этого типа). Таким образом, для любого типа a тип (a, Void) также не населен и, следовательно, эквивалентен Void. Другими словами, a*0 = 0.

Сложение и умножение чисел связаны дистрибутивным законом:

a * (b + c) = a * b + a * c

Выполняется ли он для суммы и произведения типов? Да, с точностью до изоморфизма. Левая часть тождества соответствует типу

(a, Either b c)

а правая —

Either (a, b) (a, c)

Предъявим функции, которые преобразуют типы туда и обратно:

prodToSum :: (a, Either b c) -> Either (a, b) (a, c)
prodToSum (x, e) =
    case e of
      Left  y -> Left  (x, y)
      Right z -> Right (x, z)

sumToProd :: Either (a, b) (a, c) -> (a, Either b c)
sumToProd e =
    case e of
      Left  (x, y) -> (x, Left  y)
      Right (x, z) -> (x, Right z)

Конструкция case of используется для сопоставления с образцом внутри функции. Стрелка разделяет образец и соответствующее ему выражение. Например, при вызове prodToSum с аргументом

prod1 :: (Int, Either String Float)
prod1 = (2, Left "Hi!")

переменная e в case e of будет равна Left "Hi!". Она совпадет с образцом Left y, подставляя "Hi!" вместо y. Поскольку переменная x ранее уже была связана с 2, результатом конструкции case of (и всей функции) будет, как и ожидалось, Left (2, "Hi!").

Доказательство того, что функции выше взаимнообратны, оставим читателю в качестве упражнения. Они лишь перепаковывают одни и те же данные из одного формата в другой.

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

Числа	Типы
0	Void
1	()
a + b	Either a b = Left a | Right b
a * b	(a, b) или Pair a b = Pair a b
2 = 1 + 1	data Bool = True | False
1 + a	data Maybe = Nothing | Just a

Тип списка представляет особый интерес, поскольку он определен как решение уравнения. Определяемый тип встречается в обеих сторонах равенства:

List a = Nil | Cons a (List a)

Произведя обычные подстановки и заменив List a на x, получим

x = 1 + a * x

Это уравнение нельзя решить традиционными алгебраическими методами, поскольку типы нельзя вычитать или делить. Попробуем рекурсивно подставлять вместо x справа выражение (1 + a*x) и раскрывать скобки по дистрибутивности. Получим

x = 1 + a*x
x = 1 + a*(1 + a*x) = 1 + a + a*a*x
x = 1 + a + a*a*(1 + a*x) = 1 + a + a*a + a*a*a*x
...
x = 1 + a + a*a + a*a*a + a*a*a*a...

В конце концов мы придем к бесконечной сумме произведений (кортежей), которую можно трактовать так: список либо пуст, 1; либо состоит из одного элемента, a; либо состоит из пары, a*a; либо из тройки, a*a*a, и т. д. Полученное формально определение полностью отвечает интуитивному представлению о списке как о строке, где вместо букв — значения типа a.

Мы вернемся к спискам и другим рекурсивным структурам далее, после изучения функторов и неподвижных точек.

Решение уравнений с символьными переменными — это алгебра! Поэтому такие типы данных и называются алгебраическими (АТД).

Подводя итоги, дадим одну очень важную интерпретацию алгебры типов. Заметим, что произведение типов a и b должно содержать и значение типа a, и значение типа b, что влечет населенность обоих типов. С другой стороны, сумма типов содержит либо значение типа a, либо значение типа b, так что достаточно, чтобы хотя бы один из них был населен. Логические операции конъюнкции и дизъюнкции образует полукольцо, находящееся в следующем соответствии с алгеброй типов:

Логика	Типы
false	Void
true	()
a || b	Either a b = Left a | Right b
a && b	(a, b)

Эта аналогия может быть углублена и является основой изоморфизма Карри-Говарда между логикой и теорией типов. Мы вернемся к этому вопросу при рассмотрении функциональных типов.

Упражнения

1. Покажите, что Maybe a и Either () a изоморфны.
   
2. Рассмотрим следующую сумму типов в Haskell:

   data Shape = Circle Float
              | Rect Float Float
   

   
   Чтобы определить на типе Shape функцию area, воспользуемся сопоставлением с образцом:

   area :: Shape -> Float
   area (Circle r) = pi * r * r
   area (Rect d h) = d * h
   

   
   Реализуйте Shape на C++ или Java как интерфейс и создайте два класса: Circle и Rect. Затем запишите area как виртуальную функцию.
   
3. (Продолжение) Несложно добавить новую функцию circ, которая вычисляет периметр Shape. В Haskell определение типа Shape останется неизменным; следующий код можно добавить в любое место программы:

   circ :: Shape -> Float
   circ (Circle r) = 2.0 * pi * r
   circ (Rect d h) = 2.0 * (d + h)
   

   
   Добавьте circ в вашу программу на C++ или Java. Какие части оригинальной программы пришлось модифицировать?
   
4. (Продолжение) Добавьте в тип Shape новую фигуру Square и внесите соответствующие обновления в остальной код. Что пришлось поменять в Haskell? А что в C++ или Java? (Даже если вы не знаете Haskell, изменения должны быть довольно очевидны.)
   
5. Покажите, что формальное тождество a + a = 2 * a выполняется для типов (с точностью до изоморфизма). Напоминаем, 2 на языке типов соответствует Bool (см. таблицу выше).
   

Благодарности

Автор благодарен Гершому Базерману за рецензирование поста и полезные комментарии.

This entry passed through the Full-Text RSS service - if this is your content and you're reading it on someone else's site, please read the FAQ at http://ift.tt/jcXqJW.