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

Question

这篇关于在 Haskell 中开发 ADT 的文章不幸缺乏引用，来自 A History of Haskell: Being Lazy With Class ，第 5.1 节:

In general, an algebraic type specifies a sum of one or more alternatives, where each alternative is a product of zero or more fields. It might have been useful to permit a sum of zero alternatives, which would be a completely empty type, but at the time the value of such a type was not appreciated.

让我想知道，这样的 ADT 有什么用？

Answer 1

从理论上讲:Curry-Howard 同构为我们提供了这种类型的解释，即“假”命题。 “假”作为命题本身是有用的；但对于构造“非”组合器(如 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

这样做的影响是，在解析 Lines of Action 游戏树时，如果指定了规则集，我们知道它的构造函数将是 Unknown。 , 并且可以在模式匹配等期间离开其他分支。