【问题标题】：Flipping with rank-N types使用 rank-N 类型翻转
【发布时间】：2021-11-01 11:22:45
【问题描述】：

我有以下 Rank 2 功能：

polyOn :: (f a -> f b -> c) -> (forall k . k -> f k) -> a -> b -> c
polyOn bifunc func x y =
  bifunc (func x) (func y)

我想翻一下

flippedPolyOn :: (forall k . k -> f k) -> (f a -> f b -> c) -> a -> b -> c
flippedPolyOn =
  flip polyOn

但 ghc 抱怨：

    • Couldn't match type ‘k0 -> f k0’ with ‘forall k. k -> f k’
      Expected type: (f a -> f b -> c) -> (k0 -> f k0) -> a -> b -> c
        Actual type: (f a -> f b -> c)
                     -> (forall k. k -> f k) -> a -> b -> c
    • In the first argument of ‘flip’, namely ‘polyOn’
      In the expression: flip polyOn
      In an equation for ‘flippedPolyOn’: flippedPolyOn = flip polyOn
    • Relevant bindings include
        flippedPolyOn :: (forall k. k -> f k) -> (f a -> f b -> c) -> a -> b -> c
          (bound at XXXXXX:75:1)
   |
76 |   flip polyOn
   |        ^^^^^^

所以看起来 ghc 在某些时候将forall k. k -> f k 专门化为k 的特定值（它称之为k0）。

为什么 ghc 会这样做？这种专业化可以避免吗？

【问题讨论】：

标签： haskell higher-order-functions higher-rank-types

【解决方案1】：

GHC

问题是 GHC

flip :: (a0->b0->c0) -> b0->a0->c0

这样：

a0 ~ (f a -> f b -> c)
b0 ~ (forall k . k -> f k)
c0 ~ a -> b -> c

类型推断与a0 和c0 没有问题，但不允许以这种方式选择b0。实际上，在不支持隐含多态性的情况下，像b0 这样的类型变量只能用单型（没有foralls 的类型）来实例化。

我们需要内联flip 来完成这项工作

flippedPolyOn x y = polyOn y x

GHC >= 9

默认情况下，在 GHC 9 中，我们仍然会收到类型错误，但有更好的错误消息，指出了不可预测性问题：

  Cannot instantiate unification variable `b0'
  with a type involving polytypes: forall k. k -> f k

我们可以通过打开禁言类型来对您的代码进行类型检查：

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

【讨论】：