haskell - 为什么这个类型注释是错误的？

Question

我试图跟随 article by Gabriel Gonzalez我遇到了类型不匹配。考虑以下短模块:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE Rank2Types #-}

module Yoneda where

newtype F a = F a deriving (Show, Functor)

type G f a = forall a'. (a -> a') -> f a'

fw :: Functor f => G f a -> f a
fw x = x id

bw :: Functor f => f a -> G f a
bw x = \f -> fmap f x

它编译得很好。 (使用 ghc 8.2.2 和 8.4.3。) 但是当我在 repl 中输入它时，fw 和 bw 不要编写:

λ :t bw . fw

<interactive>:1:6: error:
    • Couldn't match type ‘a’ with ‘G f a1’
      ‘a’ is a rigid type variable bound by
        the inferred type of it :: Functor f => a -> (a1 -> a') -> f a'
        at <interactive>:1:1
      Expected type: a -> f a1
        Actual type: G f a1 -> f a1
    • In the second argument of ‘(.)’, namely ‘fw’
      In the expression: bw . fw

当我更仔细地查看 bw 时，它接收和返回的仿函数的类型似乎是不同的:

λ :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

— 尽管我在类型签名中声明它们应该相同!无论我用 fw 和 bw 添加什么类型的注释，它们都不想统一。

如果我从 fw 中删除类型签名，一切都会顺利进行。特别是，推断的类型签名将是:

fw :: ((a -> a) -> t) -> t

因此，forall 量词似乎破坏了一切。但我不明白为什么。它不应该意味着 “任何类型 a -> a' 都可以，包括 a -> a”？似乎相同的类型同义词 G f a 在 fw 和 bw 的类型签名中以不同的方式起作用!

这是怎么回事？

---

更多实验:

λ (fw . bw) (F 1)
...error...
λ (fw (bw (F 1)))
F 1
λ :t fw . undefined
...error...
λ :t undefined . fw
...error
λ :t bw . undefined
bw . undefined :: Functor f => a1 -> (a2 -> a') -> f a'
λ :t undefined . bw
undefined . bw :: Functor f => f a -> c

所以(正如@chi 在回答中指出的那样)fw 不能组成函数。但对于 bw 而言并非如此。为什么？

Answer 1

这是一个预测性问题。

本质上，如果我们有一个多态值 f::forall a 。 SomeTypeDependingOn a，我们在一些更大的表达式中使用它，这可以将类型 a 实例化为适合该上下文所需的任何类型 T。但是，预测性要求 T 不包含 forall。需要此限制才能进行类型推断。

在您的代码中，bw 。 fw 你使用了多态函数 . (组合)。这具有多态类型，其中一个类型变量 t 代表要组合的第二个函数的域(g in f.g) .对于 bw 。 fw 来进行类型检查，我们应该选择 t ~ G f a，但是 G f a = (forall a' . ...) 所以它违反了预测性。

通常的解决方案是使用newtype 包装器

newtype G f a = G { unG :: forall a'. (a -> a') -> f a' }

在构造函数下“隐藏”forall，以便允许使用 t ~ G f a。要使用它，需要根据需要利用同构 G 和 unG，根据需要包装和展开。这需要程序员进行额外的工作，但正是这项工作使推理算法能够完成其工作。

或者，不要使用 .，并以有针对性的风格编写函数

test :: Functor f => G f a -> G f a
test x = bw (fw x)

---

关于 bw 的类型，由 GHCi 报告:

> :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

这种类型是“forall 提升”的结果，它本质上是以这种方式“移动”全称量词:

a1 -> ... -> forall b. F b   =====>     forall b. a1 -> ... -> F b

提升是自动执行的，以帮助类型推断。

更多的是失败，我们有

bw :: forall f a . Functor f => f a -> G f a
-- by definition of G
bw :: forall f a . Functor f => f a -> (forall a'. (a -> a') -> f a')
-- after hoisting
bw :: forall f a a'. Functor f => f a -> (a -> a') -> f a'

从现在开始，当将 bw 与 bw 中的另一个函数组合时，所有量词都位于顶层。 h 或 h 。 bw，我们可以先将f, a, a'实例化为新的类型变量，然后对这些变量进行统一，以匹配h的类型。

例如，在 bw 中。 undefined 我们进行如下操作

 -- fresh variables for (.)
 (.) :: (b -> c) -> (a -> b) -> a -> c
 -- fresh variables for bw
 bw :: Functor f . f a1 -> (a1 -> a') -> f a'
 -- fresh variables for undefined
 undefined :: a2

 So we get:
 b = f a1
 c = (a1 -> a') -> f a'
 a2 = a -> b

 Hence the type of (bw . undefined) is
 a -> c
 = a -> (a1 -> a') -> f a'
 (assuming Functor f)

GHCi 同意，只是它为类型变量选择了不同的名称。当然，这个选择并不重要。

(bw . undefined) :: Functor f => a1 -> (a2 -> a') -> f a'

---

啊哈! GHCi-8.2.2 似乎存在一些 GHC 8.4.3 中不存在的问题。

-- GHCi 8.2.2
> :set -XRankNTypes
> type G f a = forall a'. (a -> a') -> f a'
> bw :: Functor f => f a -> G f a ; bw x = \f -> fmap f x
> :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

-- GHCi 8.4.3
> :set -XRankNTypes
> type G f a = forall a'. (a -> a') -> f a'
> bw :: Functor f => f a -> G f a ; bw x = \f -> fmap f x
> :t bw
bw :: Functor f => f a -> (a -> a') -> f a'