5

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

通常，代数类型指定一个或多个备选方案的总和，其中每个备选方案是零个或多个字段的乘积。允许零个替代项的总和可能是有用的，这将是一个完全空的类型，但当时这种类型的价值并不受欢迎。

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

4

4 回答 4

9

从理论上讲：Curry-Howard 同构给了我们将这种类型解释为“假”命题的解释。“假”作为一个命题本身是有用的；但对于构造“非”组合子 (as 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，并且可以在模式匹配等过程中关闭其他分支。

于 2012-08-15T12:01:38.737 回答
3

在对应于逻辑假（如另一个答案中所述）中，它们通常用于与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，以便我们可以在其类型中编码向量的长度。然后，我们可以编写类型安全的函数，例如vhead/vtail只能应用于非空向量。

另请参阅Haskell 中的 [Haskell] 固定长度向量，第 1 部分：使用 GADT，其中详细阐述了示例。

于 2012-08-15T19:06:18.657 回答
2

没有办法构造一个无构造函数类型的“真实”值（这里的“真实”是指终止计算；Haskell 有undefined :: a，并且有可能error :: String -> a编写像mwahaha = mwahaha假”值）。

管道库的 0.5 版及更高版本就是其中一个有用的示例。库中的基本类型是Pipe l i o u m r; 对于这些类型具有不同的参数，aPipe可以用作源（产生输出而不消耗任何输入）、接收器（消耗输入而不产生任何输出）或管道（消耗输入并产生输出）。ito和otype 参数分别是其Pipe输入和输出的类型。

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

于 2012-08-15T18:24:42.127 回答
0

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

于 2012-08-15T12:16:02.560 回答