使用 rank-N 类型进行翻转

Question

我有以下 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 为什么要这样做？这种专业化是可以避免的吗？

Answer 1

GHC < 9

问题是 GHC < 9.x 不支持谓词多态性。本质上，你要做的是实例化

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 #-}

使用 rank-N 类型进行翻转

Flipping with rank-N types

haskell

higher-order-functions

higher-rank-types

GHC < 9

GHC >= 9