多态类型中的包容性

Question

多态类型中的包容性

31

在‘Practical type inference for arbitrary-rank types’一文中，作者谈到了包容性（subsumption）：

3.3 Subsumption

我在阅读时尝试在GHCi中测试事物，但即使g k2应该可以通过类型检查，在我使用GHC 7.8.3时却不能：

λ> :set -XRankNTypes
λ> let g :: ((forall b. [b] -> [b]) -> Int) -> Int; g = undefined
λ> let k1 :: (forall a. a -> a) -> Int; k1 = undefined
λ> let k2 :: ([Int] -> [Int]) -> Int; k2 = undefined
λ> :t g k1

<interactive>:1:3: Warning:
    Couldn't match type ‘a’ with ‘[a]’
      ‘a’ is a rigid type variable bound by
          the type forall a1. a1 -> a1 at <interactive>:1:3
    Expected type: (forall b. [b] -> [b]) -> Int
      Actual type: (forall a. a -> a) -> Int
    In the first argument of ‘g’, namely ‘k1’
    In the expression: g k1
g k1 :: Int
λ> :t g k2

<interactive>:1:3: Warning:
    Couldn't match type ‘[Int] -> [Int]’ with ‘forall b. [b] -> [b]’
    Expected type: (forall b. [b] -> [b]) -> Int
      Actual type: ([Int] -> [Int]) -> Int
    In the first argument of ‘g’, namely ‘k2’
    In the expression: g k2
g k2 :: Int

我还没有真正理解这篇论文，但我担心自己可能误解了一些内容。这个类型检查是否正确？我的Haskell类型是否有误？

- beta

1个回答

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

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

- Cirdec · Accepted Answer

类型检查器不知道何时应用包容规则。

您可以使用以下函数告诉它何时应用。

Prelude> let u :: ((f a -> f a) -> c) -> ((forall b. f b -> f b) -> c); u f n = f n

这段话的意思是，给定一个特定类型的转换函数，我们可以从自然变换中创建一个函数 forall b. f b -> f b。

然后我们可以在第二个例子中成功尝试它。

Prelude> :t g (u k2)
g (u k2) :: Int

第一个示例现在还提供了更详细的错误信息。

Prelude> :t g (u k1)
    Couldn't match type `forall a. a -> a' with `[a0] -> [a0]'
    Expected type: ([a0] -> [a0]) -> Int
      Actual type: (forall a. a -> a) -> Int
    In the first argument of `u', namely `k1'
    In the first argument of `g', namely `(u k1)'

我不知道我们是否能够编写一个更通用的版本u; 我们需要一个限制级别的不太多态的概念，才能编写类似let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x这样的东西。