Полиморфизм строк в Haskell: проблемы написания Forth DSL с "трансформациями"
Недавняя активность в блоге Haskell1 вдохновила меня на попытку написать Forth-подобный DSL на Haskell. Принятый мной подход одновременно прост и запутан:
{-# LANGUAGE TypeOperators, RankNTypes, ImpredicativeTypes #-}
-- a :~> b represents a "stack transformation"
-- from stack type "a" to stack type "b"
-- a :> b represents a "stack" where the top element is of type "b"
-- and the "rest" of the stack has type "a"
type s :~> s' = forall r. s -> (s' -> r) -> r
data a :> b = a :> b deriving Show
infixl 4 :>
Для выполнения простых вещей это работает довольно приятно:
start :: (() -> r) -> r
start f = f ()
end :: (() :> a) -> a
end (() :> a) = a
stack x f = f x
runF s = s end
_1 = liftS0 1
neg = liftS1 negate
add = liftS2 (+)
-- aka "push"
liftS0 :: a -> (s :~> (s :> a))
liftS0 a s = stack $ s :> a
liftS1 :: (a -> b) -> ((s :> a) :~> (s :> b))
liftS1 f (s :> a) = stack $ s :> f a
liftS2 :: (a -> b -> c) -> ((s :> a :> b) :~> (s :> c))
liftS2 f (s :> a :> b) = stack $ s :> f a b
Простые функции можно тривиально преобразовать в соответствующие им преобразования стека. Некоторая игра вокруг дает пока приятные результаты:
ghci> runF $ start _1 _1 neg add
0
Проблемы возникают, когда я пытаюсь расширить это на функции более высокого порядка.
-- this requires ImpredicativeTypes...not really sure what that means
-- also this implementation seems way too simple to be correct
-- though it does typecheck. I arrived at this after pouring over types
-- and finally eta-reducing the (s' -> r) function argument out of the equation
-- call (a :> f) h = f a h
call :: (s :> (s :~> s')) :~> s'
call (a :> f) = f a
call должен преобразовать стек вида (s :> (s :~> s')) в вид s, по сути "применяя" преобразование (хранящееся в вершине стека) к "остальной" его части. Я представляю, что это должно работать следующим образом:
ghci> runF $ start _1 (liftS0 neg) call
-1
Но на самом деле, это дает мне огромную ошибку несоответствия типов. Что я делаю не так? Может ли представление "преобразование стека" достаточно хорошо обрабатывать функции более высокого порядка, или мне нужно его подправить?
1N.B. В отличие от того, как это сделали эти ребята, вместо start push 1 push 2 add end, я хочу, чтобы это было runF $ start (push 1) (push 2) add, идея в том, что, возможно, позже я смогу использовать некоторую магию типовых классов, чтобы сделать push неявным для определенных литералов.