Đa hình hàng trong Haskell: rắc rối khi viết Forth DSL với "biến đổi"

Question

Tôi đã được lấy cảm hứng từ hoạt động blog Haskell gần đây để thử viết một Forth giống như DSL trong Haskell. Cách tiếp cận tôi đã là đồng thời đơn giản và khó hiểu:

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

Đối với làm những việc đơn giản, hoạt động này khá độc đáo:

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 

chức năng đơn giản trivially có thể được biến đổi thành nhiều biến thể ngăn xếp tương ứng của họ. Một số chơi xung quanh mang lại kết quả thú vị cho đến nay:

ghci> runF $ start _1 _1 neg add 
0 

Vấn đề xảy ra khi tôi cố gắng mở rộng này với các chức năng bậc cao.

-- 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 là nghĩa vụ phải chuyển đổi một chồng các hình thức (s :> (s :~> s')) mẫu s, bởi về cơ bản "áp dụng" sự chuyển đổi (tổ chức tại đỉnh của stack) để "nghỉ ngơi" của nó. Tôi tưởng tượng nó nên công việc như thế này:

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

Nhưng trong thực tế, nó mang lại cho tôi một khổng lồ lỗi loại không phù hợp. Tôi đang làm gì sai? Biểu diễn "chuyển đổi ngăn xếp" có thể xử lý đủ các hàm bậc cao hơn hay tôi cần điều chỉnh nó?

N.B. Không giống như cách các chàng trai đã làm điều đó, thay vì start push 1 push 2 add end, tôi muốn nó là runF $ start (push 1) (push 2) add, ý tưởng được rằng có lẽ sau này tôi có thể làm việc một số phép thuật typeclass để làm cho các push tiềm ẩn cho một số literals.

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

Answer 1

Loại :~> của bạn không phải là những gì bạn thực sự muốn (do đó là ImpredicativeTypes). Nếu bạn chỉ cần loại bỏ chú thích loại từ call thì mẫu cuối cùng của bạn sẽ hoạt động như mong đợi. Một cách khác để làm cho nó hoạt là sử dụng loại ít ưa thích nhưng thích hợp hơn với tham số phụ:

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

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

Nhưng nếu những gì bạn đang theo đuổi là một cú pháp DSL đẹp và bạn có thể chịu đựng OverlappingInstances sau đó bạn có thể thậm chí khá nhiều được Loại bỏ chức năng:

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

Vấn đề là loại từ đồng nghĩa bạn là một loại đa hình

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

Sử dụng một loại đa hình như một tham số cho một loại constructor khác hơn -> là được gọi là "impredicativity". Ví dụ: những điều sau đây sẽ là sử dụng không đúng nghĩa

Maybe (forall a. a -> a) 

Vì nhiều lý do khác nhau, việc suy luận với độ khó chịu là khó khăn, đó là lý do GHC phàn nàn. (Cái tên "impredicative" xuất phát từ logic và các đẳng cấu Curry-Howards.)

Trong trường hợp của bạn, giải pháp đơn giản là sử dụng một kiểu dữ liệu đại số với một constructor:

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

Về cơ bản, constructor rõ ràng StackArr cung cấp đủ gợi ý cho trình kiểm tra kiểu.

Hoặc, bạn có thể thử tiện ích mở rộng ngôn ngữ ImpredicativeTypes.