Serguey Zefirov (thesz) wrote,
Serguey Zefirov
thesz

Зачем нужны выкрутасы с типами.

В общем, чтобы совершать меньше ошибок.

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

Это очень ценно в случае языков программирования - вообще, в случае языков, просто программирование ближе.

В качестве примера приведу стековую машину, она умеренно проста и умеренно интересна.

Итак, стековая машина.

Основной объект её действий - это стек. Стопка. Стек может быть пустым, а может состоять из головы и стека над ней, в этом он похож на список, только элементы на стеке могут быть самыми разными.

Стековая машина имеет свой "ассемблер", состоящий из слов: DUP, DROP, OVER, LITERAL, +, <= и тд.

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

DUP имеет стековый эффект ( a -- a a), дублируя значение на верхушке стека.

Стековый эффект DROP ( a --), сбрасывает любое значение с верхушки стека.

OVER интересней: ( a b -- a b a), копирует элемент, что под вершиной стека. 'a' и 'b' здесь "переменные типа", то есть, любое значение в ячейке стека.

LITERAL имеет целочисленный параметр, его эффект ( -- int), то есть, он кладёт что-то на стек.

Сложение + : ( Int Int -- Int). Здесь выбор небогат.

Как сформулировать стековый эффект в языке наподобие Хаскеля? Наиболее просто это делается с помощью обобщённых алгебраических типов. Сперва договоримся, что пустой стек будет обозначаться типом () (unit, состоит из одного значения ()), а непустой стек будет обозначаться вложенными скобочками: (стек,голова). Например, сложение на входе потребует стек ((((),Int)),Int), а на выходе даст стек ((),Int).

Так и запишем:
data StackOp instack outstack where
    StackPrim :: (instack -> IO outstack) -> StackOp instack outstack
Мы сделали описание примитивов, при этом практически не ограничив их. Если у нас есть функция dupS :: ((),a) -> IO (((),a),a), то мы можем сформировать примитив dup = StackPrim dupS. То же относится и к plus, и к LITERAL, и даже к слову под звучным названием '.', что выводит на печать лежащее на стеке число:
dotS :: Stack1 stk Int -> IO stk
dotS (stk,a) = print a >> return stk

dot = StackPrim dotS
Это так совпало, что print имеет тип print :: Show a => a -> IO (). То есть, возвращает пустой стек.

Вот ещё несколько полезных вещей:
type Stack1 stk a = (stk,a)
type Stack2 stk b a = (Stack1 stk b,a)
type Stack3 stk c b a = (Stack2 stk c b,a)

empty = ()
push stk a = (stk,a)
Теперь надо расширить список действий операцией соединения двух последовательностей стековых операций:
data StackOp instack outstack where
	StackPrim :: (instack -> IO outstack) -> StackOp instack outstack
	StackCat :: StackOp instack tempstack
		-> StackOp tempstack outstack
		-> StackOp instack outstack

(***) = StackCat

StackCat берёт одну последовательность, берёт вторую последовательность и делает третью последовательность. Обратите внимание, что выход первой последовательности и вход второй должны быть согласованы.

Теперь пришло время написать интерпретатор:
stackInterp :: inputstack -> StackOp inputstack outputstack -> IO outputstack
stackInterp stk (StackPrim action) = action stk
stackInterp stk (StackCat actA actB) = do
	tempStack <- stackInterp stk actA
	stackInterp tempStack actB
Здесь всё понятно, так? Действий у нас немного. Если мы напоролись на прямое действие, мы его и выполним. Если у нас соединение стековых эффектов, то выполним сперва первое, потом второе.

Напишем тест:
test = literal 10
	*** dup
	*** plus
	*** dot
и тут же можем выполнить: stackInterp () test. Должно напечатать 20.

Вот лог вывода типов для кусочков нашего теста:
*S> :t literal 10
literal 10 :: StackOp () (Stack1 Int)
*S> :t literal 10 *** dup
literal 10 *** dup :: StackOp () (Stack2 Int Int)
*S> :t literal 10 *** dup *** plus
literal 10 *** dup *** plus :: StackOp () (Stack1 Int)
*S> :t literal 10 *** dup *** plus *** dot
literal 10 *** dup *** plus *** dot :: StackOp () ()
*S> :t dup *** plus *** dot
dup *** plus *** dot :: StackOp (Stack1 Int) ()
*S> :t plus *** dot
plus *** dot :: StackOp (Stack2 Int Int) ()
*S> :t dot
dot :: StackOp (Stack1 Int) ()
*S>
Мы даже можем сделать условное выполнение, воспользовавшись готовым интерпретатором:
ifS :: StackOp inp outp -> StackOp inp outp -> (inp,Bool) -> IO outp
ifS thenAct elseAct (inp,cond) =
	if cond
		then stackInterp inp thenAct
		else stackInterp inp elseAct

ifs ta ea = StackPrim (ifS ta ea)
А вот его тест, с дополнительными определениями:
lessThanS :: Stack2 stk Int Int -> IO (Stack1 stk Bool)
lessThanS ((stk,b),a) = return (stk,b < a)
lessThan = StackPrim lessThanS

stringS :: String -> stk -> IO (Stack1 stk String)
stringS str stk = return (stk,str)
string str = StackPrim (stringS str)

printStringS :: Stack1 stk String -> IO stk
printStringS (stk,str) = putStrLn str >> return stk
printString = StackPrim printStringS


testNLess10 n = literal n
	*** literal 10
	*** lessThan
	*** ifs (string "less than 10") (string "bigger or equal than 10")
	*** printString
Прогон теста:
*S> stackInterp () (testNLess10 9)
less than 10
*S> stackInterp () (testNLess10 19)
bigger or equal than 10


Вот.

Исходник тут: http://thesz.mskhug.ru/svn/misc/TypedStack.hs

Там есть даже умеренно хорошее решение для очень интересной проблемы: как типизировать использование открытого файла. Стековый эффект этого действия таков: ( string -- handle TRUE | FALSE), то есть, у нас на вершине стека может быть возвращено либо два значения сразу, либо одно, при этом количество значений зависит от значения на вершине стека.

Я запихнул handle (в моём примере String) в тип Maybe Handle. А для ветвления использовал специальный вид if, maybes, он есть в исходнике. Он принимает на вход два действия, одно для случая, когда на вершине Just something, стековый эффект этого действия ( (inp,something) -- outp), и другое для случая, когда на вершине Nothing, стековый эффект этого действия ( inp -- outp). Комбинация действий приводит к общему стековому эффекту ( (inp,Maybe something) -- outp).

То же можно сделать для более сложного типа Either, когда стековый эффект подобен ( string -- handle TRUE | error-code FALSE). И тд, и тп.

Если кому-то в голову придёт реализовывать стековую машину в виде DSEL - вполне нормальная задача, кстати, вон, dmzlj отказался от Форта из-за большого количества ошибок в программах, а так он ему нравился, - то, конечно же, примитивы надо перенумеровать, условные конструкции сделать отдельными вариантами типа StackOp, сделать вызов именованных сущностей (те же определения через :; в Форте) и тд, и тп. Ядро останется таким же.

PS
Не забыть, что Maybe something занимает более одной ячейки в стеке, поэтому DUP и OVER не должны работать с такими значениями.

Типами же можно ограничить работу с двойными словами, что фортеры любят. Чак Мур, так тот вообще считал, что целочисленная арифметика годится в 99.9(9)%.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 165 comments