¿Es útil el polimorfismo paramétrico de rango superior?

Estoy bastante seguro de que todos están familiarizados con los métodos genéricos del formulario:

T DoSomething<T>(T item)

Esta función también se llama paramétricamente polimórfica (PP), específicamente rango-1 PP.

Digamos que este método se puede representar usando un objeto de función de la forma:

<T> : T -> T

Es decir, <T>significa que toma un parámetro de tipo y T -> Tsignifica que toma un parámetro de tipo Ty devuelve un valor del mismo tipo.

Entonces lo siguiente sería una función PP de rango 2:

(<T> : T -> T) -> int 

La función no toma parámetros de tipo en sí, pero toma una función que toma un parámetro de tipo. Puede continuar esto iterativamente, haciendo que el anidamiento sea cada vez más profundo, obteniendo PP de rango cada vez más alto.

Esta característica es realmente rara entre los lenguajes de programación. Incluso Haskell no lo permite por defecto.

¿Es útil? ¿Puede describir comportamientos que son difíciles de describir de otra manera?

Además, ¿qué significa que algo sea impredecible ? (en este contexto)

En general, utiliza un polimorfismo de rango superior cuando desea que la persona que llama pueda seleccionar el valor de un parámetro de tipo, en lugar de la persona que llama . Por ejemplo:

f :: (forall a. Show a => a -> Int) -> (Int, Int)
f g = (g "one", g 2)

Cualquier función gque le pase a esto fdebe poder darme un Intvalor de algún tipo, donde lo único que se gsabe sobre ese tipo es que tiene una instancia de Show. Entonces estos son kosher:

f (length . show)
f (const 42)

Pero estos no son:

f length
f succ

Una aplicación particularmente útil es usar el alcance de tipos para aplicar el alcance de los valores . Supongamos que tenemos un objeto de tipo Action<T>, que representa una acción que podemos ejecutar para producir un resultado de tipo T, como un futuro o una devolución de llamada.

T runAction<T>(Action<T>)

runAction :: forall a. Action a -> a

Ahora, supongamos que también tenemos un Actionque puede asignar Resource<T>objetos:

Action<Resource<T>> newResource<T>(T)

newResource :: forall a. a -> Action (Resource a)

Queremos asegurar que esos recursos solo se usen dentro del lugar Actiondonde se crearon, y no se compartan entre diferentes acciones o diferentes ejecuciones de la misma acción, de modo que las acciones sean deterministas y repetibles.

Podemos utilizar tipos de mayor rango para lograr esto agregando un parámetro Sa los tipos Resourcey Action, que es totalmente abstracto: representa el "alcance" de Action. Ahora nuestras firmas son:

T run<T>(<S> Action<S, T>)
Action<S, Resource<S, T>> newResource<T>(T)

runAction :: forall a. (forall s. Action s a) -> a
newResource :: forall s a. a -> Action s (Resource s a)

Ahora, cuando damos runActionun Action<S, T>, estamos seguros de que debido a que el parámetro "alcance" Ses completamente polimórfico, no puede escapar del cuerpo de runAction, por lo tanto , ¡cualquier valor de un tipo que se utiliza Scomo Resource<S, int>tampoco puede escapar!

(En Haskell, esto se conoce como la STmónada, donde runActionse llama runST, Resourcese llama STRefy newResourcese llama newSTRef).

El polimorfismo de rango superior es extremadamente útil. En el Sistema F (el idioma central de los lenguajes de FP mecanografiados con los que está familiarizado), esto es esencial para admitir las "codificaciones de la Iglesia mecanografiadas", que en realidad es la forma en que el Sistema F programa. Sin estos, el sistema F es completamente inútil.

En el Sistema F, definimos los números como

Nat = forall c. (c -> c) -> c -> c

La adición tiene el tipo

plus : Nat -> Nat -> Nat
plus l r = Λ t. λ (s : t -> t). λ (z : t). l s (r s z)

que es un tipo de rango más alto ( forall c.aparece dentro de esas flechas).

Esto surge en otros lugares también. Por ejemplo, si desea indicar que un cálculo es un estilo de paso de continuación adecuado ("codensity haskell" de Google), entonces debe corregir esto como

type CPSed A = forall c. (A -> c) -> c

Incluso hablar de un tipo deshabitado en el Sistema F requiere un polimorfismo de rango superior

type Void = forall a. a 

En resumidas cuentas, escribir una función en un sistema de tipo puro (Sistema F, CoC) requiere un polimorfismo de rango superior si queremos tratar con datos interesantes.

En el Sistema F en particular, estas codificaciones deben ser "impredecibles". Esto significa que a forall a.cuantifica absolutamente todos los tipos . Esto incluye críticamente el mismo tipo que estamos definiendo. En forall a. aeso en arealidad podría significar de forall a. anuevo! En lenguajes como ML este no es el caso, se dice que son "predicativos" ya que una variable de tipo cuantifica solo sobre el conjunto de tipos sin cuantificadores (llamados monotipos). Nuestra definición de plusimpredicativity requerida, así porque la instancia cen l : Natque ser Nat!

Finalmente, me gustaría mencionar una última razón en la que le gustaría tanto la impredicatividad como el polimorfismo de rango superior incluso en un lenguaje con tipos arbitrariamente recursivos (a diferencia del Sistema F). En Haskell, hay una mónada para los efectos llamada "mónada de hilos de estado". La idea es que la mónada de subprocesos de estado le permite mutar cosas, pero requiere escapar para que su resultado no dependa de nada mutable. Esto significa que los cálculos de ST son observablemente puros. Para hacer cumplir este requisito, utilizamos polimorfismo de rango superior

runST :: forall a. (forall s. ST s a) -> a

Aquí, al asegurarnos de que aestá fuera del alcance donde presentamos s, sabemos que arepresenta un tipo bien formado que no depende s. ¡Usamos sparameritizar todas las cosas mutables en ese hilo de estado particular para que sepamos que aes independiente de las cosas mutables y, por lo tanto, que nada escapa al alcance de ese STcálculo! Un maravilloso ejemplo del uso de tipos para descartar programas mal formados.

Por cierto, si está interesado en aprender sobre la teoría de tipos, le sugiero que invierta en un buen libro o dos. Es difícil aprender estas cosas en pedazos. Sugeriría uno de los libros de Pierce o Harper sobre teoría PL en general (y algunos elementos de la teoría de tipos). El libro "Temas avanzados en tipos y lenguajes de programación" también cubre una buena cantidad de teoría de tipos. Finalmente, "Programación en la teoría de tipos de Martin Lof" es una muy buena exposición de la teoría de tipos intensiva que Martin Lof describió.