约束数据类型

Question

假设您有一个很好的归纳定义，并且您想将其定义为 Haskell 中的数据类型。但是，您的归纳定义（与许多归纳定义一样）具有这样一种形式，即生成规则要求它们的“前提”具有某种结构。例如，假设我们有以下定义：

• 如果x是偶数，那么T x是武器，
• 如果x 是奇数，则S x 是武器。

如果我想在 Haskell 中定义这个（作为单一的）数据类型，我会写类似的东西

data Weapon =  T Int | S Int

显然，这将不起作用，因为您现在可以生成 T 5 和 S 4，例如。是否有一种自然的方式来传递对构造函数参数的限制，以便我可以编写类似于上述代码的代码来给出正确的定义？

Answer 1

如果你愿意限制自己使用 Nats，并且可以使用相当高级的类型魔法，你可以使用GHC.TypeLits。

{-# LANGUAGE DataKinds, GADTs, TypeOperators, KindSignatures #-}

import GHC.TypeLits

data Weapon (n :: Nat) where
    Banana      :: n ~ (2 * m) => Weapon n
    PointyStick :: n ~ (2 * m + 1) => Weapon n

banana :: Weapon 2
banana = Banana

pointyStick :: Weapon 3
pointyStick = PointyStick

自己尝试一下，它不会用错误的（奇数/偶数）数字编译。

编辑：更实用的可能是仙人掌的方法。

Answer 2

这有点不合时宜，但在例如Agda：更改您的表示的解释，以便通过构造强制它是正确的。

在这种情况下，请注意如果n :: Int，则even (2 * n) 和odd (2 * n + 1)。如果我们放弃Ints 太大的情况，我们可以说偶数Ints 和Ints 之间存在双射；另一个介于奇怪的 Ints 和 Ints 之间。

所以使用这个，你可以选择这个表示：

data Weapon = T Int | S Int

并更改其解释，使值T n 实际上代表T (2 * n)，值S n 代表S (2 * n + 1)。所以无论您选择什么n :: Int，T n 都将是有效的，因为您会将其视为“T-of-2*n”值。

Answer 3

最好不要显式导出T 和S，而是允许自定义构造函数：

module YourModule (Weapon, smartConstruct) where

data Weapon =  T Int | S Int

smartConstruct :: Int -> Weapon
smartConstruct x
    | even x     = T x
    | otherwise  = S x

现在在导入YourModule 时，用户将无法显式创建T 和S，只能使用smartConstruct 函数。