Сергей Романенко
28 января 2010 г.
Некоторое время назад в HLL, входной язык суперкомпилятора HOSC, были “тихой сапой” добавлены кое-какие маленькие, но приятные возможности. Вроде бы они не очень и нужны, но их отсутствие время от времени “напрягало” и заставляло использовать в исходных программах противоестественные трюки, загромождавшие исходные и остаточные программы.
Речь будет идти о двух вопросах:
Раньше в хосковском HLL было такое ограничение. Если определение типа
данных определяло некоторый набор конструкторов C_1 , C_2 , …, C_n,
то любое case-выражение, использующее один из этих конструкторов должно
было предусматривать ветви для каждого из этих конструкторов:
case e_0 of {C_1 ... -> e_1 ; C_2 ... -> e_2 ; ... C_n -> e_n ; }
Идея была примерно такая: HOSC предполагается использовать для анализа программ, а программы должны использоваться как средство формализации чего-то в виде исполняемых спецификаций. Однако, если сами спецификации будут содержать ошибки, то и результаты анализа будут бредовые. Поэтому язык, на котором пишутся программы, должен быть со статической типизацией. Тогда проверяльщик типов сможет обнаружить хотя бы часть ошибок. Ну, а чтобы проверяльщик обнаруживал побольше ошибок, так пусть он заодно проверяет, что ни один из конструкторов не забыт.
Мысль, в принципе, верная. Но только в случае, если мы собираемся работать только со всюду определёнными (“тотальными”) функциями. Но очень часто функции, по самой своей сути, не определены для некоторых аргументов. Например, определим типы данных, соответствующие спискам и натуральным числам Пеано:
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, входном языке HOSC-а, разрешается часть
конструкторов в case-выражениях опускать. Т.е., функции tail и pred
теперь можно определить так:
tail = \xs -> case xs { Cons x xs1 -> xs1; };
pred = \n -> case n { S n1 -> n1; };
Мелочь, конечно, но жизнь в некоторых случаях облегчает.
А что получается при попытке вычислить tail Nil или pred Z? Получается
“возникновение ошибки”: выполнение программы в этом случае “аварийно
завершается”.
Выражение “часть конструкторов можно опустить” можно понимать и в том смысле, что можно опустить и вообще все конструкторы, т.е. писать case-выражения вида
case e_0 of {}
которые исполняются так. Пробуем вычислить e_0. Поскольку семантика
языка HLL - “ленивая”, в результате получается нечто, приведенное к
“слабой головной нормальной форме”. В данном случае это означает, что на
верхний уровень вылезает некий конструктор C. (А λ-абстракция вида
\x -> e получиться не может из-за ограничений статической типизации).
После чего делается попытка выбрать в case-выражении ту ветвь, которая
соответствует конструктору C. А такой ветви и нет (поскольку нет ни
одной). И это приводит к аварийной остановке программы. Но это только в
том случае, если попытка вычисления e_0 была успешной. А если вычисление
e_0 завершилось аварийно, или вообще не остановилось, то до попытки
выбора ветви дело не доходит. Впрочем, для гарантированной генерации
ошибки, в качестве e_0 всегда можно написать нечто всегда завершающееся,
например 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 { Error -> Error;
N n -> N (S n);
C v body env -> Error; } in f
а для второй версии -
letrec f=case f of { N n -> N (S n); } in f
Справедливости следует отметить, что суперкомпиляторы, имеющие дело с динамически типизированными языками, например SPSC и SCP4, изначально умеют работать с неполными case-выражениями (представленными в других обличьях). Просто из-за того, что при отсутствии статической типизации и объявлений типов данных, непонятно, что могло бы обозначать такое понятие, как “полный список конструкторов”?
До недавнего времени в HLL, входном языке HOSC-а, рекурсивные определения
можно было писать только для функций, но не для данных. Т.е.,
рекурсивные определения, записанные в программе после 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
Явная непоследовательность! Суперкомпилятор HOSC умеет заменять рекурсивные определения функций, генерирующие бесконечные структуры данных на явные уравнения, определяющие данные. И это - хорошо, ибо упрощает и проясняет структуру программы. Но почему же не разрешать писать такие определения прямо в исходной программе (в случаях, когда это удобно)?
Кстати, HOSC справляется и со случаями, когда функция определяется рекурсивно вызывая себя не напрямую, а через другие функции. Вот соответствующий пример
Суперкомпилируем программу
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;
И HOSC теперь это разрешает. Что хорошо, поскольку бесконечные структуры данных удобны для моделирования систем, которые способны работать бесконечно долго (не выдавая никакого “окончательного” результата). Пример такой системы - 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
HOSC не догадался. “Мозгов” ему не хватило… Но и так результат неплохой.