Тёмные углы суперкомпилятора HOSC: неполные case-выражения и рекурсивные определения данных

Некоторое время назад в HLL, входной язык суперкомпилятора Хоск (HOSC), были "тихой сапой" добавлены кое-какие маленькие, но приятные возможности. Вроде бы они не очень и нужны, но их отсутствие время от времени "напрягало" и заставляло использовать в исходных программах противоестественные трюки, загромождавшие исходные и остаточные программы.

Речь будет идти о двух вопросах:

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

Неполные case-выражения

Раньше в хосковском HLL было такое ограничение. Если определение типа данных определяло некоторый набор конструкторов C₁, C₂, ..., C_n, то любое case-выражение, использующее один из этих конструкторов должно было предусматривать ветви для каждого из этих конструкторов:

case e₀ of {C₁ ... -> e₁; C₂ ... -> e₂; ... C_n -> e_n; }

Идея была примерно такая: Хоск предполагается использовать для анализа программ, а программы дожны использоваться как средство формализации чего-то в виде исполняемых спецификаций. Однако, если сами спецификации будут содержать ошибки, то и результаты анализа будут бредовые. Поэтому язык, на котором пишутся программы, должен быть со статической типизацией. Тогда проверяльщик типов сможет обнаружить хотя бы часть ошибок. Ну, а чтобы проверяльщик обнаруживал побольше ошибок, так пусть он заодно проверяет, что ни один из конструкторов не забыт.

Мысль, в принципе, верная. Но только в случае, если мы собираемся работать только со всюду определёнными ("тотальными") функциями. Но очень часто функции, по самой своей сути, не определены для некоторых аргументов. Например, определим типы данных, соответствующие спискам и натуральным числам Пеано:

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 e₀ of {}

которые исполняются так. Пробуем вычислить e₀. Поскольку семантика языка HLL - "ленивая", в результате получается нечто, приведенное к "слабой головной нормальной форме". В данном случае это означает, что на верхний уровень вылезает некий конструктор C. (А лямбда-абстракция вида \x -> e получиться не может из-за ограничений статической типизации). После чего делается попытка выбрать в case-выражении ту ветвь, которая соответствует конструктору C. А такой ветви и нет (поскольку нет ни одной). И это приводит к аварийной остановке программы. Но это только в том случае, если попытка вычисления e₀ была успешной. А если вычисление e₀ завершилось аварийно, или вообще не остановилось, то до попытки выбора ветви дело не доходит. Впрочем, для гарантированной генерации ошибки, в качестве e₀ всегда можно написать нечто всегда завершающееся, например Z, тогда вычисление case Z of {} заведомо аварийно завершается.

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

• Lambda: first-order syntax (FOCL)
  
• Lambda: first-order syntax (FOCL, without Error)

В первом варианте, обрабатываемые данные представлены таким типом данных:

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,

• A Small Positive Supercompiler in Scala
• SCP4 Documentation

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

Рекурсивные определения данных

До недавнего времени в HLL, входном языке Хоска, рекурсивные определения можно было писать только для функций, но не для данных. Т.е., рекурсивные определения, записанные в программе после where, дожны были иметь такой вид

f = \x -> e;

Однако, как показывает следующий пример

• a = X a

с помощью рекурсивных функций можно было запросто генерировать бесконечные структуры данных. В результате суперкомпиляции следующей программы

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

Явная непоследовательность! Суперкомпилятор Хоск умеет заменять рекурсивные определения функций, генерирующие бесконечные структуры данных на явные уравнения, определяющие данные. И это - хорошо, ибо упрощает и проясняет структуру программы. Но почему же не разрешать писать такие определения прямо в исходной программе (в случаях, когда это удобно)?

Кстати, Хоск справляется и со случаями, когда функция определяется рекурсивно вызывая себя не напрямую, а через другие функции. Вот соответствующий пример

• p = A q; q = B p;

Суперкомпилируем программу

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. :-)

Справедливости ради следует сказать, что иногда использование рекурсивных данных для генерации бесконечных структур данных вполне уместно. В качестве (упрощенческого) примера такого рода рассмотрим забавный пример

• repeat [True, False]

В этом примере определяются две функции 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

Хоск не догадался. "Мозгов" ему не хватило... Но и так результат неплохой.

Читать дальше...