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

[@Kyarginski]

Красивые картинки! :-)

[@Halt]

Скажите пожалуйста, а в чем смысл этой статьи? Какие цели вы преследовали, при ее написании?

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

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

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

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

[@cypok]

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

Итого про existential types, GADT с интересом прочитал в других местах, а вот про ограничения по kind найти не удалось, хотелось увидеть мотивацию и примеры, где это необходимо. Если кто подкинет ссылочку, буду благодарен!

[@Halt]

Про экзистенциальные типы отлично написано опять же в «практике», но уже в четвертом выпуске.

[@Vitter]

добавил пример с ограничениями. Вектор с натуральными числами в качестве длины

data Ze
data Su n

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

[@cypok]

Спасибо! Вот в таком примере сразу понятно, зачем эти kind signatures, а то ведь обычно компилятор и сам успешно справляется с их выводом.

[@Vitter]

Я убрал примеры с монадами.
Отличие АТД от других одно — АТД — это универсальный тип данных. С помощью него можно представить большинство типов данных.
Добавил и это.
Собственно, это я и постарался показать — типы данных, которые можно создать благодаря АТД.
Это всё один тип данных.
Что касается pattern matching — механизм не используется в императивных языках, и, соответственно, понять этот плюс сложно.

[@KAndy]

pattern matching — механизм не используется в императивных языках

всегда думал что код типа
switch typeof a
case 'int':…
case 'string''…
default:…
}
или try/catch являються по сути pattern matching
возможно ошибался

[@ilammy]

Под сопоставлением с образцом обычно понимают сопоставление со структурой данных. То есть не просто a имеет какой-то тип, а ещё и содержимое a обладает определённой структурой.

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

[@Terranz]

a имеет какой-то тип, а ещё и содержимое a обладает определённой структурой

тоесть, предполагается наличие одного типа, но с разной внутренней структурой?

[@art_of_press]

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

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

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

Представьте, что вы в паттерне укажете данные типа Bool. Это будет ведь бессмысленно, правда?

[@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]

[@Vitter]

спасибо! Я думал об этом, но постарался не использовать классы. Ведь понять, что такое экзистенциальные типы достаточно сложно

[@cypok]

Просто в вашем варианте HeteroData — это реально черный ящик, ничего и никак с его значением не сделать. Это сразу наводит на мысли, что что-то нам недорассказали. При дальнейшем поиске я и нашел, что в реальном мире эта фича часто употребляется именно вместе с классами.

[@Vitter]

Да, она употребляется либо с классами, либо с «уничтожителем» экзистенциальности.
Например:

data HeteroDataBool = forall a. HDB a (a -> Bool)

toBool :: HeteroDataBool -> Bool
toBool (HDB x f) = f x

[@Shekeen]

Возникло ощущение, что это перевод — встречаются обороты, присущие иностранному языку и странно смотрящиеся в русском. Если так, то дайте, пожалуйста, ссылку на оригинал, а лучше статью оформите как перевод. Если я не прав, то прошу прощения.

[@Vitter]

Нет, это не перевод. Если встретите дикие обороты — могу об этом почитать в личке

[@Vitter]

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

[@Vitter]

почему нельзя?

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

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

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

[@art_of_press]

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

[@Vitter]

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

[@art_of_press]

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

Двоеточие в качестве первого символа конструктора нужно использовать, когда сам конструктор состоит из специальных символов (например, @@, +++, @!* и т.д.), исключением является конструктор пустого списка [ ], который состоит из спецсимволов, но не имеет двоеточия в качестве первого символа. И да — конструкторы, состоящие из спецсимволов, используются обычно в инфиксной нотации.

[@Vitter]

Мы можем вычитание выразить сложением, но оно от этого сложением на становится по сути.
Аналогично и с кванторами. То что мы квантор экзистенциальности / существования преобразовали из квантора всеобщности, типы от этого не становятся всеобщими по сути.
Как-то так )
вроде…

[@Vitter]

а каковы ваши мысли по этому поводу?

[@Vitter]

Согласно Сколему, каждый экзистенциально-квантифицированный тип ранга n+1 можно преобразовать в универсально-квантифицированный тип ранга n.
(∃b. F(b)) -> Int
можно преобразовать в
∀b. (F(b) -> Int)

[@Vitter]

Не совсем так.
Правильнее было бы написать так:
a - b ≡ a + negative(b)