Полиморфизм строк в 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

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

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


polymorphism higher-order-functions haskell concatenative-language impredicativetypes
person Dan Burton    schedule 18.02.2012    source источник
comment
на самом деле, я бы тоже хотел избавиться от start и просто иметь runF $ _1 _1 add, хотя я действительно не понимаю, как это возможно с этой настройкой.   -  person Dan Burton    schedule 18.02.2012
comment
Непредикативные типы — это обобщение типов с рангом n, которые допускают forall внутри конструктора любого типа, а не только типов функций.   -  person Carl    schedule 18.02.2012

Ответы (2)


arrow_upward
3
arrow_downward

Ваш тип :~> — это не то, что вам действительно нужно (отсюда и 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
person Ed'ka    schedule 23.02.2012

arrow_upward
4
arrow_downward

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

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.

person Heinrich Apfelmus    schedule 18.02.2012
comment
Проблема с использованием объявления данных заключается в том, что оно загрязняет желаемый синтаксис. Причина, по которой синоним типа хорошо работает, заключается в том, что преобразование является функцией, и эти функции могут быть объединены в цепочку приложением функции, как если бы это была композиция функций. Я попробовал ImpredicativeTypes, что позволяет правильно напечатать call, но использовать call по желанию невозможно; есть что-то изначально неправильное с типом, который я дал. Я думаю, проблема в том, что программа проверки типов не может понять, как работает приложение функции на уровне типа. - person Dan Burton; 19.02.2012