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

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

好吧，简单的答案是从智能构造函数中删除arity。

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

那么如果你不公开 Pred来自您的模块的构造函数并强制您的客户通过 makePred ，你知道它们总是匹配的，你不需要那个难看的 Maybe .

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

中间有一些地方可以说服 haskell 使用高级功能( GADT s + 幻像类型)强制执行您的不变量，但是在写出完整的解决方案后，我意识到我并没有真正解决您的问题，并且这些技术是特别不适用于这个问题。它们通常也比它们的值(value)更麻烦。我会坚持使用智能构造函数。

我写过 an in-depth description of the smart constructor idea .事实证明，它是类型验证和运行时验证之间的一个非常令人愉快的中间地带。