haskell - uruguay - summit trampoline park
¿Qué es el polimorfismo de gravedad? (1)
Nota: Esta respuesta se basa en observaciones muy recientes sobre discusiones de Levity. Actualmente, todo lo relacionado con el polimorfismo de Levity solo se implementa en los candidatos a la versión GHC 8.0 y, como tal, está sujeto a cambios (ver #11471 por ejemplo).
TL; DR
: es una forma de hacer que las funciones sean polimórficas sobre los tipos levantados y sin elevar, lo que no es posible con las funciones regulares.
Por ejemplo, el siguiente código no escribe check con polimorfismos regulares, ya que
Int#
tiene kind
#
, pero las variables de tipo en
id
tienen kind
*
:
{-# 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 comenzar a responder esta pregunta, demos un paso atrás y veamos una de las funciones más utilizadas,
($)
.
¿Cuál es el tipo de
($)
?
Bueno, de acuerdo con Hackage y el informe, es
($) :: (a -> b) -> a -> b
Sin embargo, eso no está 100% completo.
Es una pequeña mentira conveniente.
El problema es que los tipos polimórficos (como
b
) tienen kind
*
.
Sin embargo, los desarrolladores (de la biblioteca) querían usar
($)
no solo para los tipos con kind
*
, sino también para los de kind
#
, p
#
Ej.
unwrapInt :: Int -> Int#
Mientras que
Int
tiene kind
*
(puede ser bottom),
Int#
tiene kind
#
(y no puede ser bottom en absoluto).
Aún así, el siguiente tipo de código verifica:
unwrapInt $ 42
Eso no debería funcionar.
¿Recuerdas el tipo de devolución de
($)
?
Fue polimórfico, y los tipos polimórficos tienen tipo
*
, ¡no
#
!
Entonces, ¿por qué funcionó?
Primero, fue
un error
, y luego fue un
hack
(extracto de
un correo de Ryan Scott
en la lista de correo de ghc-dev):
Entonces, ¿por qué está pasando esto?
La respuesta larga es que antes de GHC 8.0, en el tipo de firma
($) :: (a -> b) -> a -> b
,b
realidad no estaba en especie*
, sino más bienOpenKind
.OpenKind
es un hack horrible que permite que tanto los tipos levantados (kind*
) como los no elevados (kind#
) lo habiten, por lo que(unwrapInt $ 42)
comprueban.
Entonces, ¿cuál es el nuevo tipo de
($)
en 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 mirar a
Levity
:
data Levity = Lifted | Unlifted
Ahora, podemos pensar que
($)
tiene 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
TYPE
es una constante mágica y redefine los tipos
*
y
#
como
type * = TYPE Lifted
type # = TYPE Unlifted
La cuantificación sobre los tipos también es bastante nueva y forma parte de la integración de los tipos dependientes en Haskell .
El nombre de
polimorfismo de gravedad
proviene del hecho de que ahora puede escribir funciones polimórficas sobre tipos levantados y no levantados, algo que no estaba permitido / posible con las restricciones de polimorfismo anteriores.
También elimina el hack de
OpenKind
al mismo tiempo.
Es realmente "solo" sobre esto, manejar 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 del proceso actual.
Referencias
- Polimorfismo de gravedad en Haskell dependiente ; charla de Richard A. Eisenberg sobre ICFP 2015. Muy recomendable.
- Polimorfismo de gravedad (versión extendida) por Richard A. Eisenberg y Simon Peyton Jones
-
GHC.Types
, parte de la bibliotecaghc-prim
que se envía con GHC. -
Discusiones:
- La discusión sobre ghc-dev .
- La discusión sobre haskell-cafe .
Como lo indica el título de la pregunta, quiero saber qué es el polimorfismo de Levity y cuál es su motivación. Sé que esta página tiene algunos detalles, pero la mayoría de las explicaciones se me pasan por la cabeza. :)
Si bien esta página es un poco más amigable, todavía no puedo entender la motivación detrás de ella.