Używanie systemu typu Haskell do określania, że ​​dana klasa zachowuje dodatkowe właściwości (tj. Klasy typów dla klas typów)

Question

Kiedy tworzymy klasę typu, zwykle zakładamy, że jej funkcje muszą być zgodne z pewnymi właściwościami. Tak więc mamy prawa Monoid i Monad dla ich odpowiednich klas typów. Ale co, jeśli istnieje jakieś prawo, takie jak asocjatywność, że chcę określić, że wiele klas może, ale nie musi przestrzegać tego prawa? Czy istnieje sposób, aby to zrobić w systemie typu Haskella? Czy tego typu klasy typów dla pomysłów klas klas są nawet w praktyce możliwe?

---

Oto motywowanie przykład z algebry:

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 = (*) 

Teraz, jeśli chcę, aby określić, że dodatek na INT jest łączne i przemienne, mogę tworzyć klas i wystąpień:

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

instance AssociativeAddition Int where 
instance CommutativeAddition Int where 

Jest to jednak uciążliwe, ponieważ muszę utworzyć wszystkie możliwe kombinacje dla wszystkich klas. Nie mogę po prostu utworzyć klas asocjatywnych i przemiennych, bo co z tego, że dodawanie jest przemienne, ale mnożenie nie jest (jak w macierzach)?

Co chciałbym być w stanie zrobić, to powiedzieć coś w stylu:

class Associative x where 

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

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

można to zrobić?

(streszczenie pakiety algebra Haskell, podobnie jak algebry i konstruktywnej-algebrze, obecnie nie to zrobić, więc nie jestem zgadywania Ale dlaczego nie.?)

Answer 1

rzeczywiście można to zrobić z kilku ostatnich rozszerzeń GHC:

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