4

私はこの優れた論文「構造化グラフを使用した関数型プログラミング、ブルーノC. d。S.オリベイラ」（ここにいくつかのビデオ）を読んでおり、すべての構造を実装しようとしています。私は実存主義の使用に苦労しています。著者はHaskellthroghoutについて言及していますが、タイプはCoqまたはAgdaでより簡単に表現されるようです。どうすればこれをコンパイルできますか？ありがとう。

コード

data PStream a v = Var v
                 | Mu (v -> PStream a v)
                 | Cons a (PStream a v)

data Stream a = forall v. Pack {pop :: PStream a v} 


foldStream :: (a -> b -> b) -> b -> Stream a -> b
foldStream f k (Pack s) = pfoldStream s
    where pfoldStream (Var x)     = x
          pfoldStream (Mu g)      = pfoldStream (g k)
          pfoldStream (Cons x xs) = f x (pfoldStream xs)

エラー

error:
 Couldn't match type `v' with `b'
      `v' is a rigid type variable bound by
          a pattern with constructor
            Pack :: forall a v. PStream a v -> Stream a,
          in an equation for `foldStream'
          at C:\...\StructuredGraph.hs:17:17
      `b' is a rigid type variable bound by
          the type signature for
            foldStream :: (a -> b -> b) -> b -> Stream a -> b
          at C:\...\StructuredGraph.hs:17:1
    Expected type: PStream a b
      Actual type: PStream a v
    In the first argument of `pfoldStream', namely `s'
    In the expression: pfoldStream s
4

3 に答える 3

6

あなたは存在型を持っていますが、紙に記載されている型は普遍的であるように見えます（ただし、の定義を超えて読んだことはありませんStream）。

の間には大きな違いがあります

newtype Stream a = forall v. Pack { pop :: PStream a v }

と

newtype Stream a = Pack { forall v. pop :: PStream a v }

前者は、何が何であるかを知る方法がないため、このタイプにはあまり役に立ちませんv。後者はコードをコンパイルします。

于 2013-01-11T17:17:30.603 に答える
4

では、この (部分的な) 関数の型は何だと思いますか?

pfoldStream (Var x) = x

それは簡単です：

pfoldStream :: Stream a v -> v

あなたのfoldStream f k操作は基本的に を計算しpfoldstream . popます。タイプは何でしょう？

-- this is wrong
pfoldstream . pop :: PStream a -> v

そんなことはできません。存在の内部から型を返すことはできません。v右側にがあることに注意してください。何が正しいかをどうやって知るのvですか？vは存在的に修飾されているため、型チェッカーが持つ唯一の情報は型がv存在するということであり、その型が と等しいかどうかについての情報はありませんb。

もっと簡単な例を挙げることができます：

data E = forall a. E a
unpack (E x) = x

の型はunpack、Haskell の型システムでは表現できません。基本的には、それが求められているものです。タイプは になりますがunpack :: E -> x、任意のx (x は普遍的に量化されていません) ではなく、特定のx (x は存在量化されています) の場合です。

問題の修正

次の問題は「どうやってコンパイルさせるか」です。それは問題ではありません。問題は、リクエストが正しく指定されていないことです。コンパイラよりも、あなたが何を望んでいるのかわかりません。コンパイルする方法の 1 つを提案できます。

foldStream :: (a -> b -> b) -> b -> PStream a b -> b
foldStream f k s = pfoldStream s
    where pfoldStream (Var x)     = x
          pfoldStream (Mu g)      = pfoldStream (g k)
          pfoldStream (Cons x xs) = f x (pfoldStream xs)

これは存在修飾子を取り除きますが、他にそれを行う方法がわかりません。それはあなたが望むものではないと思います。コンパイルする別の方法は、コードをユーザーのスピーカーから "O Canada" を再生する関数に置き換えることですが、上記のコードよりも、必要なものとはさらに似ていないと思います。

論文を読む

私は論文を見ましたが、その型は実存的であるべきではないと思います。より高次の型を使用するべきだと思います。したがって、存在型の代わりに：

data Stream a = forall v. Pack {pop :: PStream a v}

私たちは実際にランク 2 のタイプを見ています:

type Stream a = forall v. Stream a v

セクション 4.1 で、v変数を使用してストリームをそれ自体にフィードする方法を確認できます。これが普遍的である理由は、ストリームの消費者が の任意の型を使用できるためv、vの署名に表示する必要がないためfoldStreamです。

于 2013-01-11T17:12:38.107 に答える
3

全員が一斉に答えたようです。以下のように、GADT 構文を使用するとStr、常にこれがよりわかりやすくなるということを指摘したかっただけfoldStreamです。私は論文のコードの準可読バージョンを持っているので、ここに掲載します: https://github.com/applicative/structured_graphs 

{-#LANGUAGE GADTs, RankNTypes#-}
data PStream a v = Var v
                 | Mu (v -> PStream a v)
                 | Cons a (PStream a v)
ones :: PStream Int v
ones = Cons (1 :: Int) ones

data Stream a where P :: forall a  . (forall v . PStream a v) -> Stream a

-- つまり、(構築するのが難しい) v に依存しない PStream av を使用します --forall v . PStream a vを作成するタイプのアイテムStr a。したがってP ones、ones定義に v を使用しなかったため、上記のように定義されています。対照的に、あなたの

data Stream a where P :: forall a v .      PStream a v        -> Stream a

の型により、好きな古い a と v でa をP構築でき、v の型でさえ、結果の では見えなくなります。したがって、このタイプの有効なメンバーになります。タイプ b がではなくに特化されている場合、以下の x を抽出して頑張ってください。Str aStr aP "Hello"IntString

foldStream  :: (a -> b -> b) -> b -> Stream a -> b
foldStream f k = pfoldStream . pop
    where pfoldStream (Var x)     = x
          pfoldStream (Mu g)      = pfoldStream (g k)
          pfoldStream (Cons x xs) = f x (pfoldStream xs)
          pop (P x) = x

の最初の (意図した) 宣言でStreamは、値を構築するのは困難ですが、使用するのは簡単です。もう一方の (「存在する」) 宣言では、値を作成するのは簡単ですが、基になる型が「非表示」であるため、値を使用するのは困難です。を定義しようとして、そのような値を使用するというこの困難に直面していましたpfoldStream。

于 2013-01-11T17:40:36.903 に答える