haskell - herencia - polimorfismo java pdf

¿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 la mónada ST ), pero ninguno para un rango más alto que ese. ¿Alguien sabe de tal caso de uso?

Answer 1

Tal vez el mejor final de un resumen que haya leído hasta ahora: "Multiplate solo requiere polimorfismo de rango 3 además del mecanismo de clase de tipo normal de Haskell". . (Oh, solo el polimorfismo de rango 3, no es gran cosa!)

Answer 2

Tal vez pueda ayudar, aunque tal bestia está inevitablemente un poco involucrada. Aquí hay un patrón que a veces utilizo para desarrollar una sintaxis de ámbito bien con vinculación e indexación 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 clases de tipo para ocultar lo peor del gore, pero si desempaqueta los diccionarios, esto es lo que encontrará.

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

Aquí hay una instancia concreta 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)

Implementamos el término recorrido solo una vez, pero de una manera muy general, luego obtenemos la sustitución al implementar el patrón mkRenSub (que utiliza el recorrido general de dos maneras diferentes).

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

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

Una IMonad (mónada indexada) es algunos m :: (* -> *) -> * -> * equipado con operadores polimórficos

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

por lo que esas operaciones son de rango 2.

Ahora, cualquier operación que está parametrizada por una mónada indexada arbitraria está en el rango 3. Así, por ejemplo, construyendo la composición monádica habitual,

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 de rango 3, una vez que descomprime la definición de IMonad .

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