February 4th, 2009

with Cat The Cat

Типы данных для программ и железа.

В Parsing Techniques: A Practical Guide иерархия грамматик Хомского содержит пять пунктов:
0. Неограниченные грамматики - и слева и справа в правиле порождения могут быть и терминалы и нетерминалы, основное ограничение - левая часть непуста,
1. Конекстно-зависимые грамматики - αAβ -> ^alpha;γβ, α и β могут быть пусты, а вот γ - нет,
2. Контекстно-свободные - всем привычные A -> α,
3. Регулярные - их можно свести преобразованиями к виду A -> αB, α - строка терминалов,
и 4, последние. Фиксированные - могут описывать только конечное количество строк.

В статье на Википедии последнего пункта нет, почему-то. А в PTAPG он есть.

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

В первой версии PTAPG на это обращали особое внимание - регулярное подмножество грамматик языков используется для ускорения разбора.

Натуральные числа data Nat = Zero | Succ Nat выглядят, как правила порождения регулярной грамматики. Списки уже не могут быть регулярными: data List a = Nil | Cons a (List a) из-за параметра a. Если вместо него подставить хотя бы Nat (не говоря про List Nat), то мы уже не можем свести это комплексное определение к регулярному виду.

Для программ мы можем не беспокоиться о размере данных. Причём настолько, что для некоторых программ особенно хороши именно бесконечные данные.

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

Да и тут может подстерегать опасность:
data Node a = Node2 a a | Node3 a a a
data Tree23 a = Zero a | Succ (Node (Tree23 a))
Рекурсивная ссылка через полиморфный параметр. А по отдельности они выглядят, как фиксированные грамматики. ;)

Хотелось бы и рыбку съесть, и прочее, то есть, и типы данных железа записывать в удобной форме, и полиморфизм сохранить.

В принципе, надо только отслеживать отсутствие рекурсивных ссылок. Это приводит к полнопрограммному анализу, да, ну и что. ;)

Идея классификации типов данных была взята из статьи про обобщённое программирование в зависимых типах данных. Там есть и про конечные типы данных, но совсем немного.