Puis-je paramétrer le type de contrainte vide?

Question

J'ai une classe pour les files d'attente qui permet à l'instance de définir les contraintes qu'elle place sur les éléments. Par exemple, une file d'attente prioritaire exige que ses éléments soient commandable:

{-# LANGUAGE MultiParamTypeClasses, ConstraintKinds, FunctionalDependencies #-} 

class Queue q c | q -> c where 
    empty :: q a 
    qpop :: c a => q a -> Maybe (a, q a) 
    qpush :: c a => a -> q a -> q a 

data PriorityQueue a = ... 

instance Queue PriorityQueue Ord where 
    ... 

Cela fonctionne un charme: dans la déclaration d'instance pour PriorityQueue I peut fonctionner sur des éléments de la file d'attente à l'aide des membres de Ord tels que (>).

---

J'ai coincé essayer de définir une file d'attente qui place aucune exigence sur ses éléments:

newtype LIFO a = LIFO [a] 

instance Queue LIFO() where 
    empty = LIFO [] 
    qpop (LIFO []) = Nothing 
    qpop (LIFO (x:xs)) = Just (x, LIFO xs) 
    qpush x (LIFO xs) = LIFO $ x:xs 

Cela échoue, le message d'erreur suivant GHC:

The second argument of `Queue' should have kind `* -> Constraint', 
    but `()' has kind `*' 
In the instance declaration for `Queue LIFO()' 

Ce message d'erreur a du sens pour moi. Eq accepte un paramètre de type (nous écrivons généralement Eq a => ...) alors que () n'a pas de paramètres - c'est une vieille différence de type.

---

J'ai eu une fissure à l'écriture d'une fonction de type qui ne tient pas compte de son second argument, qui me permettrait d'écrire instance Queue LIFO (Const()):

{-# LANGUAGE TypeFamilies, KindSignatures, PolyKinds #-} 

type family Const a b :: k -> k2 -> k 
type instance Const a b = a 

Je trouve cette interaction des familles de type et polymorphisme type tout à fait beau, donc je suis un peu déçu quand il ne fonctionne pas (je pensais vraiment que ce serait!):

Expecting two more arguments to `a' 
The first argument of `Const' should have kind `*', 
    but `a' has kind `k0 -> k1 -> k0' 
In the type `a' 
In the type instance declaration for `Const' 

J'ai le sentiment que ce dernier exemple est quelque chose de stupide comme une erreur de syntaxe (je suis nouveau pour taper les familles). Comment puis-je écrire un Constraint qui ne place aucune restriction sur son argument?

Answer 1

Cela devrait fonctionner:

class NoConstraint a where 
instance NoConstraint a where 

instance Queue LIFO NoConstraint where 
    ... 

Le ci-dessus définit une contrainte qui est satisfaite par tous les types. En tant que tel, les obligations c a où c = NoConstraint peuvent toujours être déchargées. En outre, puisqu'il n'y a aucun membre dans cette classe, il devrait avoir zéro (ou presque zéro) coût d'exécution. La "contrainte" () que vous essayez d'utiliser n'est pas considérée comme une contrainte vide définie par GHC, mais comme unité () :: *. Cela provoque Const() :: k2 -> *, ce qui déclenche l'erreur de type.

Si vous ne souhaitez pas utiliser une classe personnalisée, vous pouvez essayer, par exemple. Const (Eq()) ou Const (Num Int), qui ont le bon type k2 -> Constraint. Je ne le recommande pas, car je le trouve moins lisible que d'utiliser une classe personnalisée.

(Cela nécessite de permettre des extensions, comme Benjamin Hodgson souligne ci-dessous un commentaire.)