没有构造函数的代数数据类型的目的是什么？

Question

在 Haskell 中，您可以在没有构造函数的情况下定义代数数据类型：

data Henk

但是没有构造函数的类型（或种类？）的目的是什么？

Answer 1

类型级机制通常需要类型存在，但从不构造此类类型的值。

例如，幻像类型：

module Example (Unchecked, Checked, Stuff()) where

data Unchecked
data Checked
data Stuff c = S Int String Double

check :: Stuff Unchecked -> Maybe (Stuff Checked)
check (S i s d) = if i>43 && ...
                  then Just (S i s d)
                  else Nothing

readFile :: Filepath -> IO (Stuff Unchecked)
readFile f = ...

workWithChecked :: Stuff Checked -> Int -> String
workWithChecked stuff i = ...

workWithAny :: Stuff any -> Int -> Stuff any
workWithAny stuff i = ...

只要模块不导出S构造函数，这个库的用户就不能伪造Stuff数据类型的“已检查”状态。

在上面，workWithChecked 函数不必在每次调用时都清理输入。用户必须已经完成了它，因为它必须提供一个“已检查”类型的值——这意味着用户必须事先调用check 函数。这是一种高效且稳健的设计：我们不会在每次调用时一遍又一遍地重复相同的检查，但我们也不允许用户传递未经检查的数据。

注意Checked,Unchecked 类型的值是无关紧要的——我们从不使用这些。

正如其他人在 cmets 中提到的，除了幻像类型之外，空类型还有许多其他用途。例如，一些 GADT 涉及空类型。例如

data Z
data S n
data Vec n a where
  Nil  :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

上面我们使用空类型来记录类型中的长度信息。

此外，需要没有构造函数的类型来实现一些理论属性：如果我们寻找a 使得Either a T 与T 同构，我们希望a 为空。在类型论中，空类型通常用作逻辑上“假”命题的类型等价物。