Haskell Weird Kinds : Le genre de (->) est ? ? -> ? -> *

Question

Lorsque j'ai expérimenté les types de Haskell, et que j'ai essayé d'obtenir le type de -> et ceci est apparu :

$ ghci
...
Prelude> :k (->)
(->) :: ?? -> ? -> *
Prelude> 

Au lieu de l'attendu * -> * -> * . Quels sont les ?? y ? choses ? Veulent-ils dire des types concrets ou des "variables de type" ? Ou quelque chose d'autre ?

Answer 1

Ce sont des extensions spécifiques à GHC du système de types Haskell. Le rapport Haskell 98 ne spécifie qu'un système de type simple :

... les expressions de type sont classées en différents types, qui prennent une l'une des deux formes possibles :

Le symbole * représente le type de tous les constructeurs de types nuls. Si k1 et k2 sont des types, alors k1->k2 est le type type des types qui prennent un type de type k1 et retournent un type de type k2.

GHC prolonge ce système avec une forme de sous-typage par genre, pour permettre à types non emballés et pour permettre à la fonction construtor d'être polymorphe sur les types. Le treillis de genres que GHC supporte est :

             ?
             /\
            /  \
          ??   (#)
          / \     
         *   #     

Where:       *   [LiftedTypeKind]   means boxed type
             #   [UnliftedTypeKind] means unboxed type
            (#)  [UbxTupleKind]     means unboxed tuple
            ??   [ArgTypeKind]      is the lub of {*, #}
            ?    [OpenTypeKind]     means any type at all

Défini dans ghc/compilateur/types/Type.lhs

En particulier :

> error :: forall a:?. String -> a
> (->)  :: ?? -> ? -> *
> (\\(x::t) -> ...)

Où dans le dernier exemple t :: ?? (c'est-à-dire qu'il n'est pas un tuple unboxed). Donc, pour citer GHC, "il y a un peu de sous-typage au niveau du genre".

Pour les âmes intéressées, GHC prend également en charge les types et les genres de coercition ("termes de niveau de type qui agissent comme une preuve pour les égalités de type", comme l'exige le programme Système Fc ) utilisés dans les GADT, les nouveaux types et les familles de types.