La propuesta más reciente para los tipos de Rank-N es el documento de FPH vinculado de Don. En mi opinión, también es el mejor del grupo. El objetivo principal de todos estos sistemas es requerir el menor número de anotaciones de tipo posible. El problema es que, al pasar de Hindley/Milner al Sistema F, perdemos tipos principales y la inferencia de tipos se vuelve indecidible, de ahí la necesidad de anotaciones tipo.
La idea básica del trabajo de "tipos cuadrados" es propagar anotaciones tipo en la medida de lo posible. El verificador de tipos cambia entre la verificación de tipos y el modo de inferencia de tipo y, con suerte, no se requieren más anotaciones. La desventaja aquí es que si se necesita o no una anotación de tipo es difícil de explicar porque depende de los detalles de implementación.
El sistema Remy's MLF es hasta ahora la mejor propuesta; requiere la menor cantidad de anotaciones de tipo y es estable en muchas transformaciones de código. El problema es que amplía el sistema de tipos. El siguiente ejemplo ilustra este estándar:
choose :: forall a. a -> a -> a
id :: forall b. b -> b
choose id :: forall c. (c -> c) -> (c -> c)
choose id :: (forall c. c -> c) -> (forall c. c -> c)
Tanto los tipos anteriores son admisibles en el Sistema de F. El primero es el estándar tipo Hindley/Milner y utiliza instanciación predicativo, el segundo utiliza instanciación impredicativo. Ninguno de los tipos es más general que el otro, por lo que la inferencia de tipo tendría que adivinar qué tipo desea el usuario, y esa suele ser una mala idea.
MLF en su lugar extiende el Sistema F con cuantificación limitada.El director (= más general) tipo para el ejemplo anterior sería:
choose id :: forall (a < forall b. b -> b). a -> a
usted puede leer esto como "choose id tiene el tipo a a a donde a debe ser una instancia de forall b. b -> b".
Curiosamente, esto solo no es más poderoso que el estándar Hindley/Milner. Por lo tanto, MLF también permite la cuantificación rígida. Los siguientes dos tipos son equivalentes:
(forall b. b -> b) -> (forall b. b -> b)
forall (a = forall b. b -> b). a -> a
cuantificación rígido se introduce mediante anotaciones de tipo y los detalles técnicos son de hecho bastante complicado. Lo bueno es que MLF solo necesita muy pocas anotaciones de tipo y hay una regla simple para cuando se necesitan. Las desventajas son:
tipos pueden llegar a ser más difícil de leer, ya que el lado derecho de '<' puede contener cuantificaciones más anidados.
Hasta hace poco tiempo no existía una variante explícitamente tipada de MLF. Esto es importante para las transformaciones del compilador tipadas (como hace GHC). La Parte 3 de Boris Yakobowski's PhD thesis tiene un primer intento de tal variante. (Partes 1 & 2 también son interesantes, describen una representación más intuitiva de la FML a través de "Tipos de gráficos".)
Volviendo a FPH, la idea básica es utilizar técnicas de FML internamente, sino que requieren Tipo anotaciones en enlaces let. Si solo desea el tipo de Hindley/Milner, entonces no es necesario anotar. Si desea un tipo de rango superior, debe especificar el tipo solicitado, pero solo en el enlace let (o nivel superior).
FPH (como MLF) admite la creación de instancias impredicativas, por lo que no creo que su problema se aplique. Por lo tanto, no debería tener problemas al escribir su expresión f . g arriba. Sin embargo, FPH aún no se ha implementado en GHC y lo más probable es que no lo sea. Las dificultades provienen de la interacción con coerciones de igualdad (y posiblemente con restricciones de clase de tipo). No estoy seguro de cuál es el estado más reciente, pero escuché que SPJ quiere alejarse de la impredicatividad. Todo ese poder expresivo tiene un costo, y hasta ahora no se ha encontrado una solución asequible y que lo acompañe todo.
¿Cómo se puede hacer que los tipos de (runST. Forever) funcionen? – Peaker