在值构造函数上指定不变量

Question

考虑以下情况

data Predicate = Pred Name Arity Arguments

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

这将允许创建

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

“非法”，但也

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

允许“非法”，因为元数与参数列表的长度不匹配。

如果不使用这样的函数

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

并且只从 Predicate 模块导出 makePred，有没有办法 强制值构造函数的正确性？

Answer 1

嗯，简单的答案是从智能构造函数中删除参数。

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

然后，如果您不从模块中公开 Pred 构造函数并强制您的客户端执行 makePred，您就知道它们将始终匹配，并且您不需要那个难看的也许。

没有直接方法来强制执行该不变量。也就是说，您将无法让 makePred 2 ["a","b"] 进行类型检查，但 makePred 2 ["a","b","c"] 不。为此，您需要真正的依赖类型。

中间有一些地方可以说服 haskell 使用高级功能（GADTs + 幻像类型）来强制执行你的不变量，但是在写出整个解决方案之后，我意识到我并没有真正解决你的问题，并且这些技术并不真正适用于这个问题。一般来说，它们带来的麻烦也多于它们的价值。我会坚持使用智能构造函数。

我写了智能构造函数思想的深入描述。事实证明，这是类型验证和运行时验证之间相当令人愉快的中间立场。

Answer 2

在我看来，如果您希望上述限制是可执行的，那么您应该将 Predicate 创建为一个类，并且每种谓词都有自己的数据类型，即 Predicate 的实例代码>.

这将使您可以在谓词中使用除字符串类型之外的参数。

像这样的东西（未经测试）

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

这可能会也可能不会解决您的问题，但它肯定是一个值得考虑的强大选择。