Rank 2多态性的实际应用？

Question

我正在覆盖多态性,我试图看到这种功能的实际用途.

我对Rank 2的基本了解是:

type MyType = ? a. a -> a

subFunction :: a -> a
subFunction el = el

mainFunction :: MyType -> Int
mainFunction func = func 3

我知道这允许用户在mainFunction中使用多态函数(subFunction)并严格指定它的输出(Int).这似乎与GADT非常相似:

data Example a where
 ExampleInt :: Int -> Example Int
 ExampleBool :: Bool -> Example Bool

1)鉴于以上情况,我对Rank 2多态性的理解是否正确？

2)与GADT相比,可以使用Rank 2多态性的一般情况是什么？

Answer 1

如果将多态函数作为参数传递给Rank2多态函数,那么实际上您不仅要传递一个函数,而且传递整个函数族 - 对于满足约束的所有可能类型.

通常,这些forall量词具有类约束.例如,我可能希望同时使用两种不同的类型进行数字运算(用于比较精度或其他).

data FloatCompare = FloatCompare {
     singlePrecision :: Float
   , doublePrecision :: Double
   }

现在我可能想通过一些数学运算来修改这些数字.就像是

modifyFloat :: (Num -> Num) -> FloatCompare -> FloatCompare

但Num不是类型,只是类型类.当然,我可以通过将修改任何一个功能特定号码类型,但我不能用它来修改既一个Float和Double值,至少在没有一些难看(以及可能有损)来回转换.

解决方案:Rank-2多态性!

modifyFloat :: (? n . Num n => n -> n) -> FloatCompare -> FloatCompare
mofidyFloat f (FloatCompare single double)
    = FloatCompare (f single) (f double)

这在实践中如何有用的最好的单一例子可能是镜头.镜头是某些较大数据结构中的字段的"智能访问器功能".它允许您访问字段,更新它们,收集结果......同时以非常简单的方式编写.工作原理:Rank2-polymorphism; 每个镜头都是多态的,不同的实例分别对应于"getter"/"setter"方面.

Answer 2

Rank-2 类型应用的首选示例是runSTBenjamin Hodgson 在评论中提到的。这是一个相当好的示例，并且有多种使用相同技巧的示例。例如，品牌化以维护跨多种类型的抽象数据类型不变量，避免了ad（ST 的基于区域的版本）中差异的混淆。

但我实际上想谈谈 Haskell 程序员如何一直隐式使用 2 级类型。每个其方法具有通用量化类型的类型类都会脱糖为具有 2 级类型字段的字典。实际上，这实际上总是一个更高级的类型类^*，如Functoror Monad。我将使用 的简化版本Alternative作为示例。类声明是：

class Alternative f where
    empty :: f a
    (<|>) :: f a -> f a -> f a

代表这个类的字典是：

data AlternativeDict f = AlternativeDict {
    empty :: forall a. f a,
    (<|>) :: forall a. f a -> f a -> f a }

有时这样的编码很好，因为它允许人们对同一类型使用不同的“实例”，也许只是在本地。例如，Maybe有两个明显的实例Alternative取决于Just a <|> Just bisJust a或Just b。没有类型类的语言，例如 Scala，确实使用这种编码。

要连接到 leftaroundabout 对Lens的引用，您可以将那里的层次结构视为类型类的层次结构，并将 Lens 组合器视为用于显式构建相关类型类字典的简单工具。当然，它实际上不是类型类的层次结构的原因是我们通常会有同一类型的多个“实例”。例如_head和_head . _tail都是的“实例” Traversal' s a。

^*较高种类的类型类不一定会导致这种情况，并且它可能发生在 kind 的类型类上*。例如：

-- Higher-kinded but doesn't require universal quantification.
class Sum c where
    sum :: c Int -> Int

-- Not higher-kinded but does require universal quantification.
class Length l where
    length :: [a] -> l