3 级（或更高）多态性的用例？

发布于 2024-12-19 23:51:39 字数 150 浏览 0 评论 0原文

我见过一些 2 级多态性的用例（最突出的例子是 ST monad< /a>），但没有一个比这更高的等级。有谁知道这样的用例？

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

静水深流 2024-12-26 23:51:39

我也许能帮上忙，尽管这样的野兽不可避免地会受到牵连。这是我有时在开发带有绑定和 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 是一个 2 级操作，它采用在其工作的变量集中配备适当多态操作的事物概念：将变量映射到事物的操作被转换为术语转换器。整个事情展示了如何使用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

依赖于等级 3 量化，一旦你解压 IMonad 的定义。

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

I may be able to help, although such beast are inevitably a bit involved. Here's a pattern I sometimes use in developing well-scoped syntax with binding and de Bruijn indexing, bottled.

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

Normally, I'd use type classes to hide the worst of the gore, but if you unpack the dictionaries, this is what you'll find.

The point is that mangle is a rank-2 operation which takes a notion of thingy equipped with suitable operations polymorphic in the variable sets over which they work: operations which map variables to thingies get turned into term-transformers. The whole thing shows how to use mangle to generate both renaming and substitution.

Here's a concrete instance of that pattern:

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)

We implement the term traversal just once, but in a very general way, then we get substitution by deploying the mkRenSub pattern (which uses the general traversal in two different ways).

For another example, consider polymorphic operations between type operators

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

An IMonad (indexed monad) is some m :: (* -> *) -> * -> * equipped with polymorphic operators

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

so those operations are rank 2.

Now any operation which is parametrized by an arbitrary indexed monad is rank 3. So, for example, constructing the usual monadic composition,

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

relies on rank 3 quantification, once you unpack the definition of IMonad.

Moral of story: once you're doing higher order programming over polymorphic/indexed notions, your dictionaries of useful kit become rank 2, and your generic programs become rank 3. This is, of course, an escalation that can happen again.

回复收藏 0 原文