haskell - 存在词的使用

Question

我正在阅读这篇出色的论文 "Functional Programming with Structured Graphs, Bruno C. d. S. Oliveira" ( some video here )，并且正在尝试实现所有结构。我正在努力使用存在主义。虽然作者提到了 Haskell throghout，但似乎这些类型在 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

Answer 1

您有一个存在类型，但看起来论文中提到的类型是通用的(尽管我没有阅读超出 Stream 定义的内容)。

之间有很大的区别

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

和

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

前者对于这种类型似乎不是很有用，因为您无法知道 v 是什么。后者使您的代码编译。