Алгебраические типы данных и их использование в программировании

[lionet]

Алгебраические типы данных и их использование в программировании

Роман Душкин

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

Comments

[bebos]

На странице 108 используется оператор А → Б (стрелочка). Я не смог найти его описания. По контексту, вроде как выходит, оператор возвращает тип функция. Функция такого типа принимает значение типа А и возвращает значание типа Б. И запись A → (List(A) → List(A)) следует понимать так: сначала поределятеся функция которая принимает А и врозвращает функцию которая принимает List(A) и возвращает List(A). Но выходит, записть A → (List(A) → List(A)) определяет тип функций которые принимают значание типа А и возвращают функцию типа (List(A) → List(A)). До этого же написано #prefix "принимает на вход __значение заданного типа и список__, а возвращает __пару__". Потому такое мое наивное толкование неверно. Как правильно?

[lionet]

Проблем с "значением заданного типа и списком" у меня нет; а откуда пара-то там, при живом List(A)?

А, понял. Это не "пара" в смысле 2-кортеж (не результат применения оператора (,) к двум аргументам), а это ячейка списка, с двумя значениями: головой и хвостом. Результат применения оператора (:) к двум аргументам.

[alexey_rom]

По ревизии 625, нумерация страниц для больших экранов:

Первые две страницы:
1. Примечание насчёт того, что основы перехода к точным определениям заложил Кантор (а не, например, Коши и Вейерштрасс) -- это такая шутка?

2. Первая теорема Гёделя сформулирована неправильно: для достаточно сложных непротиворечивых формальных систем найдутся формулы, которые нельзя ни доказать, ни опровергнутьВ приведённой формулировке она либо тривиально неверна (если противоречивые системы могут быть достаточно сложными), либо так же тривиально верна (в противном случае

[ex_beshenov]

ADT, вроде, появились в Hope, где-то в 1980-м.

ML - ca 1973. Теоретически, у него могли быть потомки без ADT.

В SASL Тёрнера (1972) не было, кажется, но он не потомок ML.
Зато потом Тёрнер сделал KRC (1981), который можно считать ML,
и, вероятно, там не было ADT, они появились уже в Miranda.

Но это надо проверить.

[alexey_rom]

Во введении http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html сказано

Not only did he invent the LCF-approach to theorem proving, but he also designed the ML programming language underlying it and the innovative polymorphic type system used both by ML and the LCF and HOL logics.

Подробнее, к сожалению, не объясняется. Но если там была какая-то другая полиморфная система типов, то куда она делась в SML и OCaml?

[ex_beshenov]

(Не совсем понял, почему полиморфная система типов обязательно ассоциируется с ADT.)

Не хочу строить догадки, надо кое-что проверить.

Но в статье SPJ для HOPL сказано:

Several significant meetings took place in the early ’80s that lent additional impetus to the field. In August 1980, the first Lisp conference took place in Stanford, California. Presentations included Rod Burstall, Dave MacQueen, and Don Sannella on Hope, the language that introduced algebraic data types (Burstall et al., 1980).

[thedeemon]

Извиняюсь, если вопрос прозвучит сумбурно.

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

У нас есть базовые элементы-типы и две операции - умножение и сложение, которые дают нам строить более сложные типы. Да, слагаемым может быть произведение, но может и не быть. Зачем говорить, что любая сумма - именно сумма произведений?

[thedeemon]

Я тоже так подумал, но это уже следствие, а не определение.
Для определения АТД достаточно, что это сумма слагаемых, где слагаемые - типы. Уточнять, что это произведения, в которых число множителей может быть 1 или 0 несколько излишне, имхо.

Мы же не говорим, что в декартовом произведении типов множители - это суммы, где число слагаемых может быть 1. :)

[thedeemon]

6.3.1 "Как уже упоминалось, в языке Haskell любой непримитивный тип данных являет-
ся алгебраическим." И тут же сноска на контрпример - функциональный тип. Нехорошо.

[nponeccop]

Функциональный - это data (->) a b = (->) a b

[thedeemon]

Правда? Круто!
Тогда не совсем понятен оборот "С другой стороны, в языке Haskell имеется понятие «функциональный тип»".

[nponeccop]

Это уже недостаток автора и рецензентов. Интересно, сколько их было, раз говорится во множественном числе?

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

[thedeemon]

Еще стоил упоминания вопрос пересечения наборов конструкторов разных типов. Polymorphic variants и связанные с ними штуки.

[nponeccop]

пересечения наборов конструкторов разных типов??

[thedeemon]

Именно!
В Хаскелле этого нету? Ну хоть чего-то. :)

[nponeccop]

Их там нету из-за особенности алгоритма вывода типов. Вряд ли стоило перегружать этим статью.