C'è un modo per implementare i vincoli nelle classi di tipi di Haskell?

Question

C'è un modo (qualsiasi modo) per implementare i vincoli nelle classi di tipi?

Come esempio di ciò di cui sto parlando, supponiamo di voler implementare un gruppo come classe di tipo. Quindi un tipo sarebbe un gruppo se ci sono tre funzioni:

class Group a where 
    product :: a -> a -> a 
    inverse :: a -> a 
    identity :: a 

Ma quelle non sono le funzioni, ma devono essere legati da alcuni vincoli. Per esempio:

product a identity = a 
product a (inverse a) = identity 
inverse identity = identity 

ecc ...

C'è un modo per far rispettare questo tipo di vincolo nella definizione della classe in modo che qualsiasi istanza sarebbe automaticamente ereditare? Come esempio, supponiamo desidero attuare il gruppo C2, definita da:

data C2 = E | C 

instance Group C2 where 
     identity = E 
     inverse C = C 

Queste due definizioni determina univocamente C2 (vincoli sopra definiscono tutte le possibili operazioni - infatti, C2 è l'unico gruppo possibile con due elementi a causa dei vincoli). C'è un modo per farlo funzionare?

Answer 1

C'è un modo per applicare questo tipo di vincolo?

No.sacco di persone sono state chiedendo per essa, tra cui l'illustre Tony Hoare, ma all'orizzonte appare ancora nulla.

Questo problema sarebbe un eccellente argomento di discussione per il gruppo Haskell Prime. Se qualcuno ha lanciato una buona proposta, probabilmente lo si troverà lì.

P.S. Questo è un problema importante!

Answer 2

Le classi di tipi possono contenere definizioni e dichiarazioni. Esempio:

class Equality a where 
    (?=), (!=) :: a -> a -> Bool 

    a ?= b = not (a != b) 
    a != b = not (a ?= b) 

instance Eq a => Equality a where 
    (?=) = (==) 

test = (1 != 2) 

È inoltre possibile specificare vincoli particolari (chiamiamoli leggi) in pianura Haskell, ma non è garantito che il compilatore li userà. Un esempio comune è monadic laws

Answer 3

In alcuni casi è possibile specificare le proprietà utilizzando QuickCheck. Questo non è esattamente l'applicazione, ma ti consente di fornire test generici che devono passare tutte le istanze. Ad esempio con Eq si potrebbe dire:

prop_EqNeq x y = (x == y) == not (x != y) 

Naturalmente è ancora compito dell'autore dell'istanza chiamare questo test.

Fare questo per le leggi della monade sarebbe interessante.