4

我通过阅读First Principles, Allen & Moronuki 的 Haskell Programming 一书来了解 Haskell 。

在 Monad Transformers, Functor & Applicative composition 一章的练习中，它要求读者为以下类型编写 Bifunctor 实例

data SemiDrei a b c = SemiDrei a

我的第一次尝试（编译）是

instance Bifunctor (SemiDrei a) where
    bimap f g (SemiDrei a) = SemiDrei a

但是，看着它，在我看来，我应该能够写bimap f g = id，因为最后一个参数是不变的或 write bimap f g x = x。两者都给了我编译错误，我希望有人能向我解释为什么我不能bimap用这些较短的替代方案来表达，即为什么我必须指定(SemiDrei a).

我在 Haskell 8.6.5 上运行了这个（如果相关的话）

尝试：身份证

instance Bifunctor (SemiDrei a) where
    bimap f g = id

-- compile error message:
• Couldn't match type ‘a1’ with ‘b’
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  ‘b’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  Expected type: SemiDrei a a1 c -> SemiDrei a b d
    Actual type: SemiDrei a b d -> SemiDrei a b d
• In the expression: id
  In an equation for ‘bimap’: bimap f g = id
  In the instance declaration for ‘Bifunctor (SemiDrei a)’
• Relevant bindings include
    f :: a1 -> b (bound at src/Main.hs:69:11)
    bimap :: (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
      (bound at src/Main.hs:69:5)
   |
69 |     bimap f g = id
   |                 ^^

尝试：fgx = x

instance Bifunctor (SemiDrei a) where
    bimap f g x = x

-- compile error message:
• Couldn't match type ‘a1’ with ‘b’
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  ‘b’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  Expected type: SemiDrei a b d
    Actual type: SemiDrei a a1 c
• In the expression: x
  In an equation for ‘bimap’: bimap f g x = x
  In the instance declaration for ‘Bifunctor (SemiDrei a)’
• Relevant bindings include
    x :: SemiDrei a a1 c (bound at src/Main.hs:69:15)
    f :: a1 -> b (bound at src/Main.hs:69:11)
    bimap :: (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
      (bound at src/Main.hs:69:5)
   |
69 |     bimap f g x = x
   |                   ^
4

3 回答 3

7

事实上，最后一个参数没有改变：它的类型发生了变化。输入为SemiDrei a x y，输出为SemiDrei a p q，其中f :: x -> p和g :: y -> q。

这意味着您必须解构原始类型的值并重构新类型的值，这就是您在原始实现中所做的。

但是您的直觉是正确的：这两个值确实具有相同的内存表示。而 GHC 可以推导出这个事实，当它推导出来时，它会自动Coercible为你解决一个约束，这意味着你可以使用该coerce函数将一个转换为另一个：

 bimap _ _ = coerce
于 2019-10-21T21:46:23.227 回答
6

这在更简单的情况下显示了相同的问题：

data T a = K

foo :: T a -> T b
foo K = K  -- type checks

bar :: T a -> T b
bar x = x  -- type error

-- bar = id would also be a type error, for the same reason

这里的问题是两个Kinfoo值隐藏了它们的类型参数。更精确的定义是

-- pseudo code
foo (K @a) = K @b

在这里您可以看到隐式类型参数发生了变化。当我们编写K. foo由于它们是隐式的，因此它们看起来好像是相同K的 s，但对于类型检查器来说它们不是。

相反，当我们x在 的定义中使用时bar，没有可推断的隐式类型参数。我们有，x :: T a仅此而已。我们不能使用x和声称具有不同类型的T b。

最后，请注意，使用“安全强制”我们可以执行直观正确的类型 -id将一种K（一种类型的）转换为另一种类型K的另一种：

import Data.Coerce

baz :: T a -> T b
baz = coerce

这是否更好是有争议的。对于简单的情况，模式匹配比 更容易理解coerce，因为后者可以执行大量（安全）强制，可能让读者猜测在类型级别实际发生的事情。

于 2019-10-21T21:43:59.223 回答
3

关键在于 的类型签名bimap：

bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d

在这种特殊情况下，如果我们专门p化SemiDrei a并重命名类型变量以避免与 that 混淆a，我们会得到：

bimap :: (b -> c) -> (d -> e) -> SemiDrei a b d -> SemiDrei a c e

因此，当您尝试实现此功能时：

bimap f g = ...

函数f和g是完全任意的，不仅在它们的实现上，而且在它们的输入和返回类型上也是如此。f有类型b -> cwhereb并且c绝对可以是任何东西——对于g. 您给出的定义必须绝对适用于调用者提供的任何类型和函数——这就是（参数）多态的含义。

如果我们现在用这些术语来看看你的三个定义，我们就可以解决这个明显的谜团：

第一的：

bimap f g (SemiDrei a) = SemiDrei a

正如您所见，这完全没问题。SemiDrei a有 type SemiDrei a b c，其中 onlya被指定。这意味着它可以采用任何类型，例如SemiDrei a Int String, 或SemiDrei [Bool] (Char, [Double]), 或其他任何类型。SemiDrei a它本身是多态的，它可以是任何兼容的类型。这意味着特别是它可以作为上述签名中的theSemiDrei a b c和 the 。SemiDrei a c ebimap

与您的其他尝试对比：

bimap f g = id

这里的问题是，尽管是多态的，但对于这个目的来说id，它的多态性还不够。它的类型是a -> a(for any a)，特别是可以专门化为SemiDrei a b c -> SemiDrei a b c. 但它不可能根据需要专门化为一个类型SemiDrei a b d -> SemiDrei a c e，因为b, c,d和e通常是完全不同的类型。回想一下，gets 的调用者可以bimap选择类型是什么——例如，他们可以轻松地选择函数f以及gwhereb和c是不同的类型，然后就id无法使用SemiDrei a b dto SemiDrei a c e，因为它们是不同的类型。

在这个阶段，您可能会反对该值SemiDrei a可以是所有此类类型的值。这是完全正确的，但它与类型推断无关——编译器只关心类型，而不关心它们可能包含哪些值。它必须考虑到不同的类型具有完全不同的、不相交的值。而且，说，SemiDrei a Int String实际上SemiDrei a Bool Char是不同的类型。同样，编译器不知道该Int类型的任何值实际上都没有使用 etc。这确实是为什么在实践中使用这种“幻像类型”（出现在类型定义中但不在其任何数据构造函数中的类型）的原因 - 以允许编译器能够按类型区分它们，即使运行时表示可能是完全等价的。

至于您的第三次尝试，bimap f g x = x这与前一次完全相同 - 它限制bimap f g其输出类型与其输入相同。（实际上完全等同于bimap f g = id。）

所以重要的一点是，在类型检查阶段，编译器只关心类型——并且具有不同名称的两种类型被（并且必须）被认为是完全不同的，即使它可能是等效值可以嵌入两个都。

于 2019-10-21T21:41:46.893 回答