Specifica invarianti sui costruttori di valore

Question

Si consideri il seguente

data Predicate = Pred Name Arity Arguments 

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

Ciò consentirebbe la creazione di

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

ma anche la "illegale"

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

"illegale", perché l'arity non corrisponde alla lunghezza dell'elenco di argomenti.

Breve di utilizzare una funzione come questa

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

e solo l'esportazione makePred dal modulo predicato, c'è un modo per far rispettare la correttezza del costruttore di valore?

Answer 1

Bene, la risposta facile è eliminare l'arity dal costruttore intelligente.

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

Poi, se non esporre il Pred costruttore dal modulo e forzare i vostri clienti a passare attraverso makePred, si sa che essi saranno sempre corrispondere, e non hai bisogno di quella sgradevole Maybe.

Non esiste un diretto modo per far rispettare tale invariante. Cioè, non sarai in grado di ottenere makePred 2 ["a","b"] in typececk ma non in makePred 2 ["a","b","c"]. Hai bisogno di veri tipi dipendenti per quello.

Ci sono posti nel mezzo per convincere haskell a far rispettare i tuoi invarianti usando le funzioni avanzate (GADT s + tipi di fantasma), ma dopo aver scritto una soluzione completa mi sono reso conto che non ho davvero risposto alla tua domanda, e che le tecniche non sono realmente applicabili a questo problema in particolare. Di solito sono più problemi di quanti ne valga in generale. Mi terrei con il costruttore intelligente.

Ho scritto an in-depth description of the smart constructor idea. Risulta essere una via di mezzo piuttosto piacevole tra la verifica del tipo e la verifica del runtime.

Answer 2

Mi sembra che, se si desidera che le restrizioni siano applicabili, è necessario creare una classe con Predicate e ogni tipo di predicato con il proprio tipo di dati che è un'istanza di Predicate.

Ciò ti darebbe la possibilità di avere argomenti diversi dai tipi di stringa nei tuoi predicati.

Qualcosa di simile (non testata)

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 

Questo può o non può risolvere il problema, ma è certamente una forte opzione da considerare.