27

我已经看到了一些 rank-2 多态性的用例（最突出的例子是ST monad），但没有一个比这更高的用例。有谁知道这样的用例？

4

2 回答 2

30

我也许能帮上忙，尽管这样的野兽不可避免地有点牵涉其中。这是我有时用于开发具有绑定和 de Bruijn 索引（瓶装）的范围良好的语法的模式。

mkRenSub ::
  forall v t x y.                      -- variables represented by v, terms by t
    (forall x. v x -> t x) ->            -- how to embed variables into terms
    (forall x. v x -> v (Maybe x)) ->    -- how to shift variables
    (forall i x y.                       -- for thingies, i, how to traverse terms...
      (forall z. v z -> i z) ->              -- how to make a thingy from a variable
      (forall z. i z -> t z) ->              -- how to make a term from a thingy
      (forall z. i z -> i (Maybe z)) ->      -- how to weaken a thingy
      (v x -> i y) ->                    -- ...turning variables into thingies
      t x -> t y) ->                     -- wherever they appear
    ((v x -> v y) -> t x -> t y, (v x -> t y) -> t x -> t y)
                                                 -- acquire renaming and substitution
mkRenSub var weak mangle = (ren, sub) where
  ren = mangle id var weak         -- take thingies to be vars to get renaming
  sub = mangle var id (ren weak)   -- take thingies to be terms to get substitution

通常，我会使用类型类来隐藏最糟糕的部分，但如果你打开字典，你会发现这是什么。

关键是这mangle是一个 rank-2 操作，它采用了一个概念，即 thingy 在它们工作的变量集中配备了合适的多态操作：将变量映射到 thingies 的操作变成了术语转换器。整件事展示了如何使用mangle来生成重命名和替换。

这是该模式的一个具体实例：

data Id x = Id x

data Tm x
  = Var (Id x)
  | App (Tm x) (Tm x)
  | Lam (Tm (Maybe x))

tmMangle :: forall i x y.
             (forall z. Id z -> i z) ->
             (forall z. i z -> Tm z) ->
             (forall z. i z -> i (Maybe z)) ->
             (Id x -> i y) -> Tm x -> Tm y
tmMangle v t w f (Var i) = t (f i)
tmMangle v t w f (App m n) = App (tmMangle v t w f m) (tmMangle v t w f n)
tmMangle v t w f (Lam m) = Lam (tmMangle v t w g m) where
  g (Id Nothing) = v (Id Nothing)
  g (Id (Just x)) = w (f (Id x))

subst :: (Id x -> Tm y) -> Tm x -> Tm y
subst = snd (mkRenSub Var (\ (Id x) -> Id (Just x)) tmMangle)

我们只实现了一次术语遍历，但是以一种非常通用的方式，然后我们通过部署 mkRenSub 模式（它以两种不同的方式使用通用遍历）来获得替换。

再举一个例子，考虑类型运算符之间的多态操作

type (f :-> g) = forall x. f x -> g x

（IMonad索引单子）是一些m :: (* -> *) -> * -> *配备多态运算符的

ireturn :: forall p. p :-> m p
iextend :: forall p q. (p :-> m q) -> m p :-> m q

所以这些操作是 2 级的。

现在，由任意索引单子参数化的任何操作都是等级 3。因此，例如，构造通常的单子组合，

compose :: forall m p q r. IMonad m => (q :-> m r) -> (p :-> m q) -> p :-> m r
compose qr pq = iextend qr . pq

一旦你解包IMonad.

故事的寓意：一旦你对多态/索引概念进行高阶编程，你的有用工具包的字典就会成为第 2 级，而你的通用程序会成为第 3 级。当然，这可能会再次发生升级。

于 2011-12-06T21:10:18.573 回答
9

也许是我读过的摘要的最佳结尾：“除了 Haskell 的正常类型类机制之外，Multiplate 只需要 3 级多态性。” . （哦，只有三阶多态，没什么大不了的！）

于 2011-12-07T01:08:43.793 回答