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

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"]

"非法"因为arity与参数列表的长度不匹配.

没有使用这样的功能

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使用高级功能(GADTs +幻像类型)来强制执行你的不变量,但在写完一个完整的解决方案之后,我意识到我并没有真正解决你的问题,并且这些技术并不真正适用特别是这个问题.他们通常也比一般的价值更麻烦.我坚持使用智能构造函数.

我写了一篇关于智能构造函数概念的深入描述.事实证明,它是类型验证和运行时验证之间非常令人愉快的中间环节.