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

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是无关紧要的——我们从不使用这些。

正如其他人在评论中提到的那样，除了幻像类型之外，空类型还有许多其他用途。例如，一些 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为空。在类型论中，空类型通常用作逻辑上“假”命题的类型等价物。