为什么这种类型注释是错误的？

Question

为什么这种类型注释是错误的？

haskelltypescategory-theoryisomorphismhigher-rank-types

3

我尝试按照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并非如此。为什么？

- Ignat Insarov

这对我来说看起来像是一个（糟糕的）bug。 - Daniel Wagner

:type 不是很准确，特别是对于函数。也许有一个错误正在干扰 bw 的签名。尝试使用 :type +v bw。 - HTNW

我得到了 bw :: Functor f => f a -> (a -> a') -> f a'。你是如何得到上面的 f1 和 f2 的？ - chi

2个回答

0

forall量词使您的类型接受所有a -> a'，但在fw中实际需要的是限制，确保参数类型和返回类型相同，这就是签名a -> a的含义。

因此，是的，forall版本接受函数a -> a，但它不仅接受这样的函数。如上所述，编译器告诉您fw应该仅接受类型为a -> a的函数。

- Ruifeng Xie

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- chi · Accepted Answer

这是一个预测性问题。

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

为了进行类型推断，需要此限制。

在您的代码中，bw . fw 使用了多态函数 .（组合）。这具有多态类型，其中一个类型变量 t 代表要组合的第二个函数的定义域（f . g 中的 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)

关于GHCi报告的bw类型：

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

这种类型是由于“forall提升”而产生的结果，本质上是通过以下方式“移动”全称量词：

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

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

更详细地说，我们有：

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'