构造函数中的类型约束

Question

我正在尝试为博弈论制作一个正规形式的博弈求解器，并且我正在尝试使其尽可能通用，以实现良好的实践和我自己的方便。我想使用相同的函数来解决零和游戏和非零和游戏，所以我使用以下数据类型：

data Payoffs = (Num a, Eq a, Ord a) => ZS a
    | (Num a, Eq a, Ord a) => NZS (a,a)

但是，这不是正确的语法。有什么方法可以约束a，使其必须满足这些类型约束？

Answer 1

简答（可能不是您需要的）：
要使您的代码按原样工作，您需要一个 forall 量词（您需要为此启用 ExistentialQuantification）：

{-# LANGUAGE ExistentialQuantification #-}

data Payoffs =
      forall a. (Num a, Eq a, Ord a) => ZS a
    | forall a. (Num a, Eq a, Ord a) => NZS (a,a)

---

如果你在数据构造函数中有一个类型变量（即ZS a），那么你有两种选择：要么该变量必须出现在类型构造函数中（即data Payoffs a =），要么你需要说“我不在乎它是什么类型，只要它支持这些类就行了”——这是通过forall 量词实现的。

但这对我来说似乎有点无用，这表明您可能误解了它的含义。如果您编写上面的代码，您的Payoffs 类型的每个值都将能够包装 any 类型的值，只要该类型支持Num、Eq 和@987654330 @。这样做的一个微妙结果是，如果您有两个 Payoffs 值，它们不一定会包装相同的类型。例如：

let x = ZS (42 :: Int)  -- wraps an Int
let y = NZS (2.71 :: Double, 3.14)  -- wraps two Doubles

这意味着，在解压缩它们时，例如，您将无法将它们加在一起，因为即使它们都实现了Num，编译器也没有任何证据证明它们实际上是同一类型。

我怀疑你真正需要的是一个参数化类型，像这样：

data Payoffs a = ZS a | NZS (a, a)

但是，当然，你失去了约束：任何人都可以去创建ZS String 或其他东西。您可以使用 GADT 语法（带有 GADTs 扩展名）将它们带回来：

{-# LANGUAGE GADTs #-}

data Payoffs a where
    ZS :: (Num a, Ord a, Eq a) => a -> Payoffs a
    NZS :: (Num a, Ord a, Eq a) => (a, a) -> Payoffs a

这个符号等价于ZS a | NZS (a, a)，除了你可以使用与任何函数相同的语法来定义每个构造函数——包括约束。像这样定义的类型不允许创建 Payoffs a 类型的值，除非 a 满足约束。

同时，如果你有一个像这样的类型的值，你就知道它包含什么类型。这使您可以判断两个 Payoffs 值是包装相同类型还是不同类型。然后，如果您知道它们是相同的，则可以使用支持的类对它们进行处理，例如：

addPayoffs :: Payoffs a -> Payoffs a -> Payoffs a
addPayoffs (ZS a) (ZS b) = ZS (a + b)
addPayoffs (ZS a) (NZS (x,y)) = NZS (a+x, a+y)
... etc.