4

我对程序员类别理论的第 8 章很感兴趣。

在 8.3 节中，Bartosz 定义了这种类型

newtype BiComp bf fu gu a b = BiComp (bf (fu a) (gu b))

在这里，如果我对 Haskell有所了解bf，fu, 和gu是类型构造函数，类型为bfkind(* -> *) -> (* -> *) -> * -> * -> *和fuand （就像or一样），而, 和是 kind 的一般类型；左边是一个类型构造函数，写起来很长，而右边是一个值构造函数，所以它是 type 。gu* -> *Maybe[]ab*BiComp =BiComp (bf (fu a) (gu b)) -> BiComp bf fu gu a b

然后作者在and中做BiComp了一个双函子，前提是类型构造函数参数也是 a ，并且类型构造函数and是s：abbfBifunctorfuguFunctor

instance (Bifunctor bf, Functor fu, Functor gu) => Bifunctor (BiComp bf fu gu) where
    bimap f1 f2 (BiComp x) = BiComp ((bimap (fmap f1) (fmap f2)) x)

到目前为止一切顺利，在这一点上对我来说一切似乎都是合理的。除了对类型构造函数和值构造函数使用相同的名称可能会让我迷失方向。

现在我很想提出以下意见：

  • bimap定义右侧的那个是利用约束的那个：它是bimap假定在Bifunctor任何类型的构造函数的实例中定义的那个bf，因此它bimap有 type (a -> a') -> (b -> b') -> bf a b -> bf a' b'；我认为这没有下面的那么有趣，因为它毕竟只是8.1 中呈现bimap的Bifunctor类型的签名；class
  • 相反，bimap左边的 是我们在其第 4 和第 5 个参数中定义BiComp的；Bifunctor以及参数f1和f2是必须作用于类型实体的函数，这些实体是 的第 4 个和第 5 个参数BiComp；因此， thisbimap的类型是(a -> a') -> (b -> b') -> BiComp bf fu gu a b -> BiComp bf fu gu a' b'。

它是否正确？

如果是这样，那么我不明白以下内容

bimap :: (fu a -> fu a') -> (gu b -> gu b') -> bf (fu a) (gu b) -> bf (fu a') (gu b')

因为这是bimap右边的类型，我在上面的要点中写的那个，除了它是用a= fu a，a'=等写fu a'的。

我是否遗漏了什么（或过度思考......）？

4

1 回答 1

5

你很接近。

首先，你有一种bf错误。它实际上只是* -> * -> *，这完全符合预期，因为它将是一个Bifunctor. 当然，那种BiComp很疯狂：

BiComp :: (* -> * -> *) -> (* -> *) -> (* -> *) -> * -> * -> *

至于您的要点中的类型，从技术上讲，它们都是正确的，但使用新的类型变量（尤其是对于您的第一个要点中的类型！）可能有助于使这一切更加清晰。其实bimap右边的有类型

bimap :: forall c c' d d'. (c -> c') -> (d -> d') -> bf c d -> bf c' d'

我们需要使用它来制作将我们的输入值类型转换为类型bf (fu a) (gu b)输出值的东西bf (fu a') (gu b')。只有让我们才能做到这一点c ~ fu a, c' ~ fu a', d ~ gu b, d' ~ gu b'。让我们看看这对我们的 RHS 有什么影响bimap：

bimap :: (fu a -> fu a') -> (gu b -> gu b') -> bf (fu a) (gu b) -> bf (fu a') (gu b')

啊哈！这正是您在右侧找到的内容！而且，我们可以准确地提供我们需要的论据。首先，类型的函数fu a -> fu a'。好吧，我们有一个给定的函数f1 :: a -> a'，我们知道它fu是一个函子，所以我们可以用fmap f1. 与f2和fmap f2一样，一切都很好。

于 2021-01-23T18:51:56.540 回答