Саймон Пейтон Джонс дал интервью русскоязычному журналу "Практика функционального программирования", где среди прочего рассказал о посещении в этом году Второго международного семинара по метавычислениям Meta-2010, проводимого в Переславле-Залесском.
Про главного автора этого блога - Сергея Романенко - Саймон сказал следующее:
"Для меня было большой честью быть приглашенным на Meta 2010 и встретиться с такими людьми, как Сергей Романенко, сыгравшими важную роль в развитии суперкомпиляции."
PS. Пользуясь случаем, даю ссылку на свой блог, где также время от времени проскальзывают мысли о функциональном программировании и суперкомпиляции, но которые (мысли) еще достаточно сыры или не структурированы надлежащим образом для публикаций в этом блоге.
вторник, 30 ноября 2010 г.
пятница, 30 апреля 2010 г.
Комбинаторные парсеры. Часть 1
В сообщении Проблемно-ориентированные языки и суперкомпиляция был приведен пример реализации парсеров регулярных выражений через комбинаторы.Позволим себе взять подмножество языка регулярных выражений и немного поэкспериментировать с их реализацией через комбинаторные парсеры.
re = a | b | concat re1 re2 | or re1 re2;
Для удобства чтения (or re1 re2) можно записывать как (re1|re2), а конкатенацию (concat re1 re2) - как (re1)(re2).
Результат сопоставление слова языка L с регулярным выражение re определяется так: если существует начальная часть слова, удовлетворяющая выражению, то от слова откусывается такая часть и возвращается оставшаяся часть слова; если же никакая начальная не соответствует выражению, то возвращается неудача.
Мы же разделим понятие алфавит и слова. Конкретный алфавит языка будет представляться конкретным перечислением букв, а слово языка - это список букв.
Что делают функции - понятно:
Попробуем применить парсер par1 к слову ABB. A - соответсвует выражению a, BB - выражению bb. Ожидается, что результатом работы будет Some w1, где w1 - пустое слово.
Поскольку суперкомпилятор можно применять и в качестве интерпретатора, попросим HOSC вычислить выражение par1 (Cons A (Cons B (Cons B Nil))), - как и ожидалось в результате получается (Some Nil).
Пойдем дальше - применим парсер par1 к слову ABA. AB - соответсвует выражению ab, A - выражению a. Опять ожидаем, что результатом работы будет Some w1, где w1 - пустое слово.
Вычисляем выражение par1 (Cons A (Cons B (Cons A Nil))). Получаем ... None!
Как же так? Дерево вычислений, показанное HOSC'ом помогает найти ответ на вопрос - после некоторого числа шагов вычисление исходного выражения сводится (редуцируется) к вычислению выражения (or (concat b b) a) (Cons B (Cons A Nil)), которое завершается неудачей.
Как же решить возникшую проблему? Как сделать, чтобы результирующий парсер (сконструированный из комбинаторов) пробовал все варианты? В нашем случае мы сделали так, что парсер возвращает ровно одно успешное сопоставление. Одно из решений проблемы -- заставить парсер возвращает не одно единственное сопоставление в случае успеха, а все возможные. Ясно, что тогда усложняется логика работы комбинаторов парсеров -- они должны анализировать все сопоставления парсеров, переданных как аргументы. Таким образом парсер or p1 p2 должен возращать объединение результатов парсеров p1 и p2. А парсер (concat p1 p2) должен к каждому из вариантов сопоставления p1 попробовать применить p2 и тоже объединить результаты. Этот подход изложен в классической статье Филиппа Уодлера "How to Replace Failure by a List of Successes (A method for exception handling, backtracking, and pattern matching in lazy functional languages)".
Но можно пойти и другим путем - можно каждому парсеру в качестве дополнительного аргумента передавать парсер, который будет вызван на следующем шаге сопоставления. Такой подход по духу очень близок стилю программированию в продолжениях (Continuation passing style). Действительно, в нашей первой наивной реализации парсер (or (a) (concat a b)) действовал по принципу "После нас хоть потоп" - возвращал всегда первое сопоставление - его не интересовало, пригоден ли его ответ для обработки следующим парсером в цепочке.
Легко кодируются в таком стиле парсеры для выражений a и b.
Комбинатор or записывается так:
concat = \p1 p2 next word -> p1 (p2 next) word;
В итоге для сопоставления выражения (a|ab)(bb|a) со словом ABA получается следующая программа:
Вычисление par1 (Cons A (Cons B (Cons B Nil))) тоже выдает (Some Nil).
Мы реализовали комбинаторный DSL только для подмножества языка регулярных выражений. В следующий раз мы расширим наш маленький DSL до полной поддержки классических регулярных выражений и посмотрим какие проблемы при этом могут возникнуть.
Возьмем простой язык L, алфавит которого состоит всего из двух символов - A и B. Рассмотрим следующее подмножество регулярных выражений для этого языка L:
re = a | b | concat re1 re2 | or re1 re2;
- Слово w соответствует регулярному выражению a, если слово начинает с A, то есть w = A w1.
- Слово w соответствует регулярному выражению b, если слово начинает с B, то есть w = B w1.
- Слово w соответствует регулярному выражению (concat re1 re2), если слово w превставимо в виде w = w1 w2 w3, где w1 - соответсвует re1, а w2 - соответсвует re2.
- Слово w соответствует регулярному выражению (or re1 re2), если оно соответствует либо выражению re1 либо выражению re2.
Для удобства чтения (or re1 re2) можно записывать как (re1|re2), а конкатенацию (concat re1 re2) - как (re1)(re2).
Результат сопоставление слова языка L с регулярным выражение re определяется так: если существует начальная часть слова, удовлетворяющая выражению, то от слова откусывается такая часть и возвращается оставшаяся часть слова; если же никакая начальная не соответствует выражению, то возвращается неудача.
Напишем парсеры и соответствующие комбинаторы для языка L в духе примера из упомянутого послания, но с одним отличием - в том примере алфавит языка и представление слов были жестко связаны вместе:
data Input = Eof | A Input | B Input | C Input;
Мы же разделим понятие алфавит и слова. Конкретный алфавит языка будет представляться конкретным перечислением букв, а слово языка - это список букв.
Получаем что-то в таком духе:
data Symbol = A | B;
data List a = Nil | Cons a (List a);
data Option a = Some a | None;
par1 = concat (or a (concat a b)) (or (concat b b) a);
or = \p1 p2 word -> case p1 word of {
Some word1 -> Some word1;
None -> p2 word;
};
concat = \p1 p2 word -> case p1 word of {
Some word1 -> p2 word1;
None -> None;
};
a = \word -> case word of {
Nil -> None;
Cons sym word1 -> case sym of {
A -> Some word1;
B -> None;
};
};
b = \word -> case word of {
Nil -> None;
Cons sym word1 -> case sym of {
A -> None;
B -> Some word1;
};
};
Что делают функции - понятно:
- a (парсер) - соответствует регулярному выражению a - откусывает (если можно) от слова символ A и возвращает оставшуюся часть. Если слово пустое или не начинается с A, возвращает неуспех.
- b (парсер) - аналогично a
- or (комбинатор парсеров) - берет два парсера p1 и p2 и делает новый парсер, который возвращает результат работы первого парсера, если это успех, а в противном случае возвращает результат второго парсера
- concat (комбинатор парсеров) - конкатенирует (соединяет) два парсера, - делает новый парсер, который возвращает успех, тогда и только тогда, когда первый парсер завершается успешно и второй парсер, примененный к остатку слова, выплюнутому первым парсером, также завершатся успехом.
- par1 - парсер, соответствующий регулярному выражению (a|ab)(bb|a)
Попробуем применить парсер par1 к слову ABB. A - соответсвует выражению a, BB - выражению bb. Ожидается, что результатом работы будет Some w1, где w1 - пустое слово.
Поскольку суперкомпилятор можно применять и в качестве интерпретатора, попросим HOSC вычислить выражение par1 (Cons A (Cons B (Cons B Nil))), - как и ожидалось в результате получается (Some Nil).
Пойдем дальше - применим парсер par1 к слову ABA. AB - соответсвует выражению ab, A - выражению a. Опять ожидаем, что результатом работы будет Some w1, где w1 - пустое слово.
Вычисляем выражение par1 (Cons A (Cons B (Cons A Nil))). Получаем ... None!
Как же так? Дерево вычислений, показанное HOSC'ом помогает найти ответ на вопрос - после некоторого числа шагов вычисление исходного выражения сводится (редуцируется) к вычислению выражения (or (concat b b) a) (Cons B (Cons A Nil)), которое завершается неудачей.
Можно еще отсукомпилировать выражение par1 w для неизвестного слова w. Получается следующий результат:
case w of {
Nil -> None;
Cons u10 x11 ->
case u10 of {
A ->
case x11 of {
Nil -> None;
Cons p3 u13 ->
case p3 of {
A -> (Some u13);
B -> case u13 of {
Nil -> None;
Cons z10 u8 -> case z10 of {
A -> None;
B -> (Some u8);
};
};
Nil -> None;
Cons z10 u8 -> case z10 of {
A -> None;
B -> (Some u8);
};
};
};
};
B -> None;
};
}
Видно, что на самом деле мы закодировали регулярное выражение a(a|bb), или (что то же самое) (aa|abb). Как же так получилось?
Дело в том, что парсер (or (a) (concat a b)) никогда не будет откусывать от слова AB - из-за того, что если парсер (concat a b) способен для данного слова выдать что-то наружу, то на это способен и парсер a, а он вызывается в нашей реализации первым - и получается, что наш комбинатор or работает для парсера (or p1 p2) правильно только в случае, если p1 и p2 не могут выдавать успех на одном и том же слове. Или (говоря более научно), когда языки, определяемые парсерами p1 и p2 не пересекаются.
Как же решить возникшую проблему? Как сделать, чтобы результирующий парсер (сконструированный из комбинаторов) пробовал все варианты? В нашем случае мы сделали так, что парсер возвращает ровно одно успешное сопоставление. Одно из решений проблемы -- заставить парсер возвращает не одно единственное сопоставление в случае успеха, а все возможные. Ясно, что тогда усложняется логика работы комбинаторов парсеров -- они должны анализировать все сопоставления парсеров, переданных как аргументы. Таким образом парсер or p1 p2 должен возращать объединение результатов парсеров p1 и p2. А парсер (concat p1 p2) должен к каждому из вариантов сопоставления p1 попробовать применить p2 и тоже объединить результаты. Этот подход изложен в классической статье Филиппа Уодлера "How to Replace Failure by a List of Successes (A method for exception handling, backtracking, and pattern matching in lazy functional languages)".
Но можно пойти и другим путем - можно каждому парсеру в качестве дополнительного аргумента передавать парсер, который будет вызван на следующем шаге сопоставления. Такой подход по духу очень близок стилю программированию в продолжениях (Continuation passing style). Действительно, в нашей первой наивной реализации парсер (or (a) (concat a b)) действовал по принципу "После нас хоть потоп" - возвращал всегда первое сопоставление - его не интересовало, пригоден ли его ответ для обработки следующим парсером в цепочке.
Легко кодируются в таком стиле парсеры для выражений a и b.
a = \next word -> case word of {
Nil -> None;
Cons sym word1 -> case sym of {
A -> next word1;
B -> None;
};
};
b = \next word -> case word of {
Nil -> None;
Cons sym word1 -> case sym of {
A -> None;
B -> next word1;
};
};
Дополнительный аргумент next - это следующий парсер. Логика парсера a проста - если слово начинается с A, то на остаток слова натравливается парсер next, в противном случае -- неудача.
Комбинатор or записывается так:
or = \p1 p2 next word -> case p1 next word of {
Some word1 -> Some word1;
None -> p2 next word;
};
А комбинатор concat записывается очень изящно:
concat = \p1 p2 next word -> p1 (p2 next) word;
Композиция парсеров представляется в виде композиции функций!
Неожиданно возникает вопрос а как применить парсер к слову? Ведь теперь любой парсер требует своего продолжения! Для этого потребуется специальный парсер return, который разрывает порочный круг из бесконечных продолжений:
return = \w -> Some w;
В итоге для сопоставления выражения (a|ab)(bb|a) со словом ABA получается следующая программа:
data Symbol = A | B;
data List a = Nil | Cons a (List a);
data Option a = Some a | None;
par1 (Cons A (Cons B (Cons A Nil)))
where
par1 = concat (or a (concat a b)) (or (concat b b) a) return;
return = \w -> Some w;
or = \p1 p2 next word -> case p1 next word of {
Some word1 -> Some word1;
None -> p2 next word;
};
concat = \p1 p2 next word -> p1 (p2 next) word;
a = \next word -> case word of {
Nil -> None;
Cons sym word1 -> case sym of {
A -> next word1;
B -> None;
};
};
b = \next word -> case word of {
Nil -> None;
Cons sym word1 -> case sym of {
A -> None;
B -> next word1;
};
};
Вычисляем это выражение с помощью суперкомпилятора и получаем (Some Nil)! Если посмотреть на трассировку вычислений, то видно, что новый парсер по очереди перебирает все варианты, пока не найдет успешный, - грубо говоря, неявным образом составляются все возможные комбинации парсеров и по очереди применяются ко входному слову. Первая комбинация завершиласть неудачно - пробуется вторая и т.д. Можно еще сказать, что новый комбинатор or как бы выносит разбор вариантов из глубины регулярного выражения наружу. То есть в каком то смысле переписывает регулярное выражение (re1|re2)re3 -> ((re1 re2) | (re1 re3)).
Вычисление par1 (Cons A (Cons B (Cons B Nil))) тоже выдает (Some Nil).
Платой за красоту такой записи регулярных выражений с помощью комбинаторов являются накладные расходы интерпретатора во время вычислений. Ведь выражение (a|ab)(bb|a) неявно трансформируется так:
(a|ab)(bb|a) -> (a(bb|a))| (ab(bb|a)) -> abb|aa|abbb|aba
И наш парсер по очереди перебирает эти 4 варианта -- то есть в худшем случае он 4 раза перемещается по входному слову туда-сюда. При более сложных выражениях парсер может бегать по входному слову туда-сюда очень много раз. Это особенно проявляется в случаях, когда входное слово не соответствует регулярному выражению, - прежде чем выдать неудачу парсер попробует все варианты.
Существует отдельная область математики, изучающая только регулярные выражения. Доказано, что любое (классическое) регулярное выражение можно превратить в детерминированный конечный автомат, который кушает по одному символа входного слова и выдает результат (успех или неудачу) за минимальное число шагов (поеданий очередного символа). Кодировать же регулярные выражения в виде автоматов для программиста задача неблагодарная и ведущая к потенциальным ошибкам. Поэтому многие языки (и библиотеки) поддерживают регулярные выражения удобным для программистов способом - а внутри они преобразуют красивую и изящную запись регулярного выражения в потенциально большой, но быстрый конечный автомат.
А попробуем сопоставить наше игрушечное регулярное выражение с произвольным словом w, то есть вычислить concat (or a (concat a b)) (or (concat b b) a) return w с помощью суперкомпилятора HOSC. Результат такой:
А попробуем сопоставить наше игрушечное регулярное выражение с произвольным словом w, то есть вычислить concat (or a (concat a b)) (or (concat b b) a) return w с помощью суперкомпилятора HOSC. Результат такой:
case w of {
Nil -> None;
Cons p40 v20 ->
case p40 of {
A ->
case v20 of {
Nil -> None;
Cons v1 u30 ->
case v1 of {
A -> (Some u30);
B ->
case u30 of {
Nil -> None;
Cons y18 p22 -> case y18 of {
A -> (Some p22);
B -> (Some p22);
};
};
Nil -> None;
Cons y18 p22 -> case y18 of {
A -> (Some p22);
B -> (Some p22);
};
};
};
};
B -> None;
};
}
Видно, что отсуперкомпилированный парсер не бегает по слову туда-сюда, а продвигается по слову только вперед.
Заключение
Было показано, как с использованием комбинаторного подхода реализуется проблемно-ориентированный язык для работы с подмножеством регулярных выражений. Реализовать этот язык у нас получилось только со второго раза, что является подтверждением того, что хотя работать с комбинаторным DSL легко и приятно, реализовать даже простой DSL не так то уж и тривиально. Оказалось, что суперкомпилятор HOSC способен устранять накладные расходы, вызванные использованием изящного, но требовательного к ресурсам DSL, реализованный через комбинаторы.
Мы реализовали комбинаторный DSL только для подмножества языка регулярных выражений. В следующий раз мы расширим наш маленький DSL до полной поддержки классических регулярных выражений и посмотрим какие проблемы при этом могут возникнуть.
воскресенье, 14 февраля 2010 г.
Недетерминизм: выбор по надобности или выбор при вызове?
В послании
было показано, что недетерминированные программы можно писать в рамках детерминированного ленивого функционального языка, реализовав с помощью комбинаторов проблемно-ориентированный язык, содержащий конструкцию "произвольного выбора". Идея-то с виду простая: реализуем конструкцию choice2 e1 e2. И пусть вычисление этой конструкции сводиться к вычислению e1 или e2, а выбор между e1 и e2 делается произвольно.
Или, говоря более формально, считаем, что семантика языка определяется через правила редукции выражений (т.е. сведения одних выражений к другим), просто считаем, что для choice2 определено два правила редукции:
choice2 e1 e2 --> e1
choide2 e1 e2 --> e2
Вроде бы, всё ясно и понятно... Однако, есть тут один "подводный камень". Рассмотрим такое недетерминированное выражение:
(\x -> P x x) (choice2 True False)
где P - конструктор, формирующий пару. Каковы возможные результаты вычисления этого выражения? Это зависит от того, в каком порядке выполнять редукцию. Если первый шаг редукции - применение функции (\x -> P x x) к аргументу (choice2 True False), то на первом шаге получается выражение
P (choice2 True False) (choice2 True False)
в результате дальнейшей редукции которого могут получиться 4 разных выражения: P True True, P True False, P False True, P False False.
А если первый шаге редукции - упрощение (choice2 True False), то получается одно из двух выражений
(\x -> P x x) True
(\x -> P x x) False
и дальнейшие вычисления дают только два возможных результата: P True True, P False False.
Когда выбирать: когда нужен результат или при передаче параметра?
Из рассмотренного примера видно, что результат вычисления недетерминированных конструкций может зависеть от порядка вычислений и от моментов, в которые производится выбор между возможностями. Можно затягивать выбор до последней возможности: выбирать только тогда, когда результат, возвращаемый конструкцией выбора реально понадобился. В литературе этот вариант называется "выбором по надобности" (need-time choice). А можно выбирать в тот момент, когда конструкция выбора оказывается аргументом функции. В литературе этот вариант называется "выбором при вызове" (call-time choice).
В послании
была рассмотрена реализация "выбора по надобности". При исполнении вызова функции, конструкция choice2, оказавшаяся в аргументе функции, прямо подставлялась в тело функции, а выбор из двух вариантов откладывался до момента "надобности".
Это наглядно можно увидеть просуперкомпилировав выражение
(app (lam (\x -> pairP (var x) (var x))) (choice2 (cst True) (cst False))) c
Получается остаточная программа
case c of {
D u z3 ->
case z3 of {
D u5 y5 -> (P case u5 of { L t4 -> True; R p4 -> False; }
case y5 of { L y8 -> True; R p2 -> False; });
};}
из которой видно, что каждый из компонентов пары может принимать значение независимо от другого.
Однако, существует мнение, что такой подход - не очень хорош с "идеологической" точки зрения. Вот смотрим мы на определение функции (\x -> P x x) функции, и наивно думаем, что при вызове функции переменная x должна "принять некоторое значение", и что это значение - "одно и то же" для всех вхождений x. А оказывается, что это - не так. Чувствуется в этом какая-то гниль (по мнению некоторых авторитетных товарищей). Не лучше ли делать все выборы до того, как с переменной связывается значение? Тогда в P x x оба входения x будут означать одно и то же.
Если уж "выбор при вызове", то тогда уж и "вызов по значению"
Но тут сразу же выясняется, что если мы хотим, чтобы выбор происходил до передачи аргумента в тело функции, то это означает, что аргумент функции должен вычисляться до передачи аргумента в тело функции. Другими словами, параметры должны передаваться в тело функции не "по имени" (call by name), а "по значению" (call by value).
(Конечно, ещё возможны и изощрённые варианты, когда параметр может передаваться всяко: либо по имени, если он детерминированный, либо по значению, если он недетерминированный, но в такие жуткие дебри мы углубляться не будем.)
А теперь предположим, что нам хочется реализовать недетерминированный язык через набор комбинаторов, и при этом комбинаторы нужно писать на "ленивом" языке. Можно ли при этом реализовать "выбор при вызове"? Ведь для этого надо, чтобы параметры передавались "по значению", а в "ленивом" языке параметры передаются "по имени". Оказывается, что можно...
Реализация вызова по значению в ленивом языке через "продолжения"
Вызов параметров по значению можно реализовать в рамках "ленивого" язык, если использовать писать программу "в стиле передачи продолжений" (continuation passing style). А именно, к параметрам каждой функции f нужно добавить дополнительный параметр k (который называется "продолжением"). Если вызов функции f выглядел как f x1 x2 ... xN, то теперь он принимает вид f x1 x2 ... xN k. При этом, в тех местах, где функция возвращала результат a, нужно выдачу результата делать не напрямую, а вызывать k, передав ему результат в качестве аргумента: k a.
В послании
рассматривалась реализация "ленивого" лямбда-исчисления через набор комбинаторов (см. задание на суперкомпиляцию Lambda: higher-order syntax (transparent)):
var = \x -> x;
lam = \f -> f;
app = \e1 e2 -> e1 e2;
cst = \a -> a;
fix = \f -> f (fix f);
Эти комбинаторы настолько тривиальны, что трудно даже понять их смысл! Тавтология - она тавтология и есть. Если мы реализуем ленивый язык с вызовом параметров по имени через ленивый же язык с вызовом параметров по имени, то понятия реализуемого языка тривиально отображаются на язык реализации.
А теперь попробуем сделать так, чтобы аргумент функции сначала вычислялся и только после этого связывался с параметром функции, переписав комбинаторы в стиле с продолжениями (см. задание на суперкомпиляцию Lambda: HOAS, CPS, CBV)!
var = \x k -> k x;
lam = \f k -> k f;
app = \e1 e2 k -> e1 (\f -> e2 (\v -> f v k));
cst = \a k -> k a;
var, lam и cst устроены неинтересно: переменная подсовывает продолжению k своё значение, lam - функцию, а cst - свой аргумент. Весь интерес - в комбинаторе app! Он работает так. Сначала вычисляется e1, и результат этого вычисления подсовывается продолжению (и связывается с переменной f). Затем вычисляется e2, и результат этого вычисления подсовывается продолжению (и связывается с переменной v). После этого вычисляется результат применения f к v и подсовывается продолжению k. Вот и получается, что при вызове функции предварительно вычисляется ей аргумент. В рамках "ленивого" языка реализован вызов параметра по значению.
Самый тонкий вопрос - как определить fix! Определение fix - это некая смесь из определений app и lam:
fix = \e k -> k (fixLoop e);
fixLoop = \e x k -> e(fixLoop e)(\f -> f x k);
run - вспомогательная функция, с помощью которой исполняется выражение, записанное с помощью комбинаторов. Дело сводится к тому, что нужно подсунуть выражению тривиальное "продолжение", которое ничего не делает, а просто возвращает результат, вырабатываемый выражением:
run = \e -> e (\x -> x);
Для того, чтобы можно было определять функции, что-то делающие с натуральными числами, определим ещё три комбинатора. natZ - вырабатывает ноль, natS сначала вычисляет свой аргумент, а потом прибавляет к тому, что получилось, единицу. natCase реализует разбор случаев: проверяет, является ли нулём её первый аргумент, а затем вызывает второй или третий аргумент.
data Nat = Z | S Nat;
natZ = \k -> k Z;
natS = \e k -> e (\v -> k(S v));
natCase = \e eZ eS k -> e (\v -> case v of {
Z -> eZ k;
S n -> eS n k;
});
Теперь можно определять функции над натуральными числами
data Bool = True | False;
natIsZ = \e -> natCase e (cst True) (\n -> (cst False));
natPred = \e k -> e (\v -> case v of { S v1 -> k v1;});
А с помощью fix - и рекурсивные функции. Например, "тождественную" функцию, разбирающую на части натуральное число и собирающую его обратно, можно определить так:
run (fix(\natId -> lam(\x ->
natCase (var x)
natZ
(\x1 -> (natS (app (var natId) (var x1)))))))
Просуперкомпилировав это выражение, получаем остаточную программу
\x k->
letrec f = \x0 k0 -> case x0 of {
Z -> k0 Z;
S x1 -> f x1 (\x2 -> k0 (S x2)); }
in f x k
На первый взгляд, выглядит она загадочно, но если запрограммировать тождественную функцию в стиле с продолжениями вручную, то ровно это и получается.
Реализация "выбора при вызове" через комбинаторы
Теперь мы готовы "совершить фигуру высшего пилотажа": реализовать недетерминированный язык с передачей параметров по значению и выбором при вызове в рамках ленивого языка! Для этого мы смешаем вместе два ингредиента: заставим программу потреблять дополнительный параметр, содержащий последовательность выборов, как это было сделано в послании
но используем в комбинаторах, реализующих недетерминированный язык стиль с продолжениями. Результат можно увидеть заглянув в задание на суперкомпиляцию Lambda: non-determinism (HOAS, CPS k c, CBV).
Посмотрим, что получается. Сначала определяются типы данных, которые используются в дальнейшем:
data Bool = True | False;
data Choice = L Choice | R Choice;
data Nat = Z | S Nat;
data Pair a b = P a b;
Здесь интересно то, что при реализации выбора по надобности в определении Choice нам понадобились три конструтора: L (левый выбор), R (правый выбор) и D (разделение последовательности выборов на две подпоследовательности). А теперь в определении Choice - только два конструктора: L и R. Это связано с тем, что при реализации языка с передачей параметров по значению и выбором при вызове получается, что последовательность, в которой выполняются вычисления, проста и заранее предсказуема. Поэтому нет и надобности "разветвлять" последовательность выборов: можно аккуратно "протаскивать" одну последовательность через весь процесс вычислений.
Основная идея проста. Пусть у нас есть выражение e. При вычислении этого выражения ему должно подсовываться два дополнительных аргумента: продолжение k и последовательность выборов c. Другими словами, хотим получить значение e - вычисляем e k c. При этом, в отличие от случая детерминированных программ, продолжение k должно принимать не только результат, вырабатываемый выражением e, но ещё и некоторую последовательность выборов c1. Т.е., k должно иметь вид (\v1 c1 -> e1). Откуда же берётся c1? Дело в том, что если выражение e содержит конструкции choice2, то эти конструкции могут потреблять выборы из входной последовательности выборов c. И продолжение должно получить оставшуюся "неизрасходованную" часть последовательности выборов через параметр c1.
Для исполнения недетерминированных программ, определим функцию run, возвращающую результат вычисления выражения e для заданной последовательности выборов c:
run = \e с -> e (\v c1 -> v) с;
Эта функция подсовывает выражению e продолжение \v c1 -> v и последовательность выборов c. Продолжение принимает результат, возвращаемый выражением e и выдаёт этот результат. А остаток последовательности выборов просто игнорирует. Ведь исполнение программы завершено, и этот остаток больше ни для чего не нужен.
Теперь определим комбинатор cst предназначенный для вставления констант в программу:
cst = \a k с -> k a с;
cst просто передаёт продолжению k константу a и неизменённую последовательность выборов (при вычислении константы выбирать ничего не приходится). Определение cst можно немного упростить используя "eta-редукцию". Зачем принимать и передавать c продолжению k в явном виде? Просто выдаём k a, т.е. функцию. И пусть уж она сама и забирает c! Те же соображения применимы и к функции run. Упростив run и cst получаем:
run = \e -> e (\v c -> v);
cst = \a k -> k a;
Теперь можно попробовать просуперкомпилировать первое выражение
run (cst True) --> (\c -> True)
Результат получается вполне разумный: для любой последовательности выборов всегда выдаётся True.
Теперь "возьмём быка за рога" и определим самую интересную конструкцию - choice2 (ради реализации которой всё и затевалось):
choice2 = \e1 e2 k c ->
case c of {
L c1 -> e1 k c1;
R c2 -> e2 k c2;};
choice2 должен решить, какое выражение вычислять: e1 или e2? Для этого и используется c. Если c начинается с L, то выбираем e1, а если с R - то выбираем e2. После чего передаём остаток последовательности выборов либо в e1, либо в e2.
Теперь пробуем просуперкомпилировать некоторые выражения:run (choice2 (cst True) (cst False)) -->
\c -> case c of { L c1 -> True; R c2 -> False; }
run (choice2 (cst Z) (choice2 (cst (S Z)) (cst (S(S Z))))) -->
\c -> case c of {
L c1 -> Z;
R c2 -> case c2 of { L c21 -> S Z; R c22 -> S (S Z); }; }
Теперь определим самые главные комбинаторы - var, lam и app:
var = \x k -> k x;
lam = \f k -> k f;
app = \e1 e2 k -> e1 (\f -> e2 (\v -> f v k));
Выглядит загадочно, но если не применять eta-редукцию и выписать определения в неоптимизированном виде, то получается
var = \x k c -> k x c;
lam = \f k c -> k f c;
app = \e1 e2 k c -> e1 (\f c1 -> e2 (\v c2 -> f v k c2) c1) c;
Поскольку в реализуемом языке параметры передаются по значению, то с переменными связываются уже "полностью готовые" результаты, а не выражения, которые ещё нужно вычислять (как в случае передачи по имени). Т.е., в значениях переменных уже всё вычислено и никакого недетерминизма уже нет! Поэтому при вычислении var x k c значение переменной x в неизменном виде передаётся продолжению k. Последовательность выборов c тоже передаётся в k без изменения. То же самое происходит и при вычислении lam f k c. f - это готовая функция, с которой ничего делать не надо.
А вот вычисление app e1 e2 k c - это уже более интересный случай. Сначала вычисляется e1. Ему подсовывается продолжение и последовательность выборов c. Продолжение получает результат f и остаток последовательности выборов c1. Затем c1 подсовывается под e2, и продолжение получает результат v и остаток последовательности выборов c2. После этого имеется известная функция f, известный аргумент v и остаток последовательности выборов c2. Вычисляем f v k c2.
Тонким местом является то, что f - это не просто функция от одного аргумента v, а функция, которая принимает ещё два дополнительных аргумента: продолжение k и последовательность выборов c2!
Теперь, чтобы проверить, что мы не запутались, просуперкомпилируем некоторые выражения:
lam (\x -> var x) -->
\k-> k (\x k1-> k1 x)
run (app (lam (\x -> (var x))) (cst True)) -->
(\c -> True)
Теперь наступил момент, когда мы можем вернуться к вопросу о том, какой результат должен получаться в результате вычисления выражения (\x -> P x x) (choice2 True False). Для этого определим комбинатор pairP, формирующий пару из своих двух аргументов:
pairP = \e1 e2 k ->
e1 (\v1 -> e2 (\v2 -> k (P v1 v2)));
Здесь просто выписано то, что при вычислении pairP e1 e2 нужно сначала вычислить e1, получив v1, затем - e2, получив v2, а затем - выдать P v1 v2. Ну, естественно, при этом должны надлежащим образом выполняться манипуляции с продолжениями и с последовательностью выборов.
Теперь суперкомпилируем
run (app (lam (\x -> pairP (var x) (var x)))
(choice2 (cst True) (cst False))) -->
\c -> case c of { L c1 -> P True True; R c2 -> P False False; }
и видим, что, как мы и хотели, возможными результатами вычисления этого выражения могут быть только P True True и P False False. За что боролись, то и получили.
Теперь, для интереса, напишем недетерминированную программу, генерирующую "произвольное натуральное число". Для этого определим комбинаторы, работающие с натуральными числами:
natZ = \k -> k Z;
natS = \e k -> e (\v -> k (S v));
natCase = \e eZ eS k -> e (\v -> case v of {
Z -> eZ k;
S n -> eS n k;
});
natZ возвращает ноль Z, а natS e вычисляет e, получает значение v и выдаёт S v. Теперь мы умеем генерировать натуральные числа!
Но есть одна тонкость: конструкция choice2 умеет делать выбор только из двух вариантов, а при генерации "произвольного" числа нужно делать выбор из счётного множества вариантов. Понятно, что без рекурсии нам не обойтись. Поэтому определим ещё и конструкцию fix, вычисляющую "неподвижную точку":
fix = \e k -> k (fixLoop e);
fixLoop = \e x k -> e(fixLoop e)(\f c1 -> f x k c1);
При первом взгляде на такое определение у всякого нормального человека начинается "расплавление мозгов". Но если не отступаться, то через некоторое время наступает "просветление", и смысл этого определения становится понятен. Поэтому я не буду пытаться растолковать это определение с помощью человеческих слов... Кому суждено понять - тот поймёт сам. А кому не суждено - тому будет непонятно и словесное объяснение.
А теперь, имея в руках возможность определять рекурсивные функции, запишем выражение, выдающее "произвольное" натуральное число. Это можно сделать разными способами, но, раз уж мы реализовали "строгий" язык с передачей параметров по значению (ну, прямо почти C++ :-) ), то и решим задачу в "императивном" стиле.
Заведём переменную и присвоим ей 0. А дальше будем крутить цикл и на каждом шаге решать: остановиться или продолжать. Если останавливаемся, то выдаём значение переменной в качестве результата. Если решаем не останавливаться, то прибавляем к переменной 1 и крутим цикл дальше.
В функциональных понятиях это можно переформулировать так. Определим функцию
f x = choice2 x (f (S x));
и вычислим выражение
f Z
Теперь расписываем всё это в виде имеющихся у нас комбинаторов. Определение функции f принимает вид
fix (\f -> lam (\x -> choice2 (var x) (app (var f)(natS (var x)))))
и теперь нужно применить эту функцию к аргументу Z и запустить получившееся выражение с помощью функции run. Для большей удобочитаемости результата, передадим функции run ещё и последовательность выборов c. Получается такое выражение:
run (app (fix (\f -> lam (\x -> choice2 (var x) (app (var f)(natS (var x)))))) natZ) c
Суперкомпилируем его и получаем:
letrec g = \v c1 -> case c1 of {
L c11 -> v;
R c12 -> g (S v) c12; }
in g Z c
Ну что же, суперкомпилятор Хоск показал себя молодцом! В остаточной программе от комбинаторов ничего не осталось...
пятница, 29 января 2010 г.
Превращение неявной рекурсии в явную с помощью суперкомпиляции
В послании
обсуждалась возможность записывать явные рекурсивные определения данных. А нельзя ли вообще без них обойтись?
Как известно, в "чистом, классическом" лямбда-исчислении нет ничего, кроме лямбда-термов и явные рекурсивные определения писать нельзя. Тем не менее, с помощью некоторых трюков (вроде "оператора неподвижной точки") рекурсивные определения всё же удаётся записать.
Возникает два интересных вопроса:
- Можно ли пользоваться во входном языке суперкомпилятора Хоск (HOSC) теми приёмами, которые были придуманы для "чистого, классического" лямбда-исчисления?
- Можно ли использовать суперкомпиляцию для преобразования неявной рекурсии (закодированной с помощью "оператора неподвижной точки") в явную рекурсию?
Начнём с первой проблемы.
HLL - язык со статической типизацией (по Хиндли-Милнеру). А насколько суровы ограничения, накладываемые такой типизацией? Что они не разрешают делать?
Рассмотрим выражение
\x -> x x
знакомое всем, кто интересовался теорией бестипового лямбда-исчисления. Для этого знаменитого выражения даже существует традиционное обозначение: буква омега. Итак, пусть
omega = \x -> x x
Чем же это выражение интересно? Да тем, что с его помощью конструируется "самовоспроизводящееся" выражение. А именно,
omega omega --> (\x -> x x) omega --> omega omega
А можно ли написать в HLL-программе \x -> x x ? Нельзя! Не разрешает типизация по Хиндли-Милнеру применять функцию саму к себе. Действительно, какой тип должна иметь переменная x? Раз написано x x, значит, x применяется к аргументу x. Стало быть, тип переменной x должен иметь вид a -> b, где a - тип аргумента. Но аргументом является x. Стало быть, получается, что a = a -> b. Попробуем решить это уравнение. Получается
a = a -> b = (a -> b) -> b = ((a -> b) -> b) -> b = ...
т.е. тип переменной x - бесконечное тИповое выражение. Но по правилам игры, установленным Хиндли и Милнером все типы должны изображаться конечными выражениями, т.е. считается, что уравнение a = a -> b решений не имеет. Стало быть, omega не является типизируемым!
Однако, как известно (в некоторых случаях) строгость законов уравновешивается необязательностью их исполнения. Ну, или тем, что в законах оставлены лазейки, позволяющие их нарушать, формально как бы и не нарушая. А именно, оказывается, что лазейку предоставляют типы данных, определяемые в программе.
Уравнение a = a -> a решений не имеет, но зато, как показывает пример
не запрещено определять типы данных вроде:
data D = F (D -> D);
Добавили конструктор F - и вот уже D "почти" равно D -> D (с точностью до надевания конструктора F). Было нельзя - и вдруг стало можно! Но, конечно, прямо так напрямую написать x x - нельзя. Если объявить, что типом переменной x является D - то получится, что x - не функция, а функция, на которую надет конструктор F, ибо D = F (D -> D). Но это - не страшно, конструктор ведь можно и снять. И для этого можно определить функцию apply:
apply = \x y -> case x of { F f -> f y; };
Идея функции проста: при вычислении apply e1 e2, e1 должно выдать результат вида F f, где f - функция. Снимаем тег F и вычисляем f e2. Причём, если присмотреться к определению функции apply, видно, что это определение можно ещё немного упростить: оставить только снятие тега F, чтобы выражение apply e1 выдавало функцию, которую уже можно к чему-то применить. Тогда получается такое определение:
apply = \x -> case x of { F f -> f; };
Теперь всё это собираем в одно задание на суперкомпиляцию
data D = F (D -> D);
apply omega omega
where
omega = F (\x -> apply x x);
apply = \x -> case x of { F f -> f; };
и получаем такую приятную остаточную программу
data D = F (D->D); (letrec f=f in f)
из которой видно, что суперкомпилятор правильно распознал, что при вычислении apply omega omega какого-либо результата сколько ни жди - не дождёшься...
Теперь, чтобы окончательно убедиться в том, что "невозможное - возможно", изобразим средствами HLL что-нибудь нетривиальное из нетипизированного лямбда-исчисления. А именно, определим "оператор неподвижной точки" fix не используя явную рекурсию. Классическое рекурсивное определение функции fix выглядит так:
fix = \f -> f (fix f);
Но, как учат нас учебники по лямбда-исчислению, без рекурсии можно обойтись, определив fix, например, так:
fix = \f -> (\x -> f (x x))(\x -> f (x x))
Приглядевшись, в этом выражении можно узнать слегка "усовершенствованное" выражение omega omega. Но в HLL прямо так определить fix нельзя: нужно использовать тот же трюк, который мы применяли к omega omega. Что и сделано в примере
Получается такая программа
data D = F (D -> D);
fix
where
apply = \x -> case x of { F f -> f; };
fix = \f -> apply (F (\x -> f (apply x x)))(F (\x -> f (apply x x)));
Просуперкомпилировав её, получаем
data D = F (D->D); \f -> (letrec g = f g in g)
Легко видеть, что \f -> (letrec g = f g in g) - это то же самое, что
fix = \f -> f (fix f);
хотя и записано немного по другому. Разница в том, что fix вынужден таскать с собой аргумент f в процессе вычисления, а если использовать letreс, то f может быть свободной переменной по отношению к letrec. Т.е. получается, что g - вроде как бы даже и не "функция", а "структура данных" (раз у неё нет аргумента). Молодец, Хоск! Нетривиальное преобразование сумел выполнить.
Однако, нужно заметить, что fix мы закодировали без использования рекурсии только, так сказать, из "спортивного интереса", чтобы посмотреть, испугается ли такого задания Хоск или нет. Не испугался! А на самом деле, Хиндли-Милнер как это ни странно, разрешает нам определить fix прямо через рекурсию следующим образом:
fix = \f -> f (fix f);
Несмотря на то, что fix f подсовывается под f в качестве аргумента! Как же так? Разве можно функцию f подсовывать самой себе (не используя теги)? Оказывается, что можно. Какой тип должен иметь fix? Это можно выяснить с помощью таких рассуждений. Исходим из того, что fix f = f (fix f). Из выражения f (fix f) следует, что f - функция. Стало быть, её тип должен иметь вид a -> b, где a - это тип выражения fix f. Но и fix - функция, аргумент которой имеет тип a -> b. Значит, у fix тип должен быть (a -> b) -> c. А поскольку fix f в f(fix f) является аргументом f, получается, что c = a.
Итак, у f тип a -> b, у fix тип (a -> b) -> a, у fix f тип a, у f(fix f) тип b. Вспоминаем, что fix f = f(fix f), и типы у них должны совпадать. Стало быть, a = b. Итак, у fix тип (a -> a) -> a и все концы благополучно сошлись с концами!
Поэтому, чтобы не возиться с тегами, определим fix как
fix = \f -> f (fix f);
и попробуем выполнить "фигуру высшего пилотажа": закодировать взаимную рекурсию двух определений без использования явной рекурсии через функцию fix. Как же это сделать, если у fix аргумент только один, а нам нужно с его помощью закодировать два определения? А это можно сделать, подсунув под fix функцию, аргументом которой является пара, а результатом - тоже пара. Так и сделано в примере
В этом примере пара рекурсивных определений
p = A q;
q = B p;
записана без помощи явной рекурсии. Идея заключается в том, что два уравнения можно объединить в одно, используя конструктор пар P:
P p q = P (A q) (B p);
Однако, прямо так написать нельзя, поскольку в HLL в левой части определения должна стоять переменная. Но это - не беда. Перепишем определения в виде
r = P (A q) (B p);
p = fst r;
q = snd r;
где fst и snd - функции, выбирающие первый и второй элемент пары соответственно. Теперь, подставляя вместо p и q их определения, получаем
r = P (A (snd r))(B (fst r));
p = fst r;
Ну, а это уже легко выражается через fix. В результате, задание на суперкомпиляцию выглядит так:
data Input = A Input | B Input;
data Pair a b = P a b;
fst(fix (\r -> P (A (snd r)) (B (fst r))))
where
fst = \u -> case u of { P x y -> x; };
snd = \u -> case u of { P x y -> y; };
fix = \f -> f(fix f);
А в результате суперкомпиляции получается следующая остаточная программа:
data Input = A Input | B Input; data Pair a b = P a b; letrec f=(A (B f)) in f
Таким образом, мы видим, что Хоск в очередной раз справился с преобразованием неявной рекурсии (через редукцию) в явное рекурсивное определение (удалив при этом много промежуточных шагов редукции).
четверг, 28 января 2010 г.
Тёмные углы суперкомпилятора HOSC: неполные case-выражения и рекурсивные определения данных
Некоторое время назад в HLL, входной язык суперкомпилятора Хоск (HOSC), были "тихой сапой" добавлены кое-какие маленькие, но приятные возможности. Вроде бы они не очень и нужны, но их отсутствие время от времени "напрягало" и заставляло использовать в исходных программах противоестественные трюки, загромождавшие исходные и остаточные программы.
Речь будет идти о двух вопросах:
- Неполные case-выражения (содержащие не все конструкторы из типа данных).
- Рекурсивные определения, в правой части которых не лямбда-абстракция, а что-то другое.
Неполные case-выражения
Раньше в хосковском HLL было такое ограничение. Если определение типа данных определяло некоторый набор конструкторов C1, C2, ..., Cn, то любое case-выражение, использующее один из этих конструкторов должно было предусматривать ветви для каждого из этих конструкторов:
case e0 of {C1 ... -> e1; C2 ... -> e2; ... Cn -> en; }
Идея была примерно такая: Хоск предполагается использовать для анализа программ, а программы дожны использоваться как средство формализации чего-то в виде исполняемых спецификаций. Однако, если сами спецификации будут содержать ошибки, то и результаты анализа будут бредовые. Поэтому язык, на котором пишутся программы, должен быть со статической типизацией. Тогда проверяльщик типов сможет обнаружить хотя бы часть ошибок. Ну, а чтобы проверяльщик обнаруживал побольше ошибок, так пусть он заодно проверяет, что ни один из конструкторов не забыт.
Мысль, в принципе, верная. Но только в случае, если мы собираемся работать только со всюду определёнными ("тотальными") функциями. Но очень часто функции, по самой своей сути, не определены для некоторых аргументов. Например, определим типы данных, соответствующие спискам и натуральным числам Пеано:
data List a = Nil | Cons a (List a);
data Nat = Z | S Nat;
А теперь попробуем определить функции tail (взятие "хвоста" списка) и pred (вычитание единицы из числа):
tail = \xs -> case xs { Nil -> error; Cons x xs1 -> xs1; };
pred = \n -> case n { Z -> error; S n1 -> n1; };
Если требовать, что для случаев Nil и Z должны присутствовать ветви, то надо как-то указать, что выбор этих ветвей является "ошибкой". Нужно было что-то написать для этих случаев в качестве результата работы функции. Ну, я и написал error. Пока не будем вдаваться в вопрос, что именно означает этот error, но плохо уже то, что в программе пришлось вообще что-то писать для случаев, которых "не должно быть".
Поэтому, теперь в HLL, входном языке Хоска, разрешается часть конструкторов в case-выражениях опускать. Т.е., функции tail и pred теперь можно определить так:
tail = \xs -> case xs { Cons x xs1 -> xs1; };
pred = \n -> case n { S n1 -> n1; };
Мелочь, конечно, но жизнь в некоторых случаях облегчает.
А что получается при попытке вычислить tail Nil или pred Z ? Получается "возникновение ошибки": выполнение программы в этом случае "аварийно завершается".
Выражение "часть конструкторов можно опустить" можно понимать и в том смысле, что можно опустить и вообще все конструкторы, т.е. писать case-выражения вида
case e0 of {}
которые исполняются так. Пробуем вычислить e0. Поскольку семантика языка HLL - "ленивая", в результате получается нечто, приведенное к "слабой головной нормальной форме". В данном случае это означает, что на верхний уровень вылезает некий конструктор C. (А лямбда-абстракция вида \x -> e получиться не может из-за ограничений статической типизации). После чего делается попытка выбрать в case-выражении ту ветвь, которая соответствует конструктору C. А такой ветви и нет (поскольку нет ни одной). И это приводит к аварийной остановке программы. Но это только в том случае, если попытка вычисления e0 была успешной. А если вычисление e0 завершилось аварийно, или вообще не остановилось, то до попытки выбора ветви дело не доходит. Впрочем, для гарантированной генерации ошибки, в качестве e0 всегда можно написать нечто всегда завершающееся, например Z, тогда вычисление case Z of {} заведомо аварийно завершается.
В качестве реального примера, когда применение неполных case-выражений позволяет уменьшить размер программы и делает программу более понятной, можно сравнить два варианта интерпретатора лямбда-выражений
В первом варианте, обрабатываемые данные представлены таким типом данных:
data Val = Error | N Nat | C VarName Exp Env;
При этом ошибки, связанные с несоответствием типов, явно представлены с помощью конструктора Error, и все случаи возможного несоответствия типов выписаны в явном виде. Например, при вычислении аппликации App e1 e2, результат вычисления e1 должен быть функцией (точнее, замыканием), но не числом и не ошибкой:
App e1 e2 ->
case eval e1 env of {
Error -> Error;
N n -> Error;
C v body env1 ->
eval body (Bind v (eval e2 env) env1);
};
А во втором варианте данные предствлены так:
data Val = N Nat | C VarName Exp Env;
Конструктор Error исчез, поскольку для обработки ошибок используется механизм, встроенный в HLL. Сократился и размер интерпретатора, поскольку неполные case-выражения позволяют не выписывать все "нехорошие" ситуации в явном виде. В частности, обработка App e1 e2 теперь принимает такой вид:
App e1 e2 ->
case eval e1 env of {
C v body env1 ->
eval body (Bind v (eval e2 env) env1);
};
В интерпретаторе остались только "интересные" части, а тривиальные - исчезли. Кстати, это благотворно отражается и на остаточных программах, поскольку и в них уменьшается количество рассматриваемых случаев. Например, суперкомпиляция выражения
run (Fix VZ (NatS (Var VZ)))
даёт для первой версии интерпретатора
letrec f=case f of { C r15 r13 x20 -> Error; Error -> Error; N y12 -> N (S y12); } in f
а для второй версииletrec f=case f of { N y13 -> N (S y13); } in f
Справедливости следует отметить, что суперкомпиляторы, имеющие дело с динамически типизированными языками, например SPSC и SPC4,
изначально умеют работать с неполными case-выражениями (представленными в других обличьях). Просто из-за того, что при отсутствии статической типизации и объявлений типов данных, непонятно, что могло бы обозначать такое понятие, как "полный список конструкторов"?
Рекурсивные определения данных
До недавнего времени в HLL, входном языке Хоска, рекурсивные определения можно было писать только для функций, но не для данных. Т.е., рекурсивные определения, записанные в программе после where, дожны были иметь такой вид
f = \x -> e;
Однако, как показывает следующий пример
с помощью рекурсивных функций можно было запросто генерировать бесконечные структуры данных. В результате суперкомпиляции следующей программы
data Xs = X Xs;
data Unit = U;
(f U)
where
-- a = X a;
f = \u -> X (f u);
получалась остаточная программа
data Xs = X Xs; data Unit = U ; letrec g=(X g) in g
Явная непоследовательность! Суперкомпилятор Хоск умеет заменять рекурсивные определения функций, генерирующие бесконечные структуры данных на явные уравнения, определяющие данные. И это - хорошо, ибо упрощает и проясняет структуру программы. Но почему же не разрешать писать такие определения прямо в исходной программе (в случаях, когда это удобно)?
Кстати, Хоск справляется и со случаями, когда функция определяется рекурсивно вызывая себя не напрямую, а через другие функции. Вот соответствующий пример
Суперкомпилируем программу
data Input = A Input | B Input;
data Unit = U;
p U
where
-- p = A q;
-- q = B p;
p = \u -> A (q u);
q = \u -> B (p u);
и получаем остаточную программу:
data Input = A Input | B Input; data Unit = U ; letrec f= A (B f) in f
Теперь видно, что p U генерирует бесконечный поток из A и B вида A (B (A (B ... ))).
Но, естественно, было бы лучше не использовать функции, а прямо написать в исходной программе
p = A q;
q = B p;
И Хоск теперь это разрешает. Что хорошо, поскольку бесконечные структуры данных хорошо подходят для моделирования систем, которые способны работать бесконечно долго (не выдавая никакого "окончательного" результата). Пример такой системы - Microsoft Windows. :-)
Справедливости ради следует сказать, что иногда использование рекурсивных данных для генерации бесконечных структур данных вполне уместно. В качестве (упрощенческого) примера такого рода рассмотрим забавный пример
В этом примере определяются две функции enqueue и repeat.
data List a = Nil | Cons a (List a);
data Bool = True | False;
repeat (Cons True (Cons False Nil))
where
repeat = \xs -> case xs of {
Nil -> Nil;
Cons x xs1 -> Cons x (repeat (enqueue x xs1));
};
enqueue = \a xs -> case xs of {
Nil -> Cons a Nil;
Cons x xs1 -> Cons x (enqueue a xs1);
};
enqueue a xs вставляет a в конец списка xs, а repeat xs строит бесконечный список в котором повторяются элементы списка xs. Например, repeat [A, B, C] порождает [A, B , C, A, B, C, ...]. При этом, repeat реализована таким "топорным" способом: она всё время "вращает" xs, т.е. берёт из xs первый элемент, выдаёт его и переставляет в конец списка xs (с помощью функции enqueue). В результате суперкомпиляции выражения
repeat (Cons True (Cons False Nil))
получается такое выражение:
Cons True (Cons False (letrec f=(Cons True (Cons False f)) in f))
Видно, что суперкомпилятор "прокрутил" список [True, False] один раз и сообразил, что можно построить цикл в графе конфигураций. А о том, что то же самое можно было бы записать в более краткой форме
letrec f=(Cons True (Cons False f)) in f
Хоск не догадался. "Мозгов" ему не хватило... Но и так результат неплохой.
Подписаться на:
Сообщения (Atom)