16 января в 04:08

Зоопарк Алгебрaических Типов Данных

В этой статье мы попытаемся рассмотреть всё разнообразие Алгебраических Типов Данных.

Надо сказать, задача это достаточно неподъёмная, и понять человеку, если он ранее с Алгебраическими Типами не имел дело — не очень просто.
АТД были впервые использованы в языке Hope, но основную популярность они приобрели благодаря языкам ML, такими как Standart ML, OCaml, F#, и языку Haskell.
Ныне АТД в той или иной мере поддерживаются в значительно большем количестве языков: Scala, Rust, Nemerle, Racket,…
АТД — это универсальный тип данных. С помощью него можно представить большинство типов данных.
АТД называются алгебраическими, потому что их можно представить как некую алгебраическую композицию типов его составляющих. Это знание даёт своё преимущество: понимая свойства алгебраической композиции, можно посчитать какой тип необходим для построения тех или иных данных.
Будем рассматривать типы на основе языка Haskell, однако подобного с лёгкими изменениями можно добиться в других языках с поддержкой АТД.

Надо отметить, что теории типов, развитые в ХХм веке Расселом, Чёрчем, Мартином-Лёфом получили такую популярность, что ныне (уже в ХХІм веке) появилась теория Гомотопической Теории типов, которая покусилась объяснить фундамент математики.
HoTT
Если кого заинтересовала теория, можно почитать бесплатно свежий труд на английском языке Homotopy Type Theory: Univalent Foundations of Mathematics

Наша же задача посмотреть на Алгебраические Типы Данных. Зачастую данные АТД называют коробочными или обёрнутыми. Они так названы, потому что выглядят как запакованные в коробку данные. Самое интересное, что даже реализация подразумевает хранение не данных, а указателей. Помимо простоты реализации, это даёт действенные механизмы ленивости, коим обладает Хаскель.
Справедливости ради, замечу, что Хаскель позволяет создавать неленивые, в том числе и не обёрнутые данные, что помогает при обработке высоко-нагруженными объёмами данных.
В Хаскеле существует 2 способа создать АТД, с помощью декларации data или newtype. Разница между ними состоит в том, что newtype де-факто не обёрнутый, а значит и более дешёвый (по ресурсам машины), и поэтому более выгодный, но с помощью него можно записать лишь узкий круг АТД, поэтому он не подходит в общем случае.

Типы данных, реализованные через примитивы


В Хаскеле таких немного, прежде всего это такие типы данных, как
Int, Integer, Float, Double, Char,…
Дело не в том, что нельзя составить эти типы по настоящему (через АТД), просто компьютер уже умеет работать с числами, и грех этим не воспользоваться.
Хочу обратить внимание, что все типы пишутся с заглавной буквы, это связано с тем, что все конструкторы типов и данных в Хаскеле пишутся исключительно с заглавной буквы.

Нулевые типы данных


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

Это не настоящие, псевдо-нулевые, пустые типы данных
data S
data T a
data K a b

Синтаксис, как мы видим прост до безобразия.
Тут мы создали 3 типа данных, второй из которых — параметрический. Мы видим, что a пишется с строчной буквы, а значит не может быть конструктором. Вывод — это параметр, в который можно подставлять любой тип, то есть можно иметь следующие типы: T Int, T Char, T S, T (T Double) и даже T (T ( T String)).
Мы также видим, что конструктор стоит вначале типа, а далее данные как бы упаковываются в коробку.
Вы спросите, зачем они нужны?
Например, мы можем писать следующий валидный код функций:
doubleT :: T a -> (T a, T a)
doubleT t = (t, t)

Конечно, в большинстве случаев написать все функции без внутреннего знания о данных нельзя, но можно часть функций оставить на потом, занимаясь другими задачами, такими как эта:
foo :: S -> Int -> T a
foo = undefined

nextT :: S -> Int -> (Int, T a)
nextT s i = (i+1, foo s (i+1))

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

Настоящий нулевой тип данных выглядит достаточно необычно для нетренированного глаза, но мы сможем это понять.
Он был найден сравнительно недавно, всё ещё нет в Платформе (чтобы можно было пользоваться из коробки), и ещё мало используемый.
Void
newtype Void = Void Void

Тут мы видим рекурсивный тип (об этом мы поговорим попозже), вначале идёт имя типа — Void, далее =, далее конструктор этого типа Void и параметр, который является типом Void.
Если мы переименуем, это не изменит ничего, кроме нашего понимания:
newtype VoidData = Void VoidData

Этот тип данных бесконечно зациклен сам на себя.


Единичные типы данных


Единичные типы данных не дают ничего, кроме знания о том, что он есть.
Из распространённых типов данных используются
data () = ()      --X

здесь и далее комментарием
  -- X
будут показаны данные так определённые, но их нельзя определить самому из-за того, что используются недопустимые символы.

Почти во всех программах, используется подпись:
main :: IO ()

потому что программа должна что-то возвращать. Поэтому () является самым популярным типом, когда надо возвращать ничего.
Или, вот ещё известный единичный тип:
data Unit = Unit  

то же самое, только используется обычные конструкторы.
Надо сказать, что в этих типах нет никакой рекурсии, то есть можно записать:
data UnitData = Unit  

дело в том, что пространство имён типов не пересекается с пространством конструкторов типа, поэтому компилятор отлично понимает где есть рекурсия, а где нет.

Типы произведений


Типы произведений названы так, что их можно представить как произведение нескольких типов, которые его составляют.
Очень популярные типы данных, используются повсеместно.
Самые известные из них, это кортежи или туплы. В Хаскеле используется специальный синтаксический сахар для этого:
data (,) a b        = (,) a b            --X  (a, b)
data (,,) a b c     = (,,) a b c         --X  (a, b, c)
data (,,,,) a b c d = (,,,,) a b c d     --X  (a, b, c, d)

то же самое мы можем записать и с помощью обычных конструкторов:
data Pair a b = Pair a b
data Triple a b c = Triple a b c

Везде где нужно хранить более одного данного в данных — это тип произведений.

Суммарные типы данных


Суммарные типы данных названы потому, что они суммируют типы данных, которые их составляют.
Например, если суммировать единичные типы данных, получается перечисление.
Представляю один из самых знаменитых перечислений:
data Bool = False | True

так же известным перечислением является тип Ordering, который используется в сравнениях
data Ordering = LT | EQ | GT

Если перейдём к более сложным АТД, тут необходимо вспомнить нулл-абельный тип:
data Maybe a = Nothing | Just a

Данные, которые имеют поле для результата, когда его нет, так сказать null из многих языков программирования.
(</>) :: Int -> Int -> Maybe Int
_ </> 0 = Nothing
a </> b = Just (a `div` b)

Если необходимо более детально узнать об ошибке, используется ещё более сложный тип данных:
data Either a b = Left a | Right b

тип данных, где есть либо «левый» результат (описание ошибки или сама ошибка), либо «правильный» результат.
Также этот тип данных используют для бинарного выбора.
type IdPerson = Int
type ErrorMsg = String

personChecker :: Person -> Either ErrorMsg IdPerson
personChecker p = if age p < 0          then Left "this guy is not born yet!"
            else if null $ first_name p then Left "this guy is unnamed!"
            else Right $ registeredId p

Можно составлять и более экзотические типы данных, например:
data Both a b = None | First a | Second b | Both a b

тут у нас либо нет результата, либо 1 результат, либо 2й, либо и 1й и 2й.

Рекурсивные типы данных


В Хаскеле спокойно можно создать рекурсивные типы данных.
Самым известным, использующий синтаксический сахар, типом являются списки:
data [] a = [] | a : [a]     --X

Однако его можно легко переписать словами:
data List a = Nil | Cons a (List a)

Хочу заметить, что в качестве конструкторов могут использоваться спец-символы, где первый символ обязательно двоеточие (:), тогда пользуются инфиксной записью.
Хотим построить дерево? Да без проблем.
Например, простое бинарное дерево:
data Tree a = Leaf a | Branch (Tree a) (Tree a)
data Tree2 a = Empty | Branch2 (Tree2 a) a (Tree2 a)

Или вот ещё, натуральные числа:
data Nat = Zero | Succ Nat

Если вы ещё не открыли спойлер о нулевом типе данных (или открыли, но не поняли) — самое время открыть и почитать и понять, что Void элементарный бесконечно-рекурсивный тип данных.

Степенные типы данных


Не надо думать, что в АТД можно записать лишь данные. Функции тоже легко могут быть записаны в АТД: степенные типы (общий тип имеет мощность возведения в степень одного типа данных в мощность другого):
data Fun a b = Fun (a -> b)
newtype ContT r m a = Writer ((a -> m r) -> m r)

Если мы будем использовать АТД произведений, где данные будут вперемешку с функциями — это ни что иное, как записи, и очень похожие структуры на объекты.

Фантомные типы данных


Иногда приходится создавать достаточно необычное поведение, и приходится изобретать типы, которые ничего не делают, но делают вид, что делают. Для этого используют, в частности, фантомные типы. Одним из самых известных типов является:
data Proxy a = Proxy

Как видим, в заголовке типа сказано, что тип параметрический, однако в реальности это пустышка.
Такие типы данных зачастую используются как универсальные затычки, поскольку они легко конвертируются из одних типов данных в другие
proxyСonverter :: Proxy a -> Proxy b
proxyСonverter Proxy = Proxy


Записи


Тип произведений настолько часто пользуется, что есть специальный синтаксический сахар, который помогает легче и удобней работать с ним (со встроенными геттерами и сеттерами). Такие типы называются записями.
Пусть у нас есть тип
data Sex =  Female | Male
data Person = Person String String Int Int Sex (String -> String)

значительно удобнее переписать в:
data Sex =  Female | Male
data Person = Person  { lastName  :: String
                      , firstName :: String
                      , age       :: Int 
                      , socialId  :: Int 
                      , sex       :: Sex
                      , greeting  :: String -> String
                      }


Вставки или Враперы

Вставки пользуются там, где необходимо либо скрыть реализацию типа, защитить от постороннего вмешательства, либо для придания других свойств, нежели материнский тип.
Записывается он подобным образом (с синтаксисом записей):
newtype Wrapper a = Wrapper { unwrapper :: a }
newtype Dollar = Dollar Int


Экзистенциальные типы данных


Экзистенциальные типы данных названы так из-за квантора существования ∃.
Парадокс состоит в том, что в Хаскеле нет такого квантора.
Зато есть квантор всеобщности ∀. Но эти кванторы можно легко преобразовать друг в друга.
Если быть совсем точным, то каждый экзистенциально-квантифицированный тип ранга n+1 можно преобразовать в универсально-квантифицированный тип ранга n.
data HeteroData = forall a. HeteroData a

heteroList :: [HeteroData]
heteroList = [HeteroData 3.7, HeteroData "message", HeteroData True]

Как видим, смогли создать гетерогенный список, несмотря на то, что он гомогенный.
А вот что-то похоже на объект:
data Counter a = forall self. NewCounter
    { _this    :: self
    , _inc     :: self -> self
    , _display :: self -> IO ()
    , tag      :: a
    }

С функциями, записанными со знаком подчёркивания мы не можем работать на прямую.
Правда работать с подобными объектами совсем не похоже на работу с ООП:
Запись с экзистенциальной переменной
inc :: Counter a -> Counter a
inc (NewCounter x i d t) = NewCounter { _this = i x, _inc = i, _display = d, tag = t }

display :: Counter a -> IO ()
display NewCounter{ _this = x, _display = d } = d x

counterA :: Counter String
counterA = NewCounter { _this = 0, _inc = (1+), _display = print, tag = "A" }

counterB :: Counter String
counterB = NewCounter { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }

main = do
    display (inc counterA)         -- prints "1"
    display (inc (inc counterB))   -- prints "##"



Обобщённые Алгебраические Типы Данных (GADTs)


Обобщённые АТД отличаются от обычных тем, что урезают и специализируют итоговый тип.
В Хаскеле используется «функциональная» запись этих данных. Давайте перепишем простой тип данных в новом синтаксисе:
data Maybe a = Nothing | Just a

data Maybe a where
    Nothing ::      Maybe a
    Just    :: a -> Maybe a
-- --------------------
data List a = Nil | Cons a (List a)

data List a where
    Nil  ::                List a
    Cons :: a -> List a -> List a

Мы видим, что итоговый тип данных у всех совпадает: Maybe a (или List a). ОАТД позволяют иметь разные итоговые типы данных.
Если мы имеем абстрактное дерево:
  data Term a where
      Lit    :: Int -> Term Int
      Succ   :: Term Int -> Term Int
      IsZero :: Term Int -> Term Bool
      If     :: Term Bool -> Term a -> Term a -> Term a
      Pair   :: Term a -> Term b -> Term (a,b)

то легко построить функцию вычисления подобного дерева:
  eval :: Term a -> a
  eval (Lit i) 	= i
  eval (Succ t)     = 1 + eval t
  eval (IsZero t)   = eval t == 0
  eval (If b e1 e2) = if eval b then eval e1 else eval e2
  eval (Pair e1 e2) = (eval e1, eval e2)


Параметрические типы данных с ограниченными параметрами


Иногда уж больно хочется ограничить параметрические типы данных. Срезаются они ограничением вида(kind) типа.
Вид — по сути это тип типа, например
Just 3 :: (Maybe Int :: *)

А вот и данные с ограничением на параметр:
data F (a :: * -> *) where ...

В основном подобные типы необходимы для очень высоких уровней абстракции.
Vector type
Вектор с натуральными числами в качестве длины
data Ze
data Su n

data Vec :: * -> * -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)


Вывод


Алгебраические Типы Данных — очень простой, универсальный, элегантный, легко расширяемый и мощный инструментарий создания пользовательских типов данных под очень многие нужды программистов.
+33
12787
117
Vitter 16,0

Комментарии (34)

+1
Kyarginski, #
Красивые картинки! :-)
+14
Halt, #
Скажите пожалуйста, а в чем смысл этой статьи? Какие цели вы преследовали, при ее написании?

Если говорить о ней, как о материале для начинающего, то боюсь, что в таком ключе она совершенно не годится. Статья не отвечает на главный вопрос: а в чем, собственно отличия алгебраических типов от традиционных структур данных? Не сказано и о преимуществе АТД конструкторов, которые можно использовать в функциях в подстановках и guard conditions. Не говоря уже о том, что в примерах вы используете монады, которые точно не будут понятны с первого взгляда.

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

Чтобы комментарий не выглядел как откровенный наезд на автора, напишу все же благодарность, ибо любая статья достойна внимания. Тем более, повествующая о нестандартных языках :)

Тем кто действительно хочет разобраться в алгебраических типах данных, конструкторах и прочем, советую почитать материалы журнала «Практика функционального программирования», в частности второй выпуск. Также, не лишним будет упомянуть книгу Learn You a Haskell for a Great Good (в продаже имеется и русский перевод).
+2
cypok, #
Для меня, только знакомого с Haskell (прочитал LYHGG), начало статьи было скучным, а начиная с экзистенциальных типов, пришлось самому искать информацию, потому что приведенная очень обрывочна. Т.е. для меня это был скорее список того, что еще можно почитать.

Итого про existential types, GADT с интересом прочитал в других местах, а вот про ограничения по kind найти не удалось, хотелось увидеть мотивацию и примеры, где это необходимо. Если кто подкинет ссылочку, буду благодарен!
+2
Halt, #
Про экзистенциальные типы отлично написано опять же в «практике», но уже в четвертом выпуске.
+4
Vitter, #
добавил пример с ограничениями. Вектор с натуральными числами в качестве длины
data Ze
data Su n

data Vec :: * -> * -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)
+1
cypok, #
Спасибо! Вот в таком примере сразу понятно, зачем эти kind signatures, а то ведь обычно компилятор и сам успешно справляется с их выводом.
+2
Vitter, #
Я убрал примеры с монадами.
Отличие АТД от других одно — АТД — это универсальный тип данных. С помощью него можно представить большинство типов данных.
Добавил и это.
Собственно, это я и постарался показать — типы данных, которые можно создать благодаря АТД.
Это всё один тип данных.
Что касается pattern matching — механизм не используется в императивных языках, и, соответственно, понять этот плюс сложно.
+1
KAndy, #
pattern matching — механизм не используется в императивных языках

всегда думал что код типа
switch typeof a
case 'int':…
case 'string''…
default:…
}
или try/catch являються по сути pattern matching
возможно ошибался
+5
ilammy, #
Под сопоставлением с образцом обычно понимают сопоставление со структурой данных. То есть не просто a имеет какой-то тип, а ещё и содержимое a обладает определённой структурой.

Однако, в широко используемых императивных языках принят объектно-ориентированный подход, который подразумевает инкапсуляцию структуры объектов. То есть матчить там по сути нечего, разве что тип объекта в дереве наследования (что обозвали полиморфизмом).
0
Terranz, #
a имеет какой-то тип, а ещё и содержимое a обладает определённой структурой

тоесть, предполагается наличие одного типа, но с разной внутренней структурой?
+1
art_of_press, #
Да. Большинство паттернов состоят из значений (в том числе и из присвоенных им имен, которые для удобства можно называть переменными, хотя таковыми они не являются) и конструкторов типа.

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

(++) :: [a] -> [a] -> [a]  --Функция принимает на вход два списка со зачениями типа a и возвращает список со значениями типа a
[] ++ ys = ys --Этот паттерн описывает, что делает функция, когда она применяется к пустому списку
x:xs ++ ys = x : (xs ++ ys) --А этот паттерн описывает, что делает функция, когда применяется к непустым спискам


Представьте, что вы в паттерне укажете данные типа Bool. Это будет ведь бессмысленно, правда?
+3
cypok, #
Как видим, смогли создать гетерогенный список, несмотря на то, что он гомогенный.
Создать-то создали, только что с ним делать? Я бы расширил этот простой пример для понятности, используя ограничение класса типов:

data HeteroData = forall a. Show a => HeteroData a

instance Show HeteroData where
  show (HeteroData x) = show x

list = [HeteroData 3.7, HeteroData "message", HeteroData True]
str = show list -- => [3.7,"message",True]
+3
Vitter, #
спасибо! Я думал об этом, но постарался не использовать классы. Ведь понять, что такое экзистенциальные типы достаточно сложно
+2
cypok, #
Просто в вашем варианте HeteroData — это реально черный ящик, ничего и никак с его значением не сделать. Это сразу наводит на мысли, что что-то нам недорассказали. При дальнейшем поиске я и нашел, что в реальном мире эта фича часто употребляется именно вместе с классами.
+1
Vitter, #
Да, она употребляется либо с классами, либо с «уничтожителем» экзистенциальности.
Например:
data HeteroDataBool = forall a. HDB a (a -> Bool)

toBool :: HeteroDataBool -> Bool
toBool (HDB x f) = f x
+4
Shekeen, #
Возникло ощущение, что это перевод — встречаются обороты, присущие иностранному языку и странно смотрящиеся в русском. Если так, то дайте, пожалуйста, ссылку на оригинал, а лучше статью оформите как перевод. Если я не прав, то прошу прощения.
+2
Vitter, #
Нет, это не перевод. Если встретите дикие обороты — могу об этом почитать в личке
+2
Darkus, #
Это перевод?

Блин, извиняюсь. Сначала написал вопрос, а только потом посмотрел комментарии :).
+2
Darkus, #
Хочу заметить, что в качестве конструкторов могут использоваться спец-символы (:), тогда пользуются инфиксной записью.

Сумбур. Единственный конструктор (:) — это один из конструкторов типа [a]. Другое дело, что при определении своих типов можно использовать спецсимволы, как и при определении функций, и тогда конструктор должен начинаться с (:), а его использование должно быть инфиксным. Равно как и бинарные конструкторы можно использовать в инфиксной форме при помощи заключения их идентификаторов в обратные апострофы. Равно как и инфиксные конструкторы можно использовать в префиксной форме (особенно в вызовах функций высших порядков) при помощи заключения их в круглые скобки.

Ну и терминология несколько необычно. В русском языке уже много устоявшихся терминов, которые Вы здесь не используете, придумывая для них свои.
+1
Vitter, #
Спасибо, исправил.
… в качестве конструкторов могут использоваться спец-символы, например двоеточие (:), тогда пользуются инфиксной записью.
0
Darkus, #
Ну ещё хуже вышло же: Хочу заметить, что в качестве конструкторов могут использоваться спец-символы, например двоеточие (:), тогда пользуются инфиксной записью. Этак можно понять, что в качестве конструктора можно использовать, например, (++++), но ведь нельзя же. А вот (:+) можно, и это конструктор типа Complex a. Конструктор типа, если хочется сделать его инфиксным, должен начинаться с двоеточия, вот и всё правило.
+2
Vitter, #
почему нельзя?

{-# LANGUAGE TypeOperators #-}
data a +++++ c = D (a,c)

d= D ("s","s")

> :t d
d :: [Char] +++++ [Char]

0
Darkus, #
Можно. Но, во-первых, расширение. А во-вторых, плохой стиль.
+2
art_of_press, #
Вы использовали спецсимволы в названии типа, а не в конструкторах типа. Если бы вы их использовали в конструкторах, то вам нужно было бы в качестве первого символа поставить двоеточие (исключением является конструктор пустого списка).
+1
Vitter, #
исправил
… в качестве конструкторов могут использоваться спец-символы, где первый символ обязательно двоеточие (:), тогда пользуются инфиксной записью.
+1
art_of_press, #
Любой конструктор можно сделать инфиксным, использовав его в обратных одинарных кавычках в инфиксной нотации. И любой инфиксный оператор можно использовать в префиксной нотации, заключив его в скобки.

Двоеточие в качестве первого символа конструктора нужно использовать, когда сам конструктор состоит из специальных символов (например, @@, +++, @!* и т.д.), исключением является конструктор пустого списка [ ], который состоит из спецсимволов, но не имеет двоеточия в качестве первого символа. И да — конструкторы, состоящие из спецсимволов, используются обычно в инфиксной нотации.
0
Darkus, #
Я об этом писал в комментарии выше.
+1
Darkus, #
Экзистенциальные типы данных названы так из-за квантора существования ∃.
Парадокс состоит в том, что в Хаскеле нет такого квантора.
Зато есть квантор всеобщности ∀. Но эти кванторы можно легко преобразовать друг в друга.


И почему тогда, раз в языке Haskell нет квантора существования, а есть квантор всеобщности, типы называются экзистенциальными?
+1
Vitter, #
Мы можем вычитание выразить сложением, но оно от этого сложением на становится по сути.
Аналогично и с кванторами. То что мы квантор экзистенциальности / существования преобразовали из квантора всеобщности, типы от этого не становятся всеобщими по сути.
Как-то так )
вроде…
0
Darkus, #
Не так. Вот правила преобразования кванторов друг в друга, взятые из исчисления предикатов первого порядка:

1. ∃x: P(x) = ~(∀x: ~P(x))
2. ∀x: P(x) = ~(∃x: ~P(x))

Чему они соответствуют в языке Haskell?
+1
Vitter, #
а каковы ваши мысли по этому поводу?
+1
Vitter, #
Согласно Сколему, каждый экзистенциально-квантифицированный тип ранга n+1 можно преобразовать в универсально-квантифицированный тип ранга n.
(∃b. F(b)) -> Int
можно преобразовать в
∀b. (F(b) -> Int)
+1
mktums, #
Мы можем вычитание выразить сложением, но оно от этого сложением на становится по сути.

Проясните момент для чайника, ведь a - b ≡ a + (-b).
0
Vitter, #
Не совсем так.
Правильнее было бы написать так:
a - b ≡ a + negative(b)

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