Алгебраические типы данных и их использование в программировании
Алгебраические типы данных и их использование в программировании
Роман Душкин
Аннотация Статья рассматривает важную идиому программирования - алгебраический тип данных (АТД). Приводится теоретическая база, которая лежит в основе практического применения АТД в различных языках программирования. Прикладные аспекты рассматриваются на языке ( Read more... )
Роман Душкин
Аннотация Статья рассматривает важную идиому программирования - алгебраический тип данных (АТД). Приводится теоретическая база, которая лежит в основе практического применения АТД в различных языках программирования. Прикладные аспекты рассматриваются на языке ( Read more... )
Первые две страницы:
1. Примечание насчёт того, что основы перехода к точным определениям заложил Кантор (а не, например, Коши и Вейерштрасс) -- это такая шутка?
2. Первая теорема Гёделя сформулирована неправильно: для достаточно сложных непротиворечивых формальных систем найдутся формулы, которые нельзя ни доказать, ни опровергнутьВ приведённой формулировке она либо тривиально неверна (если противоречивые системы могут быть достаточно сложными), либо так же тривиально верна (в противном случае ( ... )
Reply
ML - ca 1973. Теоретически, у него могли быть потомки без ADT.
В SASL Тёрнера (1972) не было, кажется, но он не потомок ML.
Зато потом Тёрнер сделал KRC (1981), который можно считать ML,
и, вероятно, там не было ADT, они появились уже в Miranda.
Но это надо проверить.
Reply
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?
Reply
Не хочу строить догадки, надо кое-что проверить.
Но в статье 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).
Reply
absrectype α bitree = α + (α bitree × α bitree)
with sons(t) = ...
and maketree(t,t') = ...
and tiptree(a) = ...
Указано, что эта конструкция включена в ML и описана в tech report 1977-го года.
Reply
Reply
Reply
Эээ.. Вы предлагаете все языки с ADT приводить? Есть очень мелкие и никому не интересные языки. Мне кажется, тут как раз в статье нормально.
Вы лучше приведенный список литературы прошерстите. Как и положено в публикациях русских авторов, он "для вида".
Reply
Я предлагаю сказать явно, что перечень неполон.
Впрочем, в статье упомянуты Hope (ну это, возможно, из исторического интереса), Mondrian и Haskell++. 3 упомянутых мной языка кажутся поважнее.
Строчки про F# и OCaml я предложил бы объединить в
"F#, SML, OCaml и другие языки семейства ML". Но это, по большому счёту придирки.
> Вы лучше приведенный список литературы прошерстите.
Да, когда говорится, что "Сегодня под теорией типов понимается" то-то и то-то, ссылка на книгу, написанную до Первой мировой, а изданную в 1925, выглядит странно.
Reply
> типов понимается" то-то и то-то, ссылка на книгу,
> написанную до Первой мировой, а изданную в 1925,
> выглядит странно.
Ну, это бессмысленное теоретическое введение в русских статьях. Русская научная традиция предполагает, что такие введения пролистываются, не читая.
Вы обратите внимание на содержательную часть - например, совершенно непонятно, откуда автор взял свою "теорию АДТ". Вряд ли придумал сам.
Reply
Leave a comment