January 24th, 2009

with Cat The Cat

Про систему типов для стековых машин.

Источник (см. 00index.html).

Здесь же будет моя интерпретация.

В традициях Форта указывать стековый эффект определяемого слова:
: OVER ( a b -- a b a )
  ...
;
В скобочках-комментариях стоит стековый эффект: слева от тире (--) ожидаемый стек, точнее, наиболее доступные элементы, справа - наиболее доступные элементы после выполнения функции. Получается своего рода сравнение с образцом: если применим образец слева, то можно выполнять и будет применим образец справа.

Или немного по-другому:
: OVER ( α a b -- α a b a )
  ...
;
α - это неизменная для обеих образцов часть стека. Теперь соответствие со сравнением с образцом полное, причем сравниваем мы со списком: (a:as) и (&alpha a) отличаются только порядком хвоста и головы.

Проверять просто: ведём учёт стековых эффектов и сравниваем. Если всё совпало, то всё в порядке, не совпало - всё плохо. Стек на вход в main пуст (или, допустим, содержит количество аргументов и сами аргументы), стек на выход main тоже пуст (или содержит код выхода). В общих чертах практически всё.

Загвоздка находится в области "функций высших порядков". ;)

В Форте и других соединяющих языках есть примитив "выполнить примитив, адрес которого на стеке". Называется он EXEC и его тип в Форте излишне прост: EXEC ( xt -- ). Он ничего не говорит о стековом эффекте xt.

Если попытаться записать этот тип более правильно, то получится что-то вроде:
: EXEC ( α ( &alpha -- %beta; ) -- β )
Греческие буквы - части стека. Мы принимаем на вход какой-то образец стека α плюс умеющий с ним обращаться xt типа ( &alpha -- %beta;). На выходе получим другой образец стека.

Когда я сообразил, как можно типизировать EXEC, я очень обрадовался. Радовался я недолго, поскольку мне в голову пришла идея попытаться вывести тип для последовательности EXEC EXEC.

Меньше двух типов для такой последовательности у меня не выходило. Больше - получилось, меньше - нет. ;)

Количество типов зависило от того, имелся ли специальный символ ε для обозначения пустого стекового образца.

Кстати, в более ранних попытках создать практичную систему типов для Форта были и такие варианты:
: CHECK-NON-ZERO ( int -- int TRUE )
                  ( int -- FALSE )
  DUP 0 /= \ a a/=0
  DUP NOT \ a a/=0 a==0
  IF SWAP DROP THEN \ желаемый эффект
;
Что-то мне напоминает. ;)