variables de type Functor pour le type de données de la bascule

Question

I ont la définition du type:

newtype Flip f a b = 
    Flip (f b a) deriving (Eq, Show) 

Est-ce que le constructeur de données Flip a un ou trois arguments?

Consinder mise en œuvre suivante:

data K a b = K a 

newtype Flip f a b = 
    Flip (f b a) deriving (Eq, Show) 

instance Functor (Flip K a) where 
    fmap f (Flip (K b)) = Flip (K (f b)) 

Quel est le type de (Flip K a)?

Answer 1

Le constructeur de données Flip a un argument. Cet argument a le type f b a.

Cela signifie donc que f lui-même est un argument de type d'ordre supérieur avec le type f :: * -> * -> *. Une déclaration newtype plus rigoureuse serait:

newtype Flip (f :: * -> * -> *) a b = Flip (f b a) 

Vous pouvez ainsi, par exemple instancier un Flip Either Int Bool, puisque Either est un type qui nécessite deux paramètres de type supplémentaires, puis construire un Flip (Right 1) :: Flip Either Int Bool.

Quel est le type de (Flip K a)?

Flip K a n'est pas un type complètement appliqué. En pseudo-code, il a le type b -> Flip K a b. Une fois que le b a été résolu (Functor fonctionne avec des types d'ordre supérieur), nous savons que le seul argument de Flip aura un constructeur . Par exemple, Flip (K 1) est un type Flip K a Int.

Answer 2

L'avenir est maintenant, lorsque vous (utilisez GHC 8 et) situé sur un drapeau ou deux

Prelude> :set -XPolyKinds -XFlexibleInstances 

Déclarons

Prelude> newtype Flip f a b = MkFlip (f b a) 

puis renseigner

Prelude> :kind Flip 
Flip :: (k1 -> k -> *) -> k -> k1 -> * 

Prelude> :type MkFlip 
MkFlip 
    :: forall k k1 (b :: k) (f :: k -> k1 -> *) (a :: k1). 
    f b a -> Flip f a b 

Le constructeur typeFlip prend deux arguments implicites, étant k et k1, et trois arguments explicites, étant une fonction binaire produisant un type, puis ses deux arguments dans l'ordre inverse. Les arguments de cette fonction sont de type non contraint (les personnes âgées peuvent dire "gentil" si elles le veulent), mais il renvoie certainement un type (au sens strict de "chose dans *", plutôt que le sens inutilement vague de "n'importe quel vieux ordures à droite de :: ") car il est certainement utilisé comme un type dans la déclaration de MkFlip.

Le constructeur de données, MkFlip, prend cinq arguments implicites (exactement les arguments des Flip) et un argument explicite, étant des données dans f b a.

Ce qui se passe est une inférence de type Hindley-Milner d'un niveau. Les contraintes sont recueillies (par exemple, f b a doit habiter * parce qu'un argument constructeur doit habiter f b a) mais sinon un type plus général est livré: a et b pourrait être quelque chose, de sorte que leurs types sont généralisés comme k1 et k.

Jouons le même jeu avec le constructeur de type constant:

Prelude> newtype K a b = MkK a 

Prelude> :kind K 
K :: * -> k -> * 

Prelude> :type MkK 
MkK :: forall k (b :: k) a. a -> K a b 

On voit que a :: * mais b peut y avoir vieilleries (et pour cette matière, k :: *, comme ces jours-ci, * :: *). Clairement, a est effectivement utilisé comme le type d'une chose, mais b n'est pas utilisé du tout, donc sans contrainte.

On peut alors déclarer

Prelude> instance Functor (Flip K b) where fmap f (MkFlip (MkK a)) = MkFlip (MkK (f a)) 

et demander

Prelude> :info Flip 
... 
instance [safe] forall k (b :: k). Functor (Flip K b) 

qui nous dit que le b utilisé peut encore être une vieilleries. Parce que nous avions

K :: * -> k -> * 
Flip :: (k1 -> k -> *) -> k -> k1 -> * 

nous pouvons unifier k1 = * et obtenir

Flip K :: k -> * -> * 

et ainsi

Flip K b :: * -> * 

pour tout vieux b. Une instance Functor est donc plausible, et en effet livrable, avec la fonction agissant sur l'élément a empaqueté, correspondant à l'argument de Flip K b qui devient le premier argument de K, d'où le type de l'élément stocké.

L'inférence de type basée sur l'unification est vivante et (assez) bonne, droite de ::.