Типы в МПС
From IT SPb Academy
Contents |
Язык описания систем типов в МПС (видение)
Внимание! Самого языка ещё нет!
Система типов, описанная на нашем языке, на верхнем уровне представляет собой совокупность правил. Правила эти отличаются по своему виду от привычных правил вывода, принятых для формального описания систем типов, а именно тем, что являются более операционными, чем декларативными. Однако в дальнейшем для удобства я буду называть правила нашего языка правилами вывода.
Также в языке на верхнем уровне могут быть декларации контекстов и декларации групп уравнений.
Структура самих типов не описывается на нашем языке системы типов. Типами могут быть любые ноды МПС. Тип для нашего языка - это не что-то специально помеченное, а любой объект, унаследованный от SNode. Таким образом, структуру типов можно описывать на structure language отдельно, в отдельном языке, или, также, можно использовать некоторые концепты проверяемого языка в качестве типов. Таким образом, сами ноды-типы не знают, что они типы. Именно правила вывода задают типовую семантику этих нодов.
Правила вывода
Правило вывода состоит из двух частей. В первой части правила определяется, для каких нодов применимо данное правило. Во второй части описываются действия, которые надо произвести при нахождении подходящего нода.
Скорее всего, первая часть будет написана с использованием pattern language и query language, в виде конструкции, подобной select - where, где после select идёт имя концепта, к которому должен принадлежать нод, или шаблон, к которому должен подходить нод; а после where могут идти более сложные условия, накладываемые на нод, написанные на query language.
Вторая часть представляет собой последовательность команд (statements), которые собственно и обеспечивают вывод типов. Командами могут быть: - создание новой типовой переменной, - помещение типового утверждения в контекст, - проверка на наличие типового утверждения в контексте, - создание типового уравнения и помещение его в одно из множеств уравнений, - выполнение пользовательской квери, написанной на Java (в кверь в качестве аргументов передаются: рассматриваемый нод; данное правило вывода; подстановка, получившаяся в результате сравнения с шаблоном).
Команды
1. Создание типовой переменной на этапе написания правила выглядит просто как нод с именем (например, "newvar X"). На этапе выполнения создаётся типовая переменная с уникальным id, (например, "Х239"), переменная временно (на время обработки данным правилом текущего подходящего нода) связывается с декларацией(т.е. с "newvar X") и помещается в множество типовых переменных.
2. Далее нам понадобится понятие типового выражения.
Типовые выражения - это или просто типы, или типовые переменные, или ссылки на переменные шаблона, или, наконец, типы, в которых некоторые дети и свойства заменены на типовые выражения (a la template).
Типовое утверждение - это утверждение вида X : T, где T - типовое выражение, а X может быть или нодом (N : T), или типовой переменной (т.е. ссылкой на декларацию типовой переменной) (V : T). Контекст на этапе написания правила - это просто некое имя этого контекста, а на этапе выполнения - это множество типовых утверждений. Таким образом, на этапе выполнения данная команда интерпретируется как создание типового утверждения, (причём все переменные в типовом выражении заменяются на их значения), и добавление его в нужный контекст, то есть в нужное множество. Выглядеть она будет, например, так: Gamma <- x : T
Один из контекстов должен быть объявлен как главный - именно оттуда берутся типы нодов после завершения проверки типов.
3. Команда проверки наличия типового утверждения в контексте состоит из шаблона типового утверждения, имени контекста и тела команды - списка команд. При интерпретации команда выполняет поиск в указанном контексте типового утверждения, соответствующего шаблону. Для каждого найденного шаблона выполняется список команд из тела команды проверки. Например, Gamma contains x : #T { Delta <- y : #T }
4. Типовое уравнение - это выражение вида TE1 :=: TE2, где TE - типовые выражения, то есть или просто типы, или типовые переменные, или ссылки на переменные шаблона, или, наконец, типы, в которых некоторые дети и свойства заменены на типовые выражения (a la template). В процессе интерпретации создаётся пара из двух конкретных нодов (все переменные заменяются на их значения в момент создания уравнения).
Типовые уравнения помещаются в одно из нескольких множеств, или систем уравнений. Предполагается, что каждая из систем уравнений решается отдельно, а внутри системы уравнения решаются совокупно и нераздельно. Система уравнений решается стандартным алоритмом. Тривиальные уравнения (х = х) убираются, очевидно неверные уравнения (int = class) выдают типовую ошибку, уравнения с типовыми переменными (var = expr) порождают подстановку, прочие же уравнения разбиваются на несколько более простых.
Единственное при этом, что нам нужно знать про то, какие бывают типы - это то, что они бывают простые и составные. Простые типы - это ноды без детей. А составные типы - это ноды с детьми. Соответственно, сравнение двух типов происходит таким образом: типы равны, если они равны по своим концептам и пропертям, и если при этом их соответственные дети равны. Поэтому при решении типового уравнения сначала проверяется совместимость нодов по концептам и пропертям, а затем исходное уравнение исчезает, а в систему добавляются уравнения на соответственных детей этих нодов.
При решении системы уравнений, на каждом шаге либо одно уравнение заменяется на конечное число уравнений с меньшей глубиной типов, либо исчезает какое-либо уравнение, либо происходит подстановка, при которой исчезает одна типовая переменная, либо происходит ошибка. Совокупная глубина нодов конечна, число типовых переменных конечно, число уравнений изначально конечно и увеличивается при каждом шаге не больше, чем на максимальную степень нода - 1, причём число таких увеличивающих шагов не больше, чем совокупная глубина нодов, следовательно число уравнений ограничено и гарантированно начнёт уменьшаться после исчерпания всех увеличивающих шагов и неуменьшающих шагов(каковыми являются подстановки переменных). Таким образом, алгоритм завершится. Иначе можно сказать, что тройка (P, V, E) уменьшается при каждом шаге алгоритма, где P - совокупное число родителей у нодов в уравнениях, V - количество типовых переменных, E - количество уравнений, а порядок на тройках алфавитный.
Подитог основных понятий
Итак, основными понятиями нашего языка являются:
Типовая переменная
Типовое выражение
Уравнение
Система уравнений
Контекст
Команда
Список команд
Шаблон
Select-Where query
Правило вывода
