3

どのような条件でエラーが発生したかを確認するために、コードを単純化することにしました。ST s (STArray s x y)次のような単純なネストされた「s」から始めます。

{-# LANGUAGE RankNTypes #-}
import Control.Monad.ST
import Control.Applicative

data Foo s = Foo { foo::Bool }

newFoo :: ST s (Foo s)
newFoo = return $ Foo False

状態コードをテストするために、次の変換を実行します。

changeFoo :: (forall s. ST s (Foo s)) -> ST s (Foo s)
changeFoo sf = do
   f <- sf
   let f' = Foo (not $ foo f)
   return f'

状態を維持したまま状態から値を抽出したいので、次のステップは Bool 値を抽出することです。

splitChangeFoo :: (forall s. ST s (Foo s)) -> ST s (Bool,(Foo s))
splitChangeFoo sf = do
   f <- changeFoo sf
   let b = foo f
   return (b,f)

その Bool を抽出するには、 を使用する必要がありますrunST。私の理解では、これにより追加の状態が作成されます。これはforall s.、戻り値の型にa を指定することで指定します。

extractFoo :: (forall s. ST s (Bool,(Foo s))) -> (forall s. (Bool,ST s ((Foo s))))
extractFoo sbf = (runST $ fst <$> sbf,snd <$> sbf)

上記の例はファイナルなしでコンパイルされますforallが、デバッグしようとしている状況ではこれは不可能です。とにかく、この場合、どちらの方法でもコンパイルされます。

上記のコードを使用して、状態の複数の使用を一緒に連鎖させることができます。

testFoo :: (Bool, ST s (Foo s))
testFoo = (b && b',sf')
   where
      (b,sf) = extractFoo $ splitChangeFoo newFoo
      (b',sf') = extractFoo $ splitChangeFoo sf

今、私は IO をミックスに投入しようとしているので、適用可能な fmap を利用しています<$>。これはコンパイルされません: (NB. または を使用した場合と同じfmap問題)>>= return<$>

testBar :: IO (Bool, ST s (Foo s))
testBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'
   where
      testBar' :: IO (Bool, ST s (Foo s))
      testBar' = return $ extractFoo $ splitChangeFoo newFoo

次のエラーが発生します。

Couldn't match type `s0' with `s2'
  because type variable `s2' would escape its scope
This (rigid, skolem) type variable is bound by
  a type expected by the context: ST s2 (Foo s2)
The following variables have types that mention s0
  sf :: ST s0 (Foo s0) (bound at src\Tests.hs:132:16)
Expected type: ST s2 (Foo s2)
  Actual type: ST s0 (Foo s0)
In the first argument of `splitChangeFoo', namely `sf'
In the second argument of `($)', namely `splitChangeFoo sf'
In the expression: extractFoo $ splitChangeFoo sf

ST関数の構成に関するこのSOの質問から、STのすべての可能な用途がコンパイラによって説明されているわけではないことを認識しています。この仮定をテストするために、上記の関数を変更して IO を使用せず、戻り値をラムダに渡すだけにしました。

testFooBar :: (Bool, ST s (Foo s))
testFooBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) testFooBar'
   where
      testFooBar' :: (Bool, ST s (Foo s))
      testFooBar' = extractFoo $ splitChangeFoo newFoo

予想通り、これも同じエラー メッセージでコンパイルされません。

これには課題があります。深くネストされた一連の ST 操作と対話する必要がある IO の妥当な量があります。1 回の繰り返しでは問題なく動作しますが、戻り値をさらに利用することはできません。

4

1 に答える 1

0

このすべてが実際のコードでどのように機能するかはわかりません。厳密に必要なものよりも複雑なことをしているように思えますが、それについて決定的なことを言うことはできないので、あなたの質問の差し迫った問題。

testBar機能しない理由

には、 type(\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'を持つがあります。ただし、type を持っています。インスタンス化された後にのみ適用できます。<$>forall a b. (a -> b) -> IO a -> IO btestBarforall s. IO (Bool, ST s (Foo s))fmaptestBars

あなたの場合、sは新しい変数s0にインスタンス化されるため、ラムダ内にsfもそのパラメーターがあります。残念ながら、これは最上位のパラメーター (戻り値の型で確認したい) とs0は異なるため、現在はほとんど使用できません。ssf

の場合testFooBar、問題は、ラムダ引数がデフォルトでモノモーフィックであることです (さもないと、型推論が決定不能になります)。そのため、型に注釈を付けるだけで済みます。

testFooBar :: (Bool, ST s (Foo s))
testFooBar =
  (\(x :: forall s. (Bool, (ST s (Foo s)))) -> extractFoo $ splitChangeFoo $ snd x) testFooBar'
   where
      testFooBar' :: (Bool, ST s (Foo s))
      testFooBar' = extractFoo $ splitChangeFoo newFoo

ここでやったのは、letandwhere式の扱いにくい代替手段を導入したことだけです。しかし、ラムダ引数が完全にインスタンス化された型を持つ必要があるため、これはほとんど意味がありませtestFooん。fmap

次のことを試してみましょう。

{-# LANGUAGE ScopedTypeVariables #-}

testBar :: forall s. IO (Bool, ST s (Foo s))
testBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'
   where
      testBar' :: IO (Bool, ST s (Foo s))
      testBar' = return $ extractFoo $ splitChangeFoo newFoo

testBarこれで、最初に適切なsパラメーターが得られました。もう一般化されていないので、fmapすぐに適用できます。ラムダの内部にsfは type がありST s (Foo s)ます。しかし、量化された引数をextractFoo期待し、単相的であるため、これもうまくいきません。このバージョンを GHCi で試してみると、表示されるエラー メッセージはもはや skolem のエスケープに関するものではなく、昔ながらの.forallsfcan't match type s with s2

それを助ける方法

明らかに、何らかの形で-edextractを返さなければなりません。GHCにはポリモーフィックな戻り値の型がないため、元の型は役に立ちません。forall s.ST s (Foo s)

(forall s. ST s (Bool, Foo s)) -> (forall s. (Bool, ST s (Foo s)))

実際に意味する

forall s. (forall s. ST s (Bool, Foo s)) -> (Bool, ST s (Foo s))

GHC はすべてのforall-s をスコープの先頭にフロートアウトするためです。これにより、型推論が容易になり、より多くの用語を型チェックできるようになります。実際、:t extractGHCi を入力すると、浮き出た型が表示されます。

可能な解決策は、有効ImprediactiveTypesにして持つことです

extract :: (forall s. ST s (Bool, Foo s)) -> (Bool, forall s. ST s (Foo s))

しかし、めったに使用されないのには理由ImpredicativeTypesがあります。他の型チェック機構との統合が不十分であり、最も単純な目的以外では失敗する傾向があります。例として、変更された型を想定extractすると、次の例では型チェックが行われません。

testBar :: IO (Bool, forall s. ST s (Foo s))
testBar = (\(b, sf) -> (b, sf)) <$> testBar'
  where
    testBar' :: IO (Bool, forall s. ST s (Foo s))
    testBar' = return $ extractFoo $ splitChangeFoo newFoo

しかし、!に変更(\(b, sf) -> (b, sf))すると型チェックが行われます。(\x -> x)したがって、非予測型については忘れましょう。

通常の解決策は、数量化された型を newtype でラップすることです。これは、非予測型よりもはるかに柔軟性が低くなりますが、少なくとも機能します。

{-# LANGUAGE RankNTypes #-}

import Control.Monad.ST
import Control.Applicative
import Control.Arrow

data Foo s = Foo { foo::Bool }
newtype ST' f = ST' {unST' :: forall s. ST s (f s)}

newFoo :: ST s (Foo s)
newFoo = return $ Foo False

splitChangeFoo :: ST s (Foo s) -> ST s (Bool, Foo s)
splitChangeFoo = fmap (\(Foo b) -> (b, Foo (not b)))

extract :: (forall s. ST s (Bool, Foo s)) -> (Bool, ST' Foo)
extract s = (runST $ fst <$> s, ST' $ snd <$> s)

testBar :: IO (Bool, ST s (Foo s))
testBar = (\(_, ST' s) -> second unST' $ extract $ splitChangeFoo s) <$>
          (return $ extract $ splitChangeFoo newFoo)

したがって、数量化された型を返す必要があるときはいつでも、それを newtype でラップし、必要に応じてラップを解除します。カスタム型に対して共通の型引数スキームに固執したい場合があります (たとえば、sパラメーターを常に最後にして、ST'ラップされる複数の型に対して単一の型を使用できるようにします)。

于 2014-10-04T12:47:30.340 に答える