9

私は最近のHaskellブログアクティビティ1に触発されて、HaskellでForthのようなDSLを書いてみました。私が採用したアプローチは、同時に単純で紛らわしいものです。

{-# 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 N.B. これらの人がそれをした方法とは異なりstart push 1 push 2 add end、私はそれをしたいのですrunF $ start (push 1) (push 2) addが、おそらく後で私はいくつかの型クラスの魔法を使ってpush特定のリテラルの暗黙を作ることができるという考えです。

4

2 に答える 2

4

問題は、タイプの同義語がポリモーフィックタイプであるということです

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または、言語拡張機能を試すこともできます。

于 2012-02-18T13:14:37.830 に答える
3

あなたの:~>タイプはあなたが実際に望むものではありません（したがって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
于 2012-02-23T14:26:55.170 に答える