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

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为空.在类型理论中,空类型通常用作逻辑上"假"命题的等价类型.