使用存在

Question

我正在阅读这篇优秀的论文"结构化图形的功能编程,Bruno C. d.S. Oliveira"(这里有一些视频),我正试图实现所有的结构.我正在努力使用存在感.尽管作者提到了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.后者使您的代码编译.