¿Caso de uso para el polimorfismo de rango 3 (o superior)?

Question

He visto algunos casos de uso para el polimorfismo de rango 2 (el ejemplo más destacado es el ST monad), pero ninguno para un rango superior. ¿Alguien sabe de ese caso de uso?

Answer 1

Es posible que pueda ayudar, aunque estas bestias están inevitablemente un poco involucradas. Aquí hay un patrón que a veces uso para desarrollar una sintaxis bien definida con indexación de binding e de Bruijn, embotellada.

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 

Normalmente, usaría el tipo clases de ocultar lo peor de la sangre derramada, pero si desembalar los diccionarios, esto es lo que encontrará.

El punto es que mangle es una operación de rango 2 que tiene una noción de cosa equipada con operaciones adecuadas polimórficas en los conjuntos de variables sobre las que trabajan: operaciones que asignan variables a objetos se convierten en transformadores de términos. Todo muestra cómo usar mangle para generar tanto el cambio de nombre como la sustitución.

Aquí está un ejemplo concreto de ese patrón:

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) 

ponemos en práctica el término de recorrido de una sola vez, pero de una manera muy general, entonces tenemos la sustitución mediante la implementación del patrón de mkRenSub (que utiliza el recorrido general dos formas diferentes).

Para otro ejemplo, considere operaciones polimórficas entre los operadores de tipo

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

Un IMonad (mónada indexado) es un poco de m :: (* -> *) -> * -> * equipado con operadores polimórficas

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

por lo que esas operaciones son rango 2.

Ahora cualquier operación que esté parametrizada por una mónada indexada arbitraria es el rango 3. Entonces, para ejemplo, la construcción de la composición habitual monádico,

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

se basa en la cuantificación rango 3, una vez que desempaquetar la definición de IMonad.

Moraleja de la historia: una vez que estás haciendo una programación de orden superior sobre nociones polimórficas/indexadas, tus diccionarios de kit útil se convierten en rango 2 y tus programas genéricos se convierten en rango 3. Esto es, por supuesto, una escalada que puede ocurrir de nuevo.

Answer 2

Quizás el mejor final para un resumen que leí aún: "Multiplate only requires rank 3 polymorphism in addition to the normal type class mechanism of Haskell.". (¡Oh, solo polimorfismo de rango 3, no es gran cosa!)