¿Hay alguna manera de implementar restricciones en las clases de tipos de Haskell?

¿Hay alguna manera (cualquier forma) de implementar restricciones en clases de tipos?¿Hay alguna manera de implementar restricciones en las clases de tipos de Haskell?

Como un ejemplo de lo que estoy hablando, supongamos que quiero implementar un grupo como una clase de tipo. Así que un tipo sería un grupo si hay tres funciones:

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

Pero esas no son ninguna función, pero deben estar relacionados por algunas limitaciones. Por ejemplo:

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

etc ...

¿Hay una manera de hacer cumplir este tipo de restricción en la definición de la clase para que cualquier instancia heredaría automáticamente? Como un ejemplo, supongamos que me gustaría implementar el grupo C2, que se define por:

data C2 = E | C 

instance Group C2 where 
     identity = E 
     inverse C = C

Este dos definiciones determina de forma única C2 (las limitaciones anteriormente definen todas las operaciones posibles - de hecho, C2 es el único grupo posible con dos elementos debido a las limitaciones). ¿Hay alguna manera de hacer que esto funcione?

Fuente

2010-02-12 Rafael S. Calsaverini

(Er, 'C inversa C = C', ¿no?) – dave4420

sí, gracias por notar –

Esas restricciones suelen llamarse * leyes * ejemplo, leyes de Mónada. – mb14

¿Hay alguna forma de imponer este tipo de restricciones?

Nº montón de gente ha estado preguntando por él, incluyendo el ilustre, Tony Hoare, pero no aparece nada en el horizonte todavía.

Este problema sería un excelente tema de discusión para el grupo Haskell Prime. Si alguien ha publicado una buena propuesta, es probable que se encuentre allí.

P.S. Este es un problema importante!

Fuente

2010-02-13 01:13:25

Tengo la firme creencia de que la verificación en tiempo de compilación para la satisfacción de tales restricciones es equivalente a la detención. ¿Puedes arrojar algo de luz sobre este asunto? – fishlips

@fishlips: Me sorprendería que un compilador pudiera verificar por sí solo si una implementación satisface tales restricciones, pero no puedo afirmar que conozco la literatura de reescritura de términos lo suficientemente bien como para confiar en escribir una prueba. Sin embargo, sospecho que en cualquier implementación probable, si un programador quiere que se comprueben las restricciones en * compile * time, se le pedirá que proporcione una prueba verificable por la máquina. –

hummm ... eso es triste de escuchar. ¿Hay algún otro lenguaje que pueda realizar este tipo de comprobación de restricciones? Un problema que me gustaría resolver es exactamente hacer un programa que encuentre todas las instancias posibles dadas algunas restricciones algebraicas como en este caso (es decir, encontrar todas las posibles orden n grupos). Escuché que Prolog puede hacer algo así, pero prefiero tener un lenguaje funcional. –

Las clases de tipos pueden contener definiciones y declaraciones. Ejemplo:

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)

También puede especificar restricciones especiales (llamémoslos leyes) en la llanura Haskell, pero no está garantizado que el compilador usarlos. Un ejemplo común es monadic laws

Fuente

2010-02-12 16:34:36 Dario

En algunos casos, puede especificar las propiedades con QuickCheck. Esto no es exactamente una aplicación, pero le permite proporcionar pruebas genéricas que todas las instancias deben aprobar. Por ejemplo, con la ecuación se podría decir:

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

Por supuesto que todavía depende de autor instancia para llamar a esta prueba.

Hacer esto para las leyes de mónada sería interesante.

Fuente

2010-02-13 09:57:43

¿Hay alguna manera de implementar restricciones en las clases de tipos de Haskell?

Respuesta

Cuestiones relacionadas