Utilizando el sistema de tipos de Haskell para especificar que una clase obedece propiedades adicionales (es decir, clases de tipos para las clases de tipos)

Question

Cuando creamos una clase de tipo, generalmente suponemos que sus funciones deben obedecer a algunas propiedades. Por lo tanto, tenemos las leyes Monoid y Monad para sus respectivas clases de tipos. Pero, ¿qué pasa si hay alguna ley, como la asociatividad, que deseo especificar que varias clases obedezcan o no a esa ley? ¿Hay alguna manera de hacerlo en el sistema de tipos de Haskell? ¿Este tipo de clases de tipos para las clases de tipos de idea es incluso factible en la práctica?

---

Aquí está un ejemplo motivador del álgebra:

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

Ahora, si quiero especificar que además sobre Int de es asociativa y conmutativa, puedo crear las clases e instancias:

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

instance AssociativeAddition Int where 
instance CommutativeAddition Int where 

Pero esto es engorroso porque tengo que crear todas las combinaciones posibles para todas las clases. No puedo simplemente crear clases asociativas y conmutativas, porque ¿qué ocurre si la suma es conmutativa, pero la multiplicación no es (como en las matrices)?

Lo que me gustaría ser capaz de hacer es decir algo como:

class Associative x where 

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

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

se puede hacer esto?

(paquetes de álgebra abstracta de Haskell, como el álgebra y constructivo-álgebra, actualmente no hacen esto, así que no estoy adivinando Pero por qué no.?)

Answer 1

Usted puede hacer esto con algunas extensiones recientes 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