具有类型约束的 Haskell 类型族实例

Question

我试图用类型族来表示表达式，但我似乎无法弄清楚如何编写我想要的约束，而且我开始觉得这是不可能的。这是我的代码:

class Evaluable c where
    type Return c :: *
    evaluate :: c -> Return c

data Negate n = Negate n

instance (Evaluable n, Return n ~ Int) => Evaluable (Negate n) where
    type Return (Negate n) = Return n
    evaluate (Negate n) = negate (evaluate n)

这一切都编译得很好，但它并不能完全表达我想要的。在 Negate 的约束下 Evaluable 的实例，我说 Negate里面的表达式的返回类型必须是 Int (使用 Return n ~ Int )这样我就可以调用 negate 了，但这太严格了。返回类型实际上只需要是 Num 的一个实例即可。具有 negate 的类型类功能。那样 Double年代， Integer s 或 Num 的任何其他实例也可以被否定，而不仅仅是 Int s。但我不能只写

Return n ~ Num

而是因为 Num是一个类型类和 Return n是一种类型。我也放不下

Num (Return n)

而是因为 Return n是类型而不是类型变量。

我正在尝试用 Haskell 做些什么？如果不是，应该是，还是我误解了它背后的一些理论？我觉得Java可以添加这样的约束。让我知道这个问题是否更清楚。

编辑:谢谢伙计们，这些回应很有帮助，并且正在解决我的怀疑。如果没有 UndecidableInstances，类型检查器似乎无法处理我想做的事情，所以我的问题是，我想要表达的内容真的无法确定吗？它适用于 Haskell 编译器，但一般来说是这样吗？即是否可能存在一个约束，这意味着“检查 Return n 是 Num 的一个实例”，这可以由更高级的类型检查器决定？

Answer 1

实际上，您可以完全按照您所说的进行:

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances #-}

class Evaluable c where
    type Return c :: *
    evaluate :: c -> Return c

data Negate n = Negate n

instance (Evaluable n, Num (Return n)) => Evaluable (Negate n) where
    type Return (Negate n) = Return n
    evaluate (Negate n) = negate (evaluate n)

Return n当然是一个类型，它可以是一个类的实例，就像 Int能够。你的困惑可能是关于什么可以是约束的论点。答案是“任何类型正确的东西”。那种 Int是 * , 就像 Return n 的那种. Num有样 * -> Constraint ，所以任何类型的 *可以是它的论据。写 Num Int 是完全合法的(虽然是空洞的)作为约束，与 Num (a :: *) 相同。是合法的。