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

Question

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

一般来说，代数类型指定一个或多个的和 替代品，其中每个替代品都是零个或多个的乘积 字段。允许零和可能很有用 替代品，这将是一个完全空的类型，但在当时 这种类型的价值不被欣赏。

让我想知道，这样的 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，并且可以在模式期间保留其他分支火柴之类的

Answer 2

在对应于逻辑false（如另一个答案中所述）中，它们通常用于结合GADTs创建额外的类型约束。例如：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}

import Data.List (groupBy)

data Zero
data Succ n

data Vec n a where
    Nil  ::                 Vec Zero a
    Cons :: a -> Vec n a -> Vec (Succ n) a

vhead :: Vec (Succ n) a -> a
vhead (Cons v _) = v

vtail :: Vec (Succ n) a -> Vec n a
vtail (Cons _ v) = v

这里我们有两个没有构造函数的数据类型。它们在这里的含义只是表示自然数：Zero、Succ Zero、Succ (Succ Zero) 等。它们在Vec 数据类型中用作phantom types，以便我们可以在其类型中编码向量的长度。然后，我们可以编写类型安全的函数，例如 vhead/vtail，这些函数只能应用于非空向量。

另请参阅[Haskell] Fixed-length vectors in Haskell, Part 1: Using GADTs，其中详细说明了示例。

Answer 3

没有办法构造一个无构造函数类型的“真实”值（这里的“真实”是指终止计算；Haskell 有 undefined :: a、error :: String -> a 以及编写像 @ 这样的非终止程序的可能性987654327@，为简单起见，我将其称为“假”值）。

conduit 库的 0.5 版及更高版本就是其中一个有用的示例。库中的基本类型为Pipe l i o u m r；对于这些类型具有不同的参数，Pipe 可以用作 source（产生输出而不消耗任何输入）、sink（消耗输入而不产生任何输出) 或 conduit（消耗输入并产生输出）。 Pipe 的i 和o 类型参数分别是其输入和输出的类型。

因此，管道库通过使用来自Data.Void 的Void 类型作为源的输入类型和接收器的输出类型来强制执行源不消耗输入而接收器不产生输出的概念的一种方式。同样，没有终止方法来构造这种类型的值，因此尝试使用接收器输出的程序不会终止（提醒一下，在 Haskell 中，这可能意味着“引发错误”而不一定“永远循环”）。

Answer 4

没有构造函数的类型称为幻像类型。请参阅Haskell wiki中的页面。