¿Cómo se define la igualdad para instancias de categoría?

Question

Para demostrar que, por ejemplo, las leyes de categoría tienen algunas operaciones en un tipo de datos, ¿cómo se decide cómo definir la igualdad? Teniendo en cuenta el siguiente tipo de representación de expresiones booleanas:

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

¿Es factible tratar de demostrar que Exp forma una categoría con la identidad ETrue y operador:

(<&>) = EAnd 

sin redefinir el ecuación ¿ejemplo? El uso de la instancia predeterminada de la ecuación los izquierda identidad rompe la ley, es decir:

ETrue <&> e == e 

evalúa a Falso . Sin embargo, la definición de una función de eval:

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

y la Eq ejemplo como:

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

soluciona el problema. ¿Es la comparación en términos de (==) un requisito general para solicitar el cumplimiento de dichas leyes, o es suficiente decir que las leyes son válidas para un tipo particular de operador de igualdad?

Answer 1

Igualdad es EVIL. Raramente (si alguna vez) necesita igualdad estructural, porque es demasiado fuerte. Solo quiere una equivalencia que sea lo suficientemente fuerte para lo que está haciendo. Esto es particularmente cierto para la teoría de categorías.

En Haskell, deriving Eq le dará la igualdad estructural, lo que significa que usted va a menudo desea escribir su propia implementación de ==//=.

Un ejemplo simple: defina el número racional como pares de números enteros, data Rat = Integer :/ Integer. Si usa la igualdad estructural (lo que Haskell es deriving), tendrá (1:/2) /= (2:/4), pero como fracción 1/2 == 2/4. Lo que realmente le importa es el valor que sus tuplas denotan, no su representación. Esto significa que necesitará una equivalencia que compare fracciones reducidas , por lo que debe implementar eso en su lugar.

Nota al margen: Si alguien que use el código se supone que usted ha definido una prueba la igualdad estructural, es decir, que la comprobación con == justifica la sustitución de datos subcomponentes través de coincidencia de patrones, su código puede romper.Si eso es importante, puede ocultar los constructores para no permitir la coincidencia de patrones, o quizás definir su propio class (por ejemplo, Equiv con === y =/=) para separar ambos conceptos. (Este es sobre todo importante para los demostradores de teoremas como Agda o Coq, en Haskell es realmente duro para obtener el código práctico/el mundo real tan mal que finalmente algo se rompe.)

Realmente estúpido (TM) ejemplo: Digamos que la persona desea imprimir largas listas de enormes Rat sy cree que la memorización de las representaciones de cadena de Integer guardará en la conversión de binario a decimal. Hay una tabla de búsqueda para Rat s, de modo que igual Rat s nunca se convertirán dos veces, y hay una tabla de búsqueda para enteros. Si (a:/b) == (c:/d), las entradas enteras faltantes se completarán al copiar entre a - c/ b - d para omitir la conversión (¡ay!). Para la lista [ 1:/1, 2:/2, 2:/4 ], 1 obtiene convertido y luego, como 1:/1 == 2:/2, la cadena para 1 se copia en la entrada de búsqueda 2. El resultado final "1/1, 1/1, 1/4" está borroso.