¿Qué usos ha encontrado para los tipos de rango superior en Haskell?

Question

Los tipos de rango superior parecen muy divertidos. Desde el Haskell wikibook viene este ejemplo:

foo :: (forall a. a -> a) -> (Char,Bool) 
foo f = (f 'c', f True) 

Ahora podemos evaluar foo id sin el compilador de la explosión. Este ejemplo se sigue rápidamente en el libro por el ejemplo del mundo real que he visto en algunos otros lugares: la mónada ST y runST. Eso es muy bonito.

Pero todavía tengo que encontrarme con una situación en la que resuelvo un problema escribiendo mi propia función con un argumento de mayor rango. ¿Tienes? ¿Qué ejemplos tienes de polimorfismo de rango 2 o rango n en la naturaleza?

Answer 1

Eche un vistazo a funciones como withRepoLock en el Darcs source.

Darcs tiene soporte para múltiples formatos de repositorio, y esa compatibilidad se expresa a través de una clase de tipo. Entonces puede escribir código genérico sobre formatos de repositorio. Al leer realmente un repositorio en disco que desea enviar a ese código a través de un código común que averigua en qué formato se encuentra el repositorio y elige la instanciación de clase de clase correcta.

Answer 2

Recientemente alguien asked a question here on Stack Overflow que podría ser resuelto con tipos de rango superior.

Otra aplicación se encuentra en el documento Scrap Your Boilerplate.

Answer 3

Puede ser que haya encontrado problemas en los que los tipos de mayor clasificación serían útiles, pero no se dieron cuenta. Por ejemplo, en el ejemplo de Darcs podrían haberlo implementado fácilmente sin tipos de clasificación superior. En su lugar, habría precondiciones sobre algunas funciones que la persona que llama debería asegurarse de cumplir, como elegir la instanciación correcta de una función para el formato del repositorio.

La ventaja del tipo de mayor clasificación es que transfiere la responsabilidad de obtener este derecho desde el programador hasta el compilador. Con el enfoque convencional, si un desarrollador de Darcs cometió un error con el tipo de repositorio, el resultado sería un error en tiempo de ejecución o datos dañados. Con el tipo de mayor clasificación, el desarrollador obtiene un error de tipo en tiempo de compilación.

Answer 4

Weirich and Washburnn's "Boxes go Bananas"! (paper, slides)

Aquí es una explicación muy crudo y probablemente un poco inexacta de lo que se trata todo esto: dado un tipo inductivo, BGB permite representar el espacio de las funciones de ese tipo que son "positivos" - que nunca distinga entre mayúsculas y minúsculas en sus argumentos. A lo sumo incluyen sus argumentos como parte de otros valores (generalmente del mismo tipo).

Weirich + Washburn usa esto para obtener una representación delHOAS del cálculo lambda en -XRankNTypes Haskell (¿Alguien ha demostrado que es adecuado?).

lo uso here (advertencia: código desordenado) para encender un

(forall g . GArrow g => g() x -> g() y) 

en un

(forall g . GArrow g => g x y) 

Esto funciona porque el tipo polimórfico rango-2 no puede "inspeccionar" la estructura de su argumento: todo lo que puede hacer es "pegar" ese argumento en estructuras más grandes.Algunos trucos me permiten averiguar dónde ocurre la pegadura, y luego enhebrar los puntos de pegado (si los hay) de vuelta a la entrada del GArrow.

No puede hacer esto con la clase Control.Arrow, porque todo el espacio de funciones Haskell "se filtra" a través de arr.