Polimorfismo di riga in Haskell: problemi di scrittura di Forth DSL con "trasformazioni"

Question

Mi sono ispirato alla recente attività del blog Haskell per provare a scrivere una DSL simile a Forth in Haskell. L'approccio che ho preso è allo stesso tempo semplice e confusa:

{-# 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 :> 

Per fare le cose semplici, questo funziona abbastanza bene:

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 

funzioni semplici possono banalmente essere trasformati in loro trasformazioni pila corrispondenti. Alcuni giocano intorno produce risultati piacevoli finora:

ghci> runF $ start _1 _1 neg add 
0 

Il guaio arriva quando cerco di estendere questo con funzioni di ordine superiore.

-- 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 si suppone trasformare una pila di forma (s :> (s :~> s')) alla forma s, da essenzialmente "applicando" la trasformazione (presso la punta della pila) alla "riposo" di esso. Immagino che dovrebbe lavoro come questo:

ghci> runF $ start _1 (liftS0 neg) call 
-1 

Ma in realtà, mi dà un errore di tipo non corrispondente enorme. Che cosa sto facendo di sbagliato? È possibile che la rappresentazione della "trasformazione dello stack" gestisca sufficientemente le funzioni di ordine superiore o devo modificarla?

N.B. A differenza di come hanno fatto questi ragazzi, invece di start push 1 push 2 add end, voglio che sia runF $ start (push 1) (push 2) add, l'idea è che forse più tardi potrò lavorare un po 'di magia di classe per rendere implicito lo push per determinati valori letterali.

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

Answer 1

Il tuo tipo :~> non è quello che desideri realmente (da cui il ImpredicativeTypes). Se rimuovi l'annotazione del tipo da call, l'ultimo campione funzionerà come previsto. Un altro modo per farlo funzionare è quello di utilizzare il tipo meno fantasia ma più appropriato con parametro in più:

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

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

Ma se quello che cercate è un bel sintassi DSL e si è in grado di tollerare OverlappingInstances allora si può anche tranquillamente ottenere liberarsi di funzioni 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

Il problema è che il tipo di sinonimo è un tipo polimorfico

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

Utilizzando un tipo polimorfico come argomento di un tipo di costruttore diverso -> è chiamato "impredicatività". Per esempio, il seguente sarebbe un uso impredicativa

Maybe (forall a. a -> a) 

Per vari motivi, l'inferenza dei tipi con impredicativity è difficile, ecco perché GHC lamenta. (Il nome "impredicativa" deriva dalla logica e l'isomorfismo di Curry-Howard.)

Nel tuo caso, la soluzione è semplicemente di utilizzare un tipo di dati algebrico con un costruttore:

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

In sostanza, il costruttore esplicito StackArr fornisce sufficienti suggerimenti per il controllo del tipo.

In alternativa, è possibile provare l'estensione della lingua ImpredicativeTypes.