Cas d'utilisation pour le polymorphisme du rang-3 (ou plus)?

Question

J'ai vu quelques cas d'utilisation pour le polymorphisme du rang 2 (l'exemple le plus important étant le St Monad), mais aucun pour un rang plus élevé que cela. Quelqu'un connaît-il un tel cas d'utilisation?

Answer 1

Je pourrai peut-être aider, bien que une telle bête soit inévitablement un peu impliquée. Voici un modèle que j'utilise parfois dans le développement de la syntaxe bien sommée avec la liaison et l'indexation de Bruijn, en bouteille.

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

Normalement, j'utiliserais des classes de type pour cacher le pire du Gore, mais si vous déballez les dictionnaires, c'est ce que vous trouverez.

Le fait est que mangle est une opération de Rank-2 qui prend une notion de chose équipée d'opérations appropriées polymorphes dans les ensembles variables sur lesquels ils fonctionnent: les opérations qui mappent les variables en choses sont transformées en transformateurs à terme. Le tout montre comment utiliser mangle pour générer à la fois le changement de nom et la substitution.

Voici une instance concrète de ce modèle:

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)

Nous mettons en œuvre le terme traversant une seule fois, mais de manière très générale, nous obtenons ensuite la substitution en déploiement du modèle MKRENSUB (qui utilise la traversée générale de deux manières différentes).

Pour un autre exemple, considérez les opérations polymorphes entre les opérateurs de type

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

Un IMonad (Monad indexé) est certains m :: (* -> *) -> * -> * équipé d'opérateurs polymorphes

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

Ces opérations sont donc le rang 2.

Maintenant, toute opération paramétrée par une monade indexée arbitraire est le rang 3. Ainsi, par exemple, la construction de la composition monadique habituelle,

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

repose sur la quantification du rang 3, une fois que vous avez déballé la définition de IMonad.

Morale de l'histoire: une fois que vous effectuez une programmation d'ordre supérieur sur des notions polymorphes / indexées, vos dictionnaires de kit utile deviennent le rang 2, et vos programmes génériques deviennent le rang 3. C'est, bien sûr, une escalade qui peut se reproduire.

Answer 2

Peut-être la meilleure fin à un résumé que j'ai encore lu: "Multiplate ne nécessite que le polymorphisme de rang 3 en plus du mécanisme de classe de type normal de Haskell.". (Oh, seulement le polymorphisme du rang-3, pas grave!)