Про систему типов для стековых машин.
Источник (см. 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 ( α ( α -- β ) -- β )Греческие буквы - части стека. Мы принимаем на вход какой-то образец стека α плюс умеющий с ним обращаться 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 \ желаемый эффект
;Что-то мне напоминает. ;)
Здесь же будет моя интерпретация.
В традициях Форта указывать стековый эффект определяемого слова:
: OVER ( a b -- a b a )
...
;В скобочках-комментариях стоит стековый эффект: слева от тире (--) ожидаемый стек, точнее, наиболее доступные элементы, справа - наиболее доступные элементы после выполнения функции. Получается своего рода сравнение с образцом: если применим образец слева, то можно выполнять и будет применим образец справа.
Или немного по-другому:
: OVER ( α a b -- α a b a )
...
;α - это неизменная для обеих образцов часть стека. Теперь соответствие со сравнением с образцом полное, причем сравниваем мы со списком: (a:as) и (&alpha a) отличаются только порядком хвоста и головы.
Проверять просто: ведём учёт стековых эффектов и сравниваем. Если всё совпало, то всё в порядке, не совпало - всё плохо. Стек на вход в main пуст (или, допустим, содержит количество аргументов и сами аргументы), стек на выход main тоже пуст (или содержит код выхода). В общих чертах практически всё.
Загвоздка находится в области "функций высших порядков". ;)
В Форте и других соединяющих языках есть примитив "выполнить примитив, адрес которого на стеке". Называется он EXEC и его тип в Форте излишне прост: EXEC ( xt -- ). Он ничего не говорит о стековом эффекте xt.
Если попытаться записать этот тип более правильно, то получится что-то вроде:
: EXEC ( α ( α -- β ) -- β )Греческие буквы - части стека. Мы принимаем на вход какой-то образец стека α плюс умеющий с ним обращаться 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 \ желаемый эффект
;Что-то мне напоминает. ;)