Utilisation du système de type Haskell pour spécifier qu'une classe obéit à des propriétés supplémentaires (classes de types pour les classes de type)

Question

Lorsque nous créons une classe de type, nous supposons généralement que ses fonctions doivent obéir à certaines propriétés. Nous avons donc les lois Monoid et Monad pour leurs classes de types respectives. Mais, et s'il y a une loi, comme l'associativité, que je veux spécifier que plusieurs classes peuvent ou non obéir à cette loi? Y a-t-il un moyen de faire cela dans le système de typage de Haskell? Est-ce que ce genre de classes de type pour les classes de type idée est même faisable dans la pratique?

---

Voici un exemple motivant de l'algèbre:

class Addition x where 
    add :: x -> x -> x 

class Multiplication x where 
    mult :: x -> x -> x 

instance Addition Int where 
    add = (+) 

instance Multiplication Int where 
    add = (*) 

Maintenant, si je veux préciser que l'addition sur INT est associative et commutative, je peux créer les classes et instances:

class (Addition x) => AssociativeAddition x where 
class (Addition x) => CommutativeAddition x where 

instance AssociativeAddition Int where 
instance CommutativeAddition Int where 

Mais c'est lourd parce que je dois créer toutes les combinaisons possibles pour toutes les classes. Je ne peux pas simplement créer des classes Associative et Commutative, parce que si l'addition est commutative, mais que la multiplication ne l'est pas (comme dans les matrices)?

Ce que je voudrais être en mesure de faire est de dire quelque chose comme:

class Associative x where 

instance (Associative Addition, Commutative Addition) => Addition Int where 
    add = (+) 

instance (Commutative Multiplication) => Multiplication Int where 
    mult = (*) 

peut-il être fait?

(paquets d'algèbre abstraite Haskell, comme l'algèbre et l'algèbre constructive, ne le font actuellement, alors je devine pas, mais pourquoi pas.?)

Answer 1

Vous pouvez réellement faire avec quelques extensions GHC récentes:

{-# LANGUAGE ConstraintKinds, KindSignatures, MultiParamTypeClasses #-} 
import GHC.Exts (Constraint) 

class Addition (a :: *) where 
    plus :: a -> a -> a 

instance Addition Integer where 
    plus = (+) 

class (c a) => Commutative (a :: *) (c :: * -> Constraint) where 
    op :: a -> a -> a 

instance Commutative Integer Addition where 
    op = plus