具有零构造函数的代数数据类型的意义是什么？

Question

遗憾的是,这篇文章没有提及关于Haskell中ADT的发展,来自Aask of Haskell:懒惰与类,第5.1节:

通常,代数类型指定一个或多个备选方案的总和,其中每个备选方案是零个或多个字段的乘积.允许零替代的总和可能是有用的,这将是完全空的类型,但是当时这种类型的值不被理解.

让我想知道,这样的ADT怎么会有用？

Answer 1

从理论上讲:库里 - 霍华德的同构性使我们将这种类型解释为"虚假"命题."虚假"本身就是一个有用的命题; 但是对于构造"非"组合子(as type Not a = a -> False)和其他类似结构也是有用的.

务实:此类型可用于防止参数化数据类型的某些分支存在.例如,我在库中使用它来解析各种游戏树,如下所示:

data RuleSet a            = Known !a | Unknown String
data GoRuleChoices        = Japanese | Chinese
data LinesOfActionChoices -- there are none in the spec!
type GoRuleSet            = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices

这样做的结果是,在解析一行动作游戏树时,如果指定了规则集,我们就知道它的构造函数是Unknown,并且可以在模式匹配期间关闭其他分支等.