限制类型构造函数中的值[重复]答案

【问题标题】：Restricting values in type constructors [duplicate]限制类型构造函数中的值[重复]
【发布时间】：2011-12-15 05:01:13
【问题描述】：

可能重复：
How to create a type bounded within a certain range

我有数据类型：

data Expr = Num Int
          | Expression Expr Operator Expr

在问题的上下文中，(Num Int) 将代表的数字仅为一位数。有没有办法确保类型声明中的限制？

当然，我们可以定义一个函数来测试Expr 是否有效，但最好让类型系统处理它。

【问题讨论】：

标签： haskell

【解决方案1】：

您可以使用带有 smart constructor 的抽象数据类型：

newtype Digit = Digit { digitVal :: Int }
  deriving (Eq, Ord, Show)

mkDigit :: Int -> Maybe Digit
mkDigit n
  | n >= 0 && n < 10 = Just (Digit n)
  | otherwise = Nothing

如果你把它放在另一个模块中并且不导出Digit构造函数，那么客户端代码就不能在[0,9]范围之外构造Digit类型的值，但是你必须手动换行并打开它以使用它。如果有帮助，您可以定义一个执行模运算的Num 实例；这也可以让你使用数字文字来构造数字。（Enum 和 Bounded 也是如此。）

但是，这并不能确保您永远不会尝试创建无效数字，只是您永远不会这样做。如果您想要更多的保证，那么 Jan 提供的手动解决方案会更好，但代价是不那么方便。（如果你为那个 Digit 类型定义了一个 Num 实例，它最终会像“不安全”一样，因为你可以写 42 :: Digit 多亏了你得到的数字文字支持。）

（如果您不知道 newtype 是什么，它基本上是 data 用于具有单个严格字段的数据类型；围绕 T 的新类型包装器将具有相同的运行时表示作为T。这基本上只是一个优化，所以你可以假装它说data来理解这一点。）

编辑：有关更面向理论的 100% 解决方案，请参阅此答案的相当狭窄的评论部分。

【讨论】：

对——这里的额外保证是 Digit 类型的值不会无效，而不是在事后简单地验证 Expr。请注意，即使手动枚举解决方案也允许使用 error "oops" :: Digit 等值。有一些方法可以在高级类型系统中强大而方便地处理这些事情，但是它们还没有进入 Haskell，所以像这样的妥协可能是最好的解决方案。（并不是说他们已经把它变成了任何其他“现实世界”的语言。）
确实；我只是将它与您在问题中验证Expr 的引用联系起来。如果您有一个包含Digit 的数据类型，则不必检查它：它的任何值都将包含从0 到10 的Int。只是构造 @987654342 @ 有可能出错，这会在评估 Digit 字段时出现异常（由于懒惰）。您可能会发现mkDigit :: Int -> Maybe Digit 更具吸引力，因为它强制在构造点预先处理无效数字。
好吧，你不能在编译时捕获所有东西；如果您向用户询问 1 到 9 之间的数字，并且他们输入 8192，则您必须执行运行时检查。像这样的包装器类型的优点是您可以编写在 Exprs 上运行的代码，因为您知道任何 Digit 字段都将包含 0 到 9 之间的有效整数；将任意整数值转换为 Digit 被分离到 Digit 的智能构造函数中。在编译时，可以保证没有 Digit 包含大于 10 的整数；这就是为什么你不从模块中导出构造函数的原因。
嗯，是“是的，但比半途而废要尴尬得多”。 :) 我个人会说这个解决方案使用类型系统静态地强制执行不变量，因为它可以让您保证 Digit 的值是有效的，这对我来说是强静态类型的本质。 YMMV。
用generalised abstract data types 和phantom types 提供type-level natural numbers，你可以构造小于某些类型级自然数的自然数类型n:data Fin n where { Fz :: Fin (S n); Fs :: Fin n -> Fin (S n) } — 不幸的是我很快筋疲力尽这个利润，所以这是我在这个媒体中能做到的最好的:)

【解决方案2】：

由于只有十种可能性，您可以使用Enum 指定所有可能性。

data Digit = Zero | One | Two deriving (Enum, Show)

那么您必须使用fromEnum 将它们视为数字。

1 == fromEnum One

同样，使用toEnum，您可以从一个数字中获得Digit。

toEnum 2 :: Digit

我们可以更进一步，实现Num。

data Digit = Zero | One | Two deriving (Enum, Show, Eq)

instance Num Digit where
  fromInteger x = toEnum (fromInteger x) :: Digit
  x + y = toEnum $ fromEnum x + fromEnum y
  x * y = toEnum $ fromEnum x * fromEnum y
  abs = id
  signum _ = 1

Zero + 1 + One == Two

【讨论】：