invariantes Especificación de los constructores de datos

Question

considerar los siguientes

data Predicate = Pred Name Arity Arguments 

type Name  = String 
type Arity  = Int 
type Arguments = [Entity] 
type Entity = String 

Esto permitiría la creación de

Pred "divides" 2 ["1", "2"] 
Pred "between" 3 ["2", "1", "3"] 

sino también la "ilegal"

Pred "divides" 2 ["1"] 
Pred "between" 3 ["2", "3"] 

"ilegal" porque la aridad no coincide con la longitud de la lista de argumentos.

corto de utilizar una función como esta

makePred :: Name -> Arity -> Arguments -> Maybe Predicate 
makePred n a args | a == length args = Just (Pred n a args) 
        | otherwise = Nothing 

y sólo exportar makePred desde el módulo de predicados, ¿hay una manera de hacer cumplir la corrección del valor del constructor?

Answer 1

Bueno, la respuesta fácil es quitar la aridad del constructor inteligente.

makePred :: Name -> Arguments -> Predicate 
makePred name args = Pred name (length args) args 

Entonces, si usted no exponga la Pred constructor de su módulo y forzar a sus clientes a pasar por makePred, ustedes saben que siempre van a coincidir, y que no necesitan que antiestético Maybe.

No hay directa manera de hacer cumplir ese invariante. Es decir, no podrá obtener makePred 2 ["a","b"] para marcar, pero makePred 2 ["a","b","c"] no. Necesitas tipos dependientes reales para eso.

Hay lugares en el medio para convencer a Haskell de forzar sus invariantes usando funciones avanzadas (GADT s + tipos fantasma), pero después de escribir una solución completa me di cuenta de que realmente no respondía su pregunta, y que las técnicas no son realmente aplicables a este problema en particular. Por lo general, son más problemáticos de lo que valen en general. Me quedaría con el constructor inteligente.

He escrito an in-depth description of the smart constructor idea. Resulta ser un término medio bastante agradable entre la verificación de tipo y la verificación en tiempo de ejecución.

Answer 2

Me parece que, si quieres dijo que las restricciones puedan hacerse efectivos, entonces usted debe hacer Predicate una clase, y cada tipo de predicado su propio tipo de datos que es una instancia de Predicate.

Esto le daría la posibilidad de tener argumentos distintos a String en sus predicados.

Algo como esto (sin probar)

data Entity = Str String | Numeric Int 

class Predicate a where 
    name :: a -> String 
    arity :: a -> Int 
    args :: a -> [Entity] 
    satisfied :: a -> Bool 

data Divides = Divides Int Int 
instance Predicate Divides where 
    name p = "divides" 
    arity p = 2 
    args (Divides n x) = [(Numeric n), (Numeric x)] 
    satisfied (Divides n x) = x `mod` n == 0 

Esto puede o no puede resolver el problema, pero sin duda es una opción fuerte para tener en cuenta.