4

我正在阅读这篇出色的论文“结构化图的函数式编程，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
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 是存在量化的）。

解决问题

下一个问题是“如何编译？” 这不是问题——问题是请求指定不正确。我不知道你想要什么，而不是编译器。我可以建议一种使其编译的方法：

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}

我们真的在看 rank 2 类型：

type Stream a = forall v. Stream a v

您可以在第 4.1 节中看到v变量用于将流送入自身的方式。这是通用的原因是因为它允许流的使用者使用任何类型的 for v，因此，v不需要出现在 for 的签名中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-independent PStream av -- 一个类型的项目forall v . PStream a v来制作一个Str a. 所以P onesforones定义如上，因为我没有用v来定义。相比之下，与您的

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

的类型P可以让我们Str a用你喜欢的任何旧的 a 和 v 构造 a ，甚至 v 的类型在结果中也是不可见的Str a。所以P "Hello"将是这种类型的有效成员。Int当类型 b 专门用于而不是时，祝你在下面提取 x 好运String：

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 回答