April 5th, 2009

with Cat The Cat

Зависимые типы для стековых языков.

Да хотя бы просто типы. ;)

Хотя про просто типы для Форта я уже писал.

На мысль меня натолкнули заметки для презентации про Factor, которые я обнаружил по ссылке из Google Alerts. Плюс, я когда-то давно боялся отсутствия единственного наиболее общего типа. Сейчас я не этого боюсь, поэтому можно прикинуть, что к чему.

Насчёт синтаксиса. В квадратных скобках записывается quote-цитата, последовательность операций. exec выполнит цитату на вершине стека, предварительно её оттуда забрав. f = quotea - определение f, которое в тексте другой цитаты будет развёрнуто в quote exec.

Начну с пары (которая tuple).

Парой можно считать два элемента на вершине стека. (... -- fst snd)

Тогда fst = [ swap drop ], а snd = [ drop ].

Теперь селекторы истина и ложь:

true = [ fst exec ] // (thenQ elseQ -- 'thenQ) - оставит на стеке эффект thenQ
false = [ snd exec ] // (thenQ elseQ -- 'elseQ) - а тут эффект elseQ

if = [ exec ] // (thenQ elseQ bool -- '(thenQ или elseQ) )

if берёт цитату-селектор с вершины стека и применяет её. Селектор, в свою очередь, делает проекцию пары цитат (fst или snd) и применяет её результат.

Списки и числа можно делать на зависимых парах, надо просто хранить селектор в одной из частей пары. Правда, для конструирования понадобятся empty_quote (эффект которой пустая последовательность на вершине) и conquote (добавить одну последовательность в голову другой). Что начинает напоминать ΠΣ.

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

Подумаю на неделе. И почитаю. ;)
Если сказать, что справа от равенства в определениях должна стоять последовательность, создающая цитату на вершине стека, то получается лёгкое метапрограммирование.