Como indica el título de la pregunta, quiero saber qué es el polimorfismo Levity y cuál es su motivación. Sé que esta página tiene algunos detalles, pero la mayoría de las explicaciones allí se me pasan por alto. :)
Si bien esta página es un poco más amigable, todavía no puedo entender la motivación detrás de ella.
Nota: Esta respuesta se basa en observaciones muy recientes sobre las discusiones de Levity. Todo lo relacionado con el polimorfismo Levity actualmente solo se implementa en las versiones candidatas de GHC 8.0 y, como tal, está sujeto a cambios (consulte el número 11471, por ejemplo).
TL; DR : Es una forma de hacer que las funciones sean polimórficas sobre tipos elevados y no elevados, lo cual no es posible con funciones regulares. Por ejemplo, el siguiente código no escribe check con polimorfismos regulares, ya que Int#tiene tipo #, pero las variables de tipo en idtienen tipo *:
{-# LANGUAGE MagicHash #-}
import GHC.Prim
example :: Int# -> Int#
example = id -- does not work, since id :: a -> a
Couldn't match kind ‘*’ with ‘#’
When matching types
a0 :: *
Int# :: #
Expected type: Int# -> Int#
Actual type: a0 -> a0
In the expression: id
Tenga en cuenta que (->)todavía usa algo de magia.
Antes de empezar a responder a esta pregunta, vamos a echar un paso atrás y nos vamos a una de las funciones más utilizadas, ($).
¿Qué es ($)el tipo? Bueno, según Hackage y el informe, es
($) :: (a -> b) -> a -> b
Sin embargo, eso no está completo al 100%. Es una mentira conveniente. El problema es que los tipos polimórficos (como ay b) tienen especie *. Sin embargo, los desarrolladores de (bibliotecas) querían usar ($)no solo para tipos con kind *, sino también para los de kind #, por ejemplo
unwrapInt :: Int -> Int#
Mientras Inttiene clase *(puede ser inferior), Int#tiene clase #(y no puede ser inferior en absoluto). Aún así, el siguiente tipo de código verifica:
unwrapInt $ 42
Eso no debería funcionar. ¿Recuerda el tipo de devolución de ($)? Era polimórfico, y los tipos polimórficos tienen tipo *, #¡ no ! Entonces, ¿por qué funcionó? Primero, fue un error , y luego fue un truco (extracto de un correo de Ryan Scott en la lista de correo ghc-dev):
Entonces, ¿por qué sucede esto?
La respuesta larga es que antes de GHC 8.0, en la firma de tipo
($) :: (a -> b) -> a -> b, enbrealidad no estaba en especie*, sino más bienOpenKind.OpenKindes un truco horrible que permite que tanto los tipos levantados (tipo*) como los no levantados (tipo#) lo habiten, por lo que(unwrapInt $ 42)typechecks.
Entonces, ¿cuál es ($)el nuevo tipo de GHC 8.0? Sus
($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b
-- will likely change according to Richard E.
Para entenderlo debemos fijarnos en Levity:
data Levity = Lifted | Unlifted
Ahora, podemos pensar ($)en uno de los siguientes tipos, ya que solo hay dos opciones de w:
-- pseudo types
($) :: forall a (b :: TYPE Lifted). (a -> b) -> a -> b
($) :: forall a (b :: TYPE Unlifted). (a -> b) -> a -> b
TYPEes una constante mágica, y redefine los tipos *y #como
type * = TYPE Lifted
type # = TYPE Unlifted
La cuantificación de tipos también es bastante nueva y forma parte de la integración de tipos dependientes en Haskell .
El nombre de polimorfismo Levity proviene del hecho de que ahora puede escribir funciones polimórficas sobre tipos elevados y no elevados, algo que no estaba permitido / era posible con las restricciones de polimorfismo anteriores. También se deshace del OpenKindhack al mismo tiempo. Es realmente "solo" sobre esto, manejando ambos tipos de tipos.
Por cierto, no estás solo con tu pregunta. Incluso Simon Peyton Jones dijo que se necesita una página wiki de Levity , y Richard E. (el implementador actual de esto) declaró que la página wiki necesita una actualización sobre el proceso actual.
GHC.Types, parte de la ghc-primbiblioteca que se envía con GHC.
($) :: forall (w1 w2 :: Levity) (a :: TYPE w1) (b :: TYPE w2). (a -> b) -> a -> blo es, es decir, por qué($)no se supone que se pueda utilizar con funciones con argumentos no elevados?RuntimeRep(reemplazaLevity).