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 allow the creation of

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

but also the "illegal"

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

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

Short of using a function like this

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

and only exporting makePred from the Predicate module, is there a way to enforce the correctness of the value constructor?

Answer 1

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

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

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

There is no direct way to enforce that invariant. That is, you won't be able to get makePred 2 ["a","b"] to typecheck but makePred 2 ["a","b","c"] not to. You need real dependent types for that.

There are places in the middle to convince haskell to enforce your invariants using advanced features (GADTs + phantom types), but after writing out a whole solution I realized that I didn't really address your question, and that such techniques are not really applicable to this problem in particular. They're usually more trouble than they are worth in general, too. I'd stick with the smart constructor.

I've written an in-depth description of the smart constructor idea. It turns out to be a pretty pleasant middle ground between type verification and runtime verification.

Answer 2

It seems to me that, if you want said restrictions to be enforceable, then you should make Predicate a class, and each kind of predicate its own data type that is an instance of Predicate.

This would give you the possibility of having 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 n x) = [(Numeric n), (Numeric x)]
    satisfied (Divides n x) = x `mod` n == 0

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