Come definire l'uguaglianza per le istanze di categoria?

Question

Per provare che, per esempio, le leggi di categoria sono valide per alcune operazioni su un tipo di dati, come decidere se definire l'uguaglianza? Considerando il seguente tipo per che rappresentano le espressioni booleane:

data Exp 
    = ETrue 
    | EFalse 
    | EAnd Exp Exp 
    deriving (Eq) 

E 'fattibile cercando di dimostrare che Exp forma una categoria con un'identità ETrue ed esercente:

(<&>) = EAnd 

senza ridefinire il Eq esempio? Utilizzando l'istanza predefinita di Eq le sinistra-identità pause di legge, vale a dire:

ETrue <&> e == e 

viene valutato come False. Tuttavia, definente una funzione eval:

eval ETrue = True 
eval EFalse = False 
eval (EAnd e1 e2) = eval e1 && eval e2 

e esempio Eq come:

instance Eq Exp where 
    e1 == e2 = eval e1 == eval e2 

risolve il problema. Il confronto in termini di (==) è un requisito generale per richiedere di soddisfare tali leggi, o è sufficiente dire che le leggi valgono per un particolare tipo di operatore di uguaglianza?

Answer 1

L'uguaglianza è EVIL. Hai raramente (o mai) bisogno uguaglianza strutturale, perché è troppo forte. Vuoi solo un'equivalenza che sia sufficientemente forte per quello che stai facendo. Questo è particolarmente vero per la teoria delle categorie.

In Haskell, deriving Eq vi darà l'uguaglianza strutturale, il che significa che sarete spesso vuole scrivere una propria implementazione di ==//=.

Un semplice esempio: definire il numero razionale come coppie di numeri interi, data Rat = Integer :/ Integer. Se si utilizza l'uguaglianza strutturale (che Haskell è deriving), si avrà (1:/2) /= (2:/4), ma come frazione 1/2 == 2/4. Quello che ti interessa davvero è il valore che le tue tuple indicano, non la loro rappresentazione. Ciò significa che avrai bisogno di un'equivalenza che confronta frazioni ridotte, quindi dovresti implementarla.

Nota a margine: se qualcuno utilizzando il codice si presuppone che avete definito un test uguaglianza strutturale, vale a dire che il controllo con == giustifica la sostituzione sotto-componenti di dati attraverso il pattern matching, il loro codice potrebbe rompersi.Se ciò è importante, è possibile nascondere i costruttori a per non consentire la corrispondenza del modello, oppure definire il proprio (ad esempio, Equiv con === e =/=) per separare entrambi i concetti. (Questo è importante soprattutto per i dimostratori di teoremi come Agda o Coq, in Haskell è davvero difficile da ottenere il codice pratico/del mondo reale in modo sbagliato che finalmente qualcosa si rompe.)

Stupido (TM) Esempio: Diciamo che la persona desidera stampare lunghi elenchi di enormi Rat s e crede che la memoizzazione delle rappresentazioni di stringa degli Integer risparmi sulla conversione da binario a decimale. C'è una tabella di ricerca per Rat s, tale che uguale a Rat s non sarà mai convertito due volte, e c'è una tabella di ricerca per i numeri interi. Se (a:/b) == (c:/d), le voci intere mancanti verranno riempite copiando tra a - c/ b - d per saltare la conversione (ahi!). Per l'elenco [ 1:/1, 2:/2, 2:/4 ], 1 viene convertito convertito e quindi, poiché 1:/1 == 2:/2, la stringa per 1 viene copiata nella voce di ricerca 2. Il risultato finale "1/1, 1/1, 1/4" è borked.