scp-notes-ru

Проблемно-ориентированные языки с переменными и суперкомпиляция

Сергей Романенко

27 декабря 2009 г.

Этот блог - коллективный, и у него есть несколько авторов. Но писать - занятие трудоёмкое и утомительное, поэтому остальные соавторы благоразумно попрятались в кустах (в которых пока и пребывают) и периодически жалуются, что я что-то неправильно пишу. Пишу как умею… И надеюсь, что кто-нибудь меня, наконец, поправит и переизложит всё более правильно! :-)

Вот, например, это послание собирался настрочить Илья Ключников, но недавняя поездка в США (сопровождавшаяся посещением джаз-фестивалей и тому подобных мероприятий) окончательно подорвала его силы, остатков которых всё же хватило, чтобы докончить изготовление описания внутренностей суперкомпилятора HOSC:

Это - хорошо, поскольку в предыдущих посланиях утверждалось, что “HOSC может то, HOSC может сё”, но эти утверждения как-то повисали в воздухе, поскольку не было точно определено, что такое HOSC. Конечно, это можно было узнать, расковыряв исходные тексты, но, при отсутствии описания HOSC-а на более абстрактном уровне, это занятие напоминало бы выковыривание изюма из булочки…

Так что, так и быть, пускай Илья поотдыхает после препринта, а послание в блог я сам как-нибудь накатаю (хотя то, что в нём излагается, является плодом наших совместных раздумий). Или, скажем, так: все мысли, которые читателям этого послания понравятся, а припишу себе, а все неправильные и сомнительные идеи я припишу Илье!

Итак, в посланиях

обсуждалась следующая идея: суперкомпиляция может использоваться для реализации “проблемно-ориентированных” (ПО) языков программирования (которые по-английски любят назвать domain-specific languages или DSLs). Точнее говоря, ПО-язык завсегда можно реализовать в виде интерпретатора этого языка, но эффективность такой реализации оставляет желать лучшего. Но если применить суперкомпилятор к паре из интерпретатора и конкретной программы (предназначенной для этого интерпретатора), то интерпретатор и программа как бы сплавляются в одно целое, и в результате получается вполне эффективная остаточная программа.

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

Эта идея обсуждалась в послании

на примере функциональных парсеров.

Пример с парсерами вроде бы хорош! Но у некоторых проницательных читателей он вызвал справедливые подозрения. Уж как-то всё легко, красиво и гладко получается! Видимо, есть во всём этом какой-то подвох. А не сжульничал ли автор послания? Небось специально подобрал такой пример, для которого всё хорошо получается. А вдруг получается хорошо от того, что язык описания парсеров - слишком простой? Ведь всем ясно, что наиболее тонкие вопросы при реализации языков программирования обычно связаны с переменными (с их объявлениями и их использованиями). Переменные принимают значения, и эти значения нужно где-то хранить, создавать для этого “среду” (environment), таскать эту среду туда-сюда в интерпретаторе языка.

А в языке описания парсеров переменных не было, вот от этого он и получился таким простым и чистеньким (и в комбинаторы так легко разложился).

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

А вот что получится, если попытаться заменить интерпретатор первого порядка на набор комбинаторов? Получится ли это? А если получиться, то получится ли лучше? Забегая вперёд, сразу же скажу что, во-первых, получится, а, во-вторых, получиться лучше!

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

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

Чтобы написать интерпретатор, нужно решить, какой язык он должен интерпретировать. Выберем в качестве “подопытного кролика” такой язык, как бестиповое (а точнее - динамически типизированное) ламбда-исчисление). Язык λ-исчисления хорош тем, что он “мал - да удал”: конструкций в нём совсем не много, но на этих конструкциях проявляется весь букет проблем, возникающих из-за наличий переменных в программах.

“Чистое” λ-исчисление работает только с функциями, т.е. в нём данных первого порядка вообще нет. Но во всех практических языках программирования проводится различие между функциями и данными первого порядка. Поэтому, давайте рассмотрим слегка “загрязнённое” λ-исчисление, в котором есть не только функции, но ещё и натуральные числа (представленные в унарной системе счисления).

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

Первым делом выпишем определения данных, с которыми будут работать программы на языке λ-исчисления:

data Nat = Z | S Nat;

data Val = Error | N Nat | F (Val -> Val);

Натуральные числа 0, 1, 2, … будем представлять как Z, S Z, S (S (Z)), … А все значения, обрабатываемые и возвращаемые λ-выражениями будут делиться на три категории: ошибки (изображаемые конструктором Error), натуральные числа и функции из значений в значения. (А конструкторы, служащие для различения данных различных типов в народе принято называть “тегами”. В данном случае имеем три тега: Error, N и F.)

Как известно, в “чистом” лямда-исчислении любое выражение имеет один из следующих видов:

Но мы будем рассматривать расширенное λ-исчисление, умеющее работать с натуральными числами, поэтому добавим ещё две конструкции:

Ну, чтобы было интереснее, ещё добавим конструкцию

Конструкция fix позволяет записывать рекурсивные определения функций и бесконечных данных. Например, “бесконечное” натуральное число S (S (S (... ))) можно записать так: fix x -> S x.

Смысл конструкци fix можно объяснить через следующее эквивалентное преобразование:

(fix x -> e) = (\x -> e) (fix x -> e)

Например,

(fix x -> S x) ⟹ (\x -> S x)(fix x -> S x) ⟹ S (fix x -> S x)

Теперь нужно выписать тип данных, изображающий выражения на λ-языке в виде некоторых констант первого порядка.

Первым делом нужно решить, как изображать счетное множество переменных. Обычно в качестве имён переменных используются “идентификаторы” (строки из букв и цифр, начинающиеся с буквы). Но во входном языке суперкомпилятора HOSC строк (пока) нет. Поэтому мы поступим следующим образом: определим тип данных

data VarName = VZ | VS VarName;

и будем считать, что

VZ, VS VZ, VS (VS VZ), ...

изображают переменные

x0, x1, x2, ...

после чего мы можем определить “абстрактный синтаксис” (первого порядка) для языка λ-исчисления

data Exp =
  NatZ | NatS Exp |
  Var VarName | App Exp Exp | Lam VarName Exp |
  Fix VarName Exp;

Например, λ-термы

S Z
\x -> x x
fix x -> S x

представляются в виде констант

NatS NatZ
Lam VZ (App (Var VZ) (Var VZ))
Fix VZ (NatS (Var VZ))

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

Теперь, определившись с формой записи программ, переходим к написанию интерпретатора. Первым делом надо решить, каким способом мы собираемся хранить значения переменных? Допустим, у нас есть переменные x_1 , x_2 ,… , x_n имеющие значения v_1 , v_2 , …, v_n` соответственно. Классический подход - использовать “среду” (или “окружение”) вида

[(x_1 ,v_1 ), (x_2 ,v_2 ), ..., (x_n ,v_n )]

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

Чтобы сделать интерпретатор немного менее громоздким, мы не станем вводить отдельные понятия списка и пары, а прямо определим тип данных, предназначенный для представления сред:

data Env = Empty | Bind VarName Val Env;

Таким образом, среда [(x0, 0), (x1,1)], будет представлена следующим образом:

Bind VZ (N Z) (Bind (VS VZ) (N (S Z)) Empty

Теперь нам нужна функция lookup v env, которая для переменной v и среды env извлекает из env значение, соответствующее переменной v. Понятно, что для реализации этой функции нужно уметь сравнивать имена переменных на равенство, поэтому требуется ещё определить предикат varNameEq x y, проверяющий x и y на равенство. На входном языке HOSC-а эти функции можно определить так:

varNameEq = \x y ->
  case x of {
    VZ -> case y of {VZ -> True; VS y1 -> False;};
    VS x1 -> case y of {VZ -> False; VS y1 -> varNameEq x1 y1;};
  };

lookup = \v env ->
   case env of {
     Empty -> Error;
     Bind w val env1 ->
       case (varNameEq v w) of {
         True -> val;
         False -> lookup v env1;
     };
   };

Кстати, ещё не дописав интерпретатор, уже можно проделывать эксперименты по суперкомпиляции его отдельных частей. Например, просуперкомпилировав

lookup x (Bind VZ v1 (Bind (VS VZ) v2 Empty))

получаем такое забавное остаточное выражение:

case x of { VZ -> v1;
            VS s2 -> case s2 of { VZ -> v2;
                                  VS t1 -> Error; }; }

Если его внимательно изучить, то станет понятен тезис о том, что суперкомпиляцию можно использовать как средство “символического тестирования” программ…

А теперь, разделавшись с занудной частью работы, мы можем дописать интересную часть интерпретатора. Собственно говоря, интерпретатор - это функция eval e env, которая вычисляет значение выражения e при условии, что значения свободных переменных из e определены средой env.

eval = \e env ->
  case e of {
    NatZ -> N Z;
    NatS e1 -> evalNatS (eval e1 env);
    Var v -> lookup v env;
    Lam v body ->
      F (\x -> eval body (Bind v x env));
    App e1 e2 ->
      case eval e1 env of {
        Error -> Error;
        N n -> Error;
        F f -> f (eval e2 env);
      };
    Fix v body -> evalFix v body env;
  };

evalNatS = \x ->
  case x of {
    Error -> Error;
    N n -> N (S n);
    F f -> Error;
  };

evalFix = \v body env ->
  eval body (Bind v (evalFix v body env) env);

run = \e -> eval e Empty;

Функция run e вычисляет значение выражения e, при условии, что e не содержит свободных переменных, и определена для удобства запуска тестов.

Можно погонять и посуперкомпилировать этот интерпретатор “вживую”, используя заранее заготовленное задание Lambda: first-order syntax (FOCL) для суперкомпилятора HOSC.

Например,

run NatZ ⟹ (N Z)
run (NatS NatZ) ⟹ (N (S Z))
run (Lam VZ (App (Var VZ) (Var VZ))) ⟹
  (F (\t3-> case t3 of { Error -> Error;
                         N t4 -> Error; F s6 -> (s6 (F s6)); }))
run (App (Lam VZ (Var VZ)) NatZ) ⟹ (N Z)
run (Lam VZ (NatS (Var VZ))) ⟹
  (F (\w1-> case w1 of { Error -> Error;
                         N p2 -> (N (S p2)); F s2 -> Error; }))

Вроде бы всё правильно… Но смотреть на такие результаты суперкомпиляции как-то неприятно: суть дела в них затемнена непрерывными манипуляциями с конструкторами (“тегами”) Error, N и F. При каждой операции эти теги снимаются с данных, а потом тут же снова надеваются. Особенно наглядно это видно из реализации функции evalNatS. Казалось бы, всего и делов-то: надеть на аргумент конструктор S. Да не тут-то было. Сначала нужно проверить: а действительно ли в качестве аргумента подано число? А вдруг в аргументе Error или функция? Если на входе действительно число, с него нужно содрать тег N, надеть на число конструктор S, а потом надеть тег N обратно. Куча тупой и глупой работы! Да и текст интерпретатора от этого заметно раздувается.

Но, как бы то ни было, интерпретатор первого порядка для языка с переменными изготовить удалось (что было изначально понятно из общих соображений). А теперь мы переходим к следующему, более интересному вопросу: а можно ли реализовать язык λ-исчисления с помощью комбинаторов? При этом хотелось бы сделать это не для λ-исчисления с динамической типизацией (в духе языков Lisp или Scheme), а со статической (в духе Standard ML и Haskell)? А не помешает ли статическая типизация собирать проблемно-ориентированные программы из комбинаторов? Допустим, каждый из комбинаторов по отдельности мы сумеем придумать, а при попытке их соединить вместе получим “по рукам” от проверяльщика типов (type-checker-а)?

А между тем, очевидно, что желательно определять комбинаторы именно с помощью типизированного языка, поскольку в этом случае проверяльщик типов контролирует правильность соединения комбинаторов в ПО-программу. Без такой проверки использование комбинаторов превращается в нечто похожее на хождение по минному полю: чуть-чуть ошибёшься - и поди разбери что за бред полезет при попытке исполнить ПО-программу…

Кстати, разработчики самоприменимых частичных вычислителей лет 20 назад напоролись на проблему плохой совместимости статической типизации с самоприменением функций. Получалось так, что в частичном вычислителе, написанном на языке со статической типизацией, обрабатываемые программы и данные приходилось кодировать, чтобы погрузить их в некий “универсальный” тип данных. А при попытке самоприменения эта искусственная кодировка потом вываливалась в остаточную программу в виде ненужных “тегов”, делающих её громоздкой и неэффективной.

Например, если интерпретируемый язык разрешает использовать конструкции со связанными переменными, значения переменных нужно хранить в виде “среды”. Допустим, есть в программе переменная i типа Int, связанная со значением 25, и переменная s типа String, связанная со значением "abc". Тогда среда, связывающая переменные со значениями, выглядит так:

[(i, 25), (s, "abc")]

т.е. это список, состоящий из упорядоченных пар вида (v, a), где v - имя переменной, а a - её значение. В языке с динамической типизацией такие среды не создают никаких проблем. Но в языках вроде Standard ML и Haskell таким способом сконструировать среду нельзя! Ибо статическая полиморфная типизация по Хиндли-Милнеру требует, чтобы все элементы списка были /одного типа/! Стало быть, если значение одной переменной имеет тип Int, то и значения остальных переменных (из того же окружения) должны иметь тот же тип.

Ну и как же бороться с этим ограничением? Да очень просто: нужно, чтобы тип был одинаковый - сделаем. Определим такой тип данных:

data EnvVal = EnvInt Int | EnvString String;

и представим среду в виде

[(i, EnvInt 25), (s, EnvString "abc")]

(Собственно говоря, так и было сделано в интерпретаторе для λ-исчисления, рассмотренном выше.)

Теперь всё, вроде бы, становится “хорошо”: в каждой паре имя переменной связывается со значением типа EnvVal, и интерпретатор языка становится типизируемым. А расплата за это состоит в том, что интерпретатор вынужден работать с данными типа Int и String не напрямую, а всё время надевая на них и снимая “теги”: конструкторы EnvInt и EnvString.

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

И вот, представьте себе, эта маленькая, но гадкая, “проблема тегов” лет 20 висела над головой людей разрабатывавших частичные вычислители для языков со статической типизацией. Писались статьи, выдумывались изощрённые алгоритмы для удаления тегов из остаточных программ, защищались диссертации… А оказалось, что решение - существует! И лежало оно на поверхности, у всех на виду! Поэтому, наверное, никто его и не замечал. :-)

Желающим ознакомиться с историей вопроса, с литературой посвящённой проблеме и с её решением советую покопаться в этой статье:

Пересказывать всю статью не буду, но основная идея решения очень проста. “Классический” подход - представление сред в виде списков, а типа данных “список” определяется так:

data List a = Nil | Cons a (List a);

У конструктора типов List a - только один типовый параметр, вот и получается, что все элементы списка должны иметь одинаковый тип. Но ведь нас никто не заставляет использовать для представления сред именно списки. А почему бы не изготавливать среды из пар? Например, кто нам мешает представить окружение, например, в таком виде:

((i, 25),  ((s, "abc"), ()))

т.е. соорудить среду из упорядоченных пар. А компоненты пары могут иметь разные типы!

Идея - проста и хороша, но если её попытаться применить к интерпретатору, написанному на языке первого порядка, она не работает. Причина в том, что такой интерпретатор представляет собой слишком “монолитное”, “сильно связанное” сооружение. Есть в таком интерпретаторе такое место, в которую сходятся все пути: это то место, где происходит распознавание типа интерпретируемой конструкции. Все пути проходят через функцию eval e env. А эта функция должна быть рассчитана на любое выражение e и любую среду env. Вот и получается, что при попытке приписать тип функции eval e env приходится рассчитывать на самый худший вариант: считать, что env может иметь любую структуру, и что все её элементы должны иметь одинаковый тип.

Однако, в результате “рассыпания” интерпретатора на набор комбинаторов картина сразу меняется! Каждой конструкции интерпретируемого языка соответствует отдельный комбинатор, и каждому вхождению этой конструкции в программу соответствует отдельный вызов комбинатора, которому можно приписать индивидуальный тип.

Итак, попробуем реализовать язык λ-исчисления в виде комбинаторов. В интерпретаторе первого порядка много места занимала возня не только с тегами, но и с именами переменных: нужно было уметь извлекать значение переменной из среды, а для этого - уметь сравнивать имена переменных. А нельзя ли вообще обойтись без имён переменных? Можно. Для этого можно заменить переменные “индексами де Брёйна”. Например, выражение

\x -> \y -> \ z -> z y x

можно представить в виде

\ \ \ 0 1 2

Для каждой переменной в выражении ищем лямбду, в которой она определяется и подсчитываем, через сколько других лямбд нужно “вылезти наружу” по пути к “своей” лямбде. Индексы де Брёйна описаны во многих классических сочинениях, поэтому формальный алгоритм перехода к ним описывать не буду, а лучше сразу перейду к тому, как ими воспользоваться.

Если уже мы решили все конструкции изображать комбинаторами, а комбинаторы - это функции, то отчего бы и индексы де Брёйна не изобразить функциями?

Начнём с того, что определим несколько нужных нам типов данных (“пустышку”, пару, булевские значения и натуральные числа) и парочку вспомогательных функций:

data Unit = U;
data Pair a b = P a b;
data Bool = True | False;
data Nat = Z | S Nat;

fst = \v -> case v of {P x y -> x;};
snd = \v -> case v of {P x y -> y;};

А теперь принимаем такое решение: пусть индексы де Брёйна 0, 1, 2, изображаются как varZ, varS varZ, varS (varS varZ)), где функции varZ и varS определены следующим образом:

varZ = \env -> fst env;
varS = \v env -> v (snd env);

Идея состоит в том, что переменные можно изображать функциями, которые как раз и осуществляют выборку нужных значений из среды! А сама среда при этом имён переменных не содержит, и состоит из одних значений переменных. Функция varZ извлекает из среды самое последнее значение, а функция (varS v) отбрасывает из среды верхнее значение и предлагает функции v выбрать из оставшейся части среды нужное значение.

Ну, а теперь не составляет труда выписать остальные комбинаторы, реализующие различные конструкции λ-исчисления. При этом, в случае интерпретатора первого порядка, у нас была функция eval e env, которая вычисляла значение выражения e в среде env. А в случае комбинаторного подхода, само выражение e, составленное из суперпозиции комбинаторов, является функцией, которая “заглатывает” среду env и выдаёт результат своего собственного вычисления в среде env! Получается такой набор комбинаторов:

natZ = \env -> Z;
natS = \n env -> S(n env);

lam = \e env x -> e (P x env);
app = \e1 e2 env -> (e1 env) (e2 env);
fix = \f env -> f (P (fix f env) env);

На первый взгляд эти определения выглядят загадочно, но на самом деле они написаны совершенно прямолинейным и бесхитростным способом.

С помощью описанных выше комбинаторов, например, выражение \x -> \y -> y x записывается следующим образом:

lam (lam (app varZ (varS varZ)))

Ну что же, хоть и “не сахар”, но внешне такая запись выглядит примерно так же, как и в случае абстрактного синтаксиса первого порядка. Основная разница заключается в том, что раньше lam, app и fix писались с большой буквы, а теперь пишутся с маленькой. :-)

Однако, если сравнить текст интерпретатора первого порядка с реализацией комбинаторов, то простота реализации на основе комбинаторов прямо-таки поражает воображение!

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

Например, захотелось нам добавить конструкцию (cst a), результатом вычисления которой является a, определяем комбинатор:

cst = \a env -> a;

который игнорирует среду и выдаёт a. Теперь в программе можно писать cst True и cst False. А если захотелось добавить условные выражения, определяем комбинатор if:

if = \e0 e1 e2 env ->
  case e0 env of {
    True -> e1 env;
    False -> e2 env;
  };

А те комбинаторы, что уже есть, модифицировать не надо.

Для вычисления замкнутых выражений в пустой среде также определим функцию run:

run = \e -> e U;

И вот теперь наступает интересный момент. А что получится, если посуперкомпилировать выражения λ-языка, представленные с помощью комбинаторов? Пробуем, и вот что получается:

run (natS (natS natZ)) ⟹ (S (S Z))
run (app (lam varZ) (cst True)) ⟹ True
run (lam (if (varZ) (natS natZ) natZ)) ⟹
   (\y-> case y of { True -> (S Z); False -> Z; })
run (fix (natS varZ)) ⟹ (letrec f=(S f) in f)

И самое приятное состоит в том, что результаты суперкомпиляции теперь получаются чистенькие и аккуратные! Нету никаких тегов и манипуляций с ними. Результаты получаются именно те, которые и должны были получиться из здравого смысла.

Да и за суперкомпилятор HOSC душа радуется. Если посмотреть на графы конфигураций, которые получаются в случае работы с комбинаторами, то видно, что их размер, значительно меньше, чем в случае, когда HOSC-у приходится иметь дело с интерпретатором первого порядка. А это - очень важно в тех случаях, когда суперкомпилятор используется как средство анализа программ и доказательства утверждений о программах. Если граф конфигураций невелик, и смысл его понятен из здравого смысла, тогда есть основания доверять доказательству, построенному с помощью суперкомпиляции. А если граф конфигураций громаден и загадочен, то и понять, что он означает становится невозможно. А как тогда убедиться, что этот граф реально что-то доказывает, а не является следствием клопов, недовыловленных и ползающих в недрах суперкомпилятора?

Можно погонять и посуперкомпилировать интерпретатор, реализованный через комбинаторы вживую используя заранее заготовленное задание Lambda: higher-order syntax для суперкомпилятора HOSC.

Оригинал послания и комментарии