Verwendung des Haskell-Typensystems, um festzulegen, dass eine Klasse zusätzlichen Eigenschaften gehorcht (d. h. Typklassen für Typklassen)

Question

Wenn wir eine Typklasse erstellen, gehen wir in der Regel davon aus, dass ihre Funktionen einigen Eigenschaften gehorchen müssen. So gibt es die Monoid- und Monadengesetze für ihre jeweiligen Typklassen. Aber was ist, wenn es ein Gesetz gibt, wie z.B. Assoziativität, das ich spezifizieren möchte, dass mehrere Klassen diesem Gesetz entweder gehorchen oder nicht gehorchen können? Gibt es eine Möglichkeit, dies im Typsystem von Haskell zu tun? Ist diese Art von Typklassen für Typklassen-Idee in der Praxis überhaupt realisierbar?

---

Hier ist ein motivierendes Beispiel aus der Algebra:

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

Wenn ich nun festlegen möchte, dass die Addition über Int's assoziativ und kommutativ ist, kann ich die Klassen und Instanzen erstellen:

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

instance AssociativeAddition Int where
instance CommutativeAddition Int where

Aber das ist mühsam, weil ich alle möglichen Kombinationen für alle Klassen erstellen muss. Ich kann nicht einfach assoziative und kommutative Klassen erstellen, denn was ist, wenn die Addition kommutativ ist, die Multiplikation aber nicht (wie bei Matrizen)?

Ich würde gerne etwas sagen können wie:

class Associative x where

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

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

Ist das machbar?

(Haskells abstrakte Algebra-Pakete, wie algebra und constructive-algebra, tun dies derzeit nicht, daher nehme ich an, dass dies nicht der Fall ist. Aber warum nicht?)

Answer 1

Mit einigen neueren GHC-Erweiterungen können Sie dies tatsächlich tun:

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