Qu'est-ce que le polymorphisme de Levity?

Question

Comme le titre de la question l'indique, je veux savoir ce qu'est le polymorphisme de Levity et quelle est sa motivation. Je sais que cette page contient des détails, mais la plupart des explications qui y figurent me pardonnent. :)

Bien que cette page soit un peu plus conviviale, je ne comprends toujours pas la motivation qui la sous-tend.

Answer 1

Note: Cette réponse est fondée sur des observations très récentes sur la Légèreté des discussions. Tout ce qui concerne la Légèreté polymorphisme est actuellement mis en œuvre dans le GHC la version 8.0 candidats et soumises en tant que telles à changer (voir #11471 par exemple).

---

TL;DR: C'est une façon de faire de fonctions polymorphes plus de levé et unlifted types, ce qui n'est pas possible avec des fonctions classiques. Par exemple, le code suivant ne tapez pas de vérifier régulièrement les polymorphismes, depuis Int# a #, mais le type des variables en id ont *:

{-# 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

Notez que (->) utilise encore un peu de magie.

---

Avant de commencer à répondre à cette question, faisons un pas en arrière et aller à l'un des les plus souvent utilisés en fonctions, ($).

Qu'est - ($)s'type? Eh bien, selon Hackage et le rapport, c'est

($) :: (a -> b) -> a -> b

Cependant, ce n'est pas complète à 100%. C'est une pratique peu de mensonge. Le problème est que les types polymorphes ont *. Cependant, (bibliothèque), les développeurs voulaient utiliser ($) pas seulement pour les modèles avec l'aimable *, mais aussi pour ceux de type #, par exemple

unwrapInt :: Int -> Int#

Alors qu' Int a * (il peut être en bas), Int# a # (et ne peut pas être inférieur à tous). Encore, le code suivant typechecks:

unwrapInt $ 42

Cela ne fonctionnerait pas. Rappelez-vous le type de retour d' ($)? Il est polymorphe, et polymorphe types de genre *, pas #! Alors, pourquoi ça marche? Tout d'abord, c'était un bug, et puis c'était un hack (extrait d' un mail par Ryan Scott sur le ghc-dev mailing list):

Alors pourquoi est-ce qui se passe?

La réponse longue est que, avant de GHC 8.0, la signature de type ($) :: (a -> b) -> a -> b, b fait n'était pas dans le genre *, mais plutôt OpenKind. OpenKind est un affreux hack qui permet à la fois de levée ( *) et unlifted (genre #) types de l'habitent, c'est pourquoi (unwrapInt $ 42) typechecks.

Donc, qu'est - ($)'s nouveau type dans GHC 8.0? C'est

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b
-- will likely change according to Richard E.

Pour la comprendre, nous devons examiner Levity:

data Levity = Lifted | Unlifted

Maintenant, nous pouvons penser à de la ($) soit l'un des types suivants, puisqu'il y a seulement deux choix de w:

-- pseudo types
($) :: forall a (b :: TYPE   Lifted). (a -> b) -> a -> b
($) :: forall a (b :: TYPE Unlifted). (a -> b) -> a -> b

TYPE magique est une constante, et il redéfinit le genre * et # comme

type * = TYPE Lifted
type # = TYPE Unlifted

La quantification sur les types est également assez nouveau et une partie de l' intégration des types de charge en Haskell.

Le nom de Légèreté polymorphisme vient du fait que vous pouvez maintenant écrire des fonctions polymorphes sur les deux levées et unlifted types, quelque chose qui n'était pas autorisé/possible avec le précédent polymorphisme de restriction. Il obtient également débarrasser de l' OpenKind hack en même temps. C'est vraiment "juste" à ce sujet, la manipulation de ces deux sortes de types.

_{Par ailleurs, vous n'êtes pas seul avec votre question. Même Simon Peyton Jones a dit qu'il ya un besoin pour une Légèreté page wiki, et Richard E. (l'actuel responsable de l'implémentation de ce) a déclaré que la page wiki a besoin d'une mise à jour sur le processus en cours.}

Références

• La légèreté du Polymorphisme Dans Dépendante Haskell; parler par Richard A. Eisenberg sur ICFP 2015. Très recommandé.
• GHC.Types, une partie de l' ghc-prim bibliothèque livré avec GHC.
• Le archivé(?) discussion sur ghc-dev.
• Le débat en cours sur haskell-café.