Specifying Invariants on Value Constructors

Question

Consider the following

data Predicate = Pred Name Arity Arguments type Name = String type Arity = Int type Arguments = [Entity] type Entity = String 

This would create

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

but also "illegal"

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

"Invalid" because arity does not match the length of the argument list.

Using this feature is not enough

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

and only exporting makePred from the Predicate module, is there a way to ensure that the value constructor is correct?

Answer 1

Well, the simple answer is to drop arity from a smart constructor.

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

Then, if you do not expose the Pred constructor from your module and force your clients to go through makePred , you know that they will always match, and you won’t need this unsightly Maybe .

There is no direct way to enforce this invariant. That is, you cannot get makePred 2 ["a","b"] to typecheck, but makePred 2 ["a","b","c"] not to. To do this, you need real dependent types.

There are places in the middle to convince haskell to force your invariants to be used using advanced functions ( GADT + phantom types), but after drinking the whole solution, I realized that I really did not consider your question, and that such methods didn’t really applicable to this problem. Usually this is more of a problem than in general. I would stick with a smart constructor.

I wrote a detailed description of the idea of ​​an intelligent designer . It turns out to be a pretty nice environment between type checking and runtime checking.

Answer 2

It seems to me that if you want these restrictions to be enforced, then you should make the Predicate class, and each kind of predicate your own data type, which is an instance of Predicate .

This will give you the opportunity to have arguments other than String types in your predicates.

Something like this (UNTESTED)

 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 nx) = [(Numeric n), (Numeric x)] satisfied (Divides nx) = x `mod` n == 0 

This may or may not solve your problem, but it is certainly a strong option to consider.