时间戳

首页 > 解决方案 > 为什么这种类型注释是错误的？

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

问题描述

我试图按照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

它编译得很好。（使用ghc8.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”？似乎相同的类型同义词在andG f a的类型签名中以不同的方式起作用！fwbw

这里发生了什么？

更多实验：

λ (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. 为什么？

标签： haskelltypescategory-theoryisomorphismhigher-rank-types

解决方案

这是一个预测性问题。

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

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

GHCi 报告的关于 的类型bw：

> :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'

推荐阅读