Полиморфизм строк в Haskell: проблема написания Forth DSL с "преобразованиями"

Question

Я был вдохновлен недавним блогом на Haskell^1, чтобы попробовать свои силы в написании 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

Но на самом деле это дает мне огромную ошибку несоответствия типов. Что я делаю неправильно? Может ли представление "преобразование стека" в достаточной степени обрабатывать функции высшего порядка, или мне нужно его настроить?

¹ NB В отличие от того, как эти парни сделали это, вместо start push 1 push 2 add endЯ хочу, чтобы это было runF $ start (push 1) (push 2) addидея в том, что, может быть, позже я смогу поработать над магией классов типов, чтобы push неявный для определенных литералов.

• https://github.com/leonidas/codeblog/blob/master/2012/2012-02-17-concatenative-haskell.md
• https://gist.github.com/1847747

Answer 1

Ваш :~> тип не то, что вы на самом деле хотите (следовательно, ImpredicativeTypes). Если вы просто удалите аннотацию типа из call тогда ваш последний образец будет работать как положено. Еще один способ заставить его работать - использовать менее сложный, но более подходящий тип с дополнительным параметром:

type Tran s s' r = s -> (s' -> r) -> r

call :: Tran (s :> (Tran s s' r)) s' r
call (a :> f) = f a

Но если то, что вы хотите, это хороший синтаксис DSL, и вы можете терпеть OverlappingInstances тогда вы даже можете в значительной степени избавиться от функций liftSx:

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, TypeFamilies,
             FlexibleInstances, FlexibleContexts,
             UndecidableInstances, IncoherentInstances  #-}

data a :> b = a :> b deriving Show
infixl 4 :>


class Stackable s o r where
    eval :: s -> o -> r


data End = End

instance (r1 ~ s) => Stackable s End r1 where
    eval s End = s


instance (Stackable (s :> a) o r0, r ~ (o -> r0)) => Stackable s a r where
    eval s a = eval (s :> a)

instance (a ~ b, Stackable s c r0, r ~ r0) => Stackable (s :> a) (b -> c) r where
    eval (s :> a) f = eval s (f a)

-- Wrap in Box a function which should be just placed on stack without immediate application
data Box a = Box a

instance (Stackable (s :> a) o r0, r ~ (o -> r0)) => Stackable s (Box a) r where
    eval s (Box a) = eval (s :> a)


runS :: (Stackable () a r) => a -> r
runS a = eval () a

-- tests
t1 = runS 1 negate End
t2 = runS 2 1 negate (+) End

t3 = runS 1 (Box negate) ($) End
t4 = runS [1..5] 0 (Box (+)) foldr End
t5 = runS not True (flip ($)) End

t6 = runS 1 (+) 2 (flip ($)) End

Answer 2

Проблема в том, что ваш синоним типа является полиморфным типом

type s :~> s' = forall r. s -> (s' -> r) -> r

Использование полиморфного типа в качестве аргумента для конструктора типа, отличного от -> называется "непредсказуемость". Например, следующее будет нецелесообразным использованием

Maybe (forall a. a -> a)

По разным причинам вывод типа с непредсказуемостью труден, поэтому GHC жалуется. (Название "непредсказуемый" происходит от логики и изоморфизма Карри-Ховардса.)

В вашем случае решение состоит в том, чтобы просто использовать алгебраический тип данных с конструктором:

data s :~> s' = StackArr { runStackArr :: forall r. s -> (s' -> r) -> r}

По сути, явный конструктор StackArr предоставляет достаточно подсказок для проверки типов.

Кроме того, вы можете попробовать ImpredicativeTypes расширение языка.