![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
wizzardРешил перевести для не-англоговорящих коллег найденное
простое и наглядное введение в ADT.
Комментарии и исправления приветствуются :)Ссылка на оригинал – в конце поста.
С увеличением популярности языков вроде F# и Haskell, многие люди впервые сталкиваются с понятием алгебраического типа данных. Когда этот термин употребляется без пояснений, он практически всегда становится источником путаницы. В каком смысле типы «алгебраические»? Есть какие-то параллели между обьектами матанализа и типами данных Haskell? Могу ли я создать тип-«полином»? Нужно ли мне помнить формулу квадрата суммы? Имеют ли смысл преобразования, например, дифференциального исчисления для алгебраических типов данных? Разве это не просто набор абстрактных слов?
Мы рассмотрим эти вопросы, и постараемся развеять тайну над этим важным концептом функциональных языков.
Алгебраические выражения из типов
Чтобы понять концепцию алгебраических типов данных, нам надо провести параллели между понятиями, которые мы связываем с алгеброй, и понятиями, которые мы связываем с типами данных
В алгебраических выражениях мы можем столкнуться с простой одинокой переменной:
x
В выражении, описывающем тип данных, мы можем столкнуться с обыкновенным типом:
int
Формулы в алгебре могут также быть композицией других выражений, например, мы можем встретить
x*x
И аналогично для типов данных:
int*int
«Произведение» двух типов на самом деле означает тип пар из этих типов. В некоторых языках это записывается как pair<int,int>, но, как станет видно дальше, лучше пока думать об этом как о произведении.
Конечно, формулу выше можно упростить до х**2 (икс квадрат), и т.д. Можно написать и int**2
Среди формул алгебры также можно встретить такое выражение:
x+x
Та же концепция существует для типов:
int+int
«Сумма» двух типов обозначает тип «выбор из двух вариантов», который может иметь либо значение левой части, либо правой (но не оба сразу). В этом примере значок «сумма» может показаться излишним, потому что в любом случае ясно, что значение этого типа имеет тип int.
Но информация, какую же часть мы выбрали, тоже полезна. Рассмотрим тип данных, представляющий собой остаток счета в банке:
type balance = int+int
Мы могли бы интерпретировать значения слева как «оставшиеся деньги» , а значения справа – как «оставшиеся долги»
Поэтому, если мы написали функцию для вывода баланса на экран, она может выглядеть, например, так:
string describe(balance b) {
if (b.is_left()) {
return “The bank owes you $” + b.left();
} else {
return “You owe the bank $” + b.right();
}
}
Для многих людей сумма типов менее очевидна, чем произведение типов. Если вспомнить про аналогию произведения с типом pair<int,int>, то для суммы аналогом являются обьединения (unions) в С, или boost:variant<int,int> в С++.
Теперь мы можем использовать эти функции-комбинирующие-типы чтобы составлять сложные выражения:
(int*int*string)+(date*(string+int))
Точно так же, как мы могли их использовать для составления алгебраических выражений:
(x*x*y)+(z*(y+x))
Но, пожалуй, вначале мы посмотрим на штуку попроще:
1
Что означает «единица» на уровне типов? Так обозначается «единичный тип», который имеет только одно значение, обозначаемое как (). Иметь экземпляр единичного типа не очень-то полезно – ведь наперед известно, что там внутри :). Но он полезен в выражениях, например, если рассмотреть такое уравнение:
1+1=2
Теперь «два» - это тип «бит» (или булево значение), поскольку экземпляр этого типа может принимать либо «левое значение» (заранее известное), либо «правое». Может, вам поможет такой пример:
int+int=2*int
Иными словами, сумма двух типов int – то же самое, что и произведение boolean*int (значение переменной типа boolean скажет вам, по какую сторону суммы находится значение типа int )
Кроме того, как и ожидалось,
1*int=int
Другими словами, иметь пару из единичного типа и int – это то же самое, что иметь просто int (т.к. мы всегда знаем, какое значение имеет экземпляр единичного типа)
Вот еще одно натуральное число, которое заслуживает особого внимания:
0
Это особый тип, известный как «пустое множество» или «void» (слегка отличающийся от типа void в C-подобных языках, простите за перегруженность терминов). В отличие от единичного типа, который имеет одно значение, тип-ничто не имеет значений. Экземпляр этого типа нельзя создать.
Это означает, например, что
1+0=1
Потому что если у вас есть сумма единичного типа слева и пустое множество справа, то у этого типа могут быть только значения «слева» (потому что значение справа нельзя создать), поэтому можно с уверенностью предположить, что эту сумму типов можно упростить до единичного типа.
Аналогично,
1*0=0
Потому что для создания экземпляра пары надо создать экземпляр каждого из его членов – если мы не можем создать экземпляр одного из членов пары, то мы не можем построить целую пару.
Типы, описанные до сих пор, весьма полезны, и, надеюсь, понятно, как они отражают аналогичные алгебраические выражения. Однако полезны и более сложные типы, и более сложные выражения (невзирая на то, что на первый взгляд они могут показаться излишне сложными)
Например, как описать список чисел (list<int>) в виде алгебраических выражений? Чтобы ближе подойти к решению, можно рассмотреть возможные варианты списков, которые мы можем создать. Например, список чисел может быть пустым, может состоять из одного числа, из двух, трех и т.д. Каждое «или» здесь следует понимать как сумму, и таким образом (приняв, что пустой список эквивалентен экземпляру единичного типа), мы приходим к типу, описанному бесконечной суммой:
1+int+int**2+int**3+…+int**n
Мы можем оставить это выражение как есть, или переписать его в виде суммы ряда («Σ-нотация»). Однако, в мире типов такое бесконечное расширение описывается при помощи рекурсивных типов. Рекурсивный тип имеет обозначение (символ), и описывается выражением, внутри которого этот символ обозначает значение этого же типа. В случае нашего списка целых чисел, это записывается так:
μX.(1+int*X)
Это можно произносить как «мю икс, один плюс инт умножить на икс». Забудьте о «мю», если вас смущают греческие буквы, оно всего лишь значит «смотрите, это рекурсивный тип». Важно то, что такой тип следует рассматривать как бесконечно раскрывающееся выражение, которое вы получите, если будете много раз подставлять весь тип вместо переменной Х. К примеру, если подставить его один раз, мы получим:
1+int*(μX.(1+int*X))
И еще раз:
1+int*(1+int*(μX.(1+int*X)))
При помощи свойства дистрибутивности операций * и +, это можно упростить до:
1+int+int**2 * (μX.(1+int*X))
И если мы будем продолжать выполнять эту подстановку дальше, мы получим такую же бесконечную сумму, как мы ожидали для этого списка int’ов.
Хотя этот формализм выглядит далеким от языка описания типов в F#, вы можете быстро туда вернуться, если заменить «мю» на слово «type», «.» на «=», и воспользоваться пустыми конструкторами для обозначения единичных типов. Например:
type IntList = Nil | Cons of int*IntList
аналогичен
μIntList.(1+int*IntList)
Опять тот самый тип списков целых чисел, который мы уже определили (если не считать использования IntList вместо X)
Такое обозначение рекурсивных типов данных немного непривычно, но оно дает те же самые бесконечные ряды, которые мы видим в алгебре, и очень удобно для рекурсивных типов с несколькими ветвями рекурсии, например, вот тип двоичных деревьев Int’ов:
μX.(int+X*X)
Иными словами, бинарное дерево является либо листом (содержащим значение типа int), либо веткой (содержащей еще пару бинарных деревьев)
Мы можем выразить очень большую категорию типов таким способом (более подробно см. «Библия теории типов» (англ.)). Более того, существующие знания алгебры могут быть перенесены в этот мир, где мы находим много похожих вещей. Но эта формализация типов идет глубже, и у нас есть еще нерассмотренные аналогии.
∂ для данных
В мире функционального программирования разрушительное изменение не поощряется, а иногда вообще запрещено. С формальной точки зрения, изменение должно создать новую копию старого значения, оставив обе версии доступными для дальнейшего использования. Эта точка зрения упрощает многие проблемы, которые гораздо более сложны в противном случае, и упрощает рассуждения о программах.
Мы раньше обсуждали способы воссоздания функций-мутаторов, вдохновленные самой известной структурой данных в своем роде: the Zipper
В 2001 году Конор МакБрайд сделал замечательное открытие о алгебраических типах данных, и концепцию молнии, которую он развил 4 года спустя (вместе с соавторами Эбботом, Ганой и Альтенкирхом)
Ключом этого открытия является концепция контекста-с-одной-дыркой. Контекст с дыркой можно рассматривать как тип данных «с дыркой в нём». Это понятие тесно связано с понятием мутации, поскольку значение может быть «обновлено» «затыканием» этой дырки.
Рассмотрим простой пример, тройку целых чисел. Ее тип будет int*int*int, или int**3. Теперь мы можем взять значение этого типа:
(98, 76, 54)
Мы хотим «обновить» одно из этих значений, при помощи «проделывания дыры» в структуре данных там, где мы хотим изменить конкретное значение. Другими словами, мы можем изменить первое, второе или третье значение этого кортежа (используя «_» для обозначения дырки):
(_, 76, 54)
(98, _, 54)
(98, 76, _)
Эти три случая представляют собой все способы «проделывания дыры» в этом кортеже данных, и мы можем отразить это при помощи соответствующего типа. Поскольку случаев три, тип должен быть суммой трех элементов. Каждый элемент состоит из 2 чисел (в разных сочетаниях), поэтому мы можем довольно просто вывести этот тип «однодырочного контекста»:
(int*int)+(int*int)+(int*int)
Иными словами, первые int*int соответствуют типу «(_, 76, 54)», вторые int*int соответствуют типу «(98, _, 54)», и третьи int*int соответствуют типу «(98, 76, _)».
Неплохо бы упростить это выражение, поэтому мы вначале введем квадраты
int**2+int**2+int**2
а потом соединим слагаемые:
3*int**2
Иными словами, тип однодырочного контекста троек целых чисел – один из 3 пар целых чисел.
Теперь странная штука, мы начали с типа
int**3
И, найдя ее «однодырочный контекст», мы получили тип
3*int**2
Это ужасно похоже на производную из дифференциального исчисления!
На самом деле это именно то, что открыл МакБрайд: производная алгебраического типа данных – это тип его «однодырочных контекстов». Расширив эту операцию до рекурсивных типов (см. Его статью), мы можем использовать операцию дифференцирования чтобы автоматически выводить функции для изменения и итерации по произвольным структурам данных.
Статьи по теме:
До МакБрайда, Андре Джоэл изучал концепцию комбинаторных видов (построенную на концепции производящих функций – формализм, сходный с алгебраическими типами данных), где также было открыто использование производной.
МакБрайд также является одним из создателей языка программирования Epigram, языка с мощной теорией типов.
В следующей статье мы рассмотрим реализацию концепции «производных от типов» в краткой программе на Haskell.
* Оригинал статьи: http://blog.lab49.com/archives/3011
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2009-10-31 11:59 pm (UTC)http://community.livejournal.com/fprog/2921.html
no subject
Date: 2009-11-01 06:31 am (UTC)Интересная статья.
Date: 2009-11-01 08:05 am (UTC)Первый ведь vector, а второй list, так ?
Re: Интересная статья.
Date: 2009-11-01 08:20 am (UTC)Re: Интересная статья.
Date: 2009-11-01 08:26 am (UTC)но: на первом варианте не реализовать car/cdr, а на втором не получить длину за O(1).
Re: Интересная статья.
Date: 2009-11-01 09:00 am (UTC)no subject
Date: 2009-11-01 09:23 am (UTC)Алгебраически и int==short*2==bool**32 и любой сложный ADT можно превратить в массив бит, так ?
А из массива бит - в другой сложный ADT.
И это будет одно и тоже ?
Или вот, проще:
Date: 2009-11-01 09:33 am (UTC)Re: Или вот, проще:
Date: 2009-11-01 09:48 am (UTC)Если осознать, почему это так, то может и другие вопросы пропадут?
Re: Или вот, проще:
Date: 2009-11-01 07:49 pm (UTC)() и ((),()) - разные типы
Re: Или вот, проще:
Date: 2009-11-01 08:19 pm (UTC)1 здесь - символ метаязыка, объединяющий все 0-арные конструкторы данных.
Re: Интересная статья.
Date: 2009-11-01 08:33 am (UTC)Re: Интересная статья.
Date: 2009-11-01 11:57 am (UTC)Re: Интересная статья.
Date: 2009-11-01 12:07 pm (UTC)Re: Интересная статья.
Date: 2009-11-01 12:12 pm (UTC)data X = Nil () | List Int XRe: Интересная статья.
Date: 2009-11-01 12:29 pm (UTC)должна быть бесконечной в том же смысле, в котором бесконечно число натуральных чисел
Это стандартный математический термин: либо мы суммируем до конечного n, либо, имея в виду отсутствие верхней границы, пишем бесконечность в качестве верхнего предела (и говорим тоже - бесконечность). В том же Хаскелле конечный Int определяется в документации (GIH) как сумма
а бесконечный Integer как
Re: Интересная статья.
Date: 2009-11-01 12:49 pm (UTC)Не-не-не. Да, конечных списков - бесконечное число, но бесконечного списка среди них нет.
Мне просто показалось интересным, что в сумму (1+int+int**2+int**3+…+int**n+…) входят все списки конечной длины, но не входит бесконечный список. А в μX.(1+int*X) - вроде как входит. Или нет. Неясно. В соответсвующем определении на Haskell - входит, а в записи μX.(1+int*X) - не знаю.
Re: Интересная статья.
Date: 2009-11-01 01:11 pm (UTC)Re: Интересная статья.
Date: 2009-11-01 01:44 pm (UTC)Нет ли здесь антисемитизма?
Re: Интересная статья.
Date: 2009-11-01 02:27 pm (UTC)Re: Интересная статья.
Date: 2009-11-01 02:41 pm (UTC)Зачем нужно иметь гарантию конечности списка? Для анализа завершимости алгоритмов, например. Для гарантии того, что любой map/fold не завесит программу из-за бесконечности списка. Я считаю это важным свойством алгебраических типов данных. (конечно, не тех, которые в хаскеле, так как там какое-то извращение сего понятия.)
Re: Интересная статья.
Date: 2009-11-01 03:10 pm (UTC)Если в языке уже есть рекурсия, то наличие корекурсии ни разу не усложняет такой анализ. Он невозможен в общем виде, и должен быть полноценно-доказательным в частных случаях.
И потом, почему это map должен завесить программу из-за бесконечного списка? Отмэппировав функцию увеличивающую свой аргумент на единицу на бесконечный список двоек мы получим бесконечный список троек.
Это уже от деталей семантики вычислителя зависит, справится ли он с такой простой задачей или спасует :-)
Re: Интересная статья.
Date: 2009-11-01 03:09 pm (UTC)существенно зависят от возможности использовать общерекурсивное описание.
Коиндукция этого не требует.
no subject
Date: 2009-11-01 08:36 am (UTC)int+int+int+int = 4*232 = 234
int*int*int*int = (232)4 = 2128
int*int+int*int = 2*264 = 265
ADT как число = мощность множества
ceil(log2(ADT)) = минимальное число бит которым его можно представить
no subject
Date: 2009-11-01 10:20 am (UTC)no subject
Date: 2009-11-01 11:57 am (UTC)no subject
Date: 2009-11-01 03:41 pm (UTC)no subject
Date: 2009-11-07 07:54 am (UTC)Наверное, стоило назвать эти типы данных «полиномиальными».