具有类型约束的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 或任何其他 Num 的实例也可以被否定，而不仅仅是 Int。但我不能只写

Return n ~ Num

相反，因为Num是一个类型类而Return n是一个类型。我也不能放置。

Num (Return n)

Return n 是一个类型而非类型变量，所以不能这么用。在 Haskell 中是否有实现的可能？如果没有，是否应该有这样的实现，还是我理解有误？我感觉 Java 可以添加这样的约束。如果问题不够清晰，请告诉我。

编辑：谢谢大家的回答，它们有帮助并且指出了我的疑惑。似乎类型检查器不能处理我想要做的事情，除非使用 UndecidableInstances。那么我的问题是，我想要表达的内容是否真的是不可判定的？对于更高级的类型检查器来说，是否存在一种约束条件，可以检查“Return n 是否为 Num 的实例”这一点，从而变得可判定？

- user3773003

---

顺便问一下，在你的尝试和错误过程中，GHC有没有推荐过诸如FlexibleContexts之类的语言扩展？因为我相当确定它确实这样做了——只是关于_Haskell究竟能否实现这一点_的副注。 - Erik Kaplun

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 (a :: *)一样，将Num Int作为约束是完全合法的（尽管无意义）。

- crockeea

---

对，我应该解释一下，我已经研究过这个问题了，但是FlexibleContexts和UndecidableInstances扩展让我感到有些紧张。我觉得当添加更多实例时，它们可能会在最后反噬我，除非我错了。 - user3773003

据我所知，“FlexibleContexts”是完全安全的，只是允许非类型变量作为类型参数。“UndecidableInstances”可能会在编译过程中导致实例循环而无法终止（编译器无法检查此类情况）。更多信息请参见此答案。 - crockeea

@user3773003: 我想说的比 Eric 更强烈：我认为在没有使用 FlexibleContexts 以及 UndecidableInstances 的情况下，使用 TypeFamilies 是不合理的！非灵活上下文规则是为一种没有类型族的语言设计的；它需要扩展也就不足为奇了。而且由于类型族是类型级别的函数，所以(类型级别的)终止检查可能会成为问题，特别是因为它并不是很聪明；我们没有一个值级别的终止检查器，因此UndecidableInstances 可以提供类似的表达式能力到类型级别。 - Antal Spector-Zabusky

@user3773003 我认为FlaxibleContexts是完全无害的，希望它能够被包含在下一个Haskell标准中。UndecidableInstances也可以接受，尽管我可以看到需要显式开启它的一些价值。然而，Incoherent-和Overlapping-实例是邪恶的，应尽量避免使用。 - chi

Answer 2

为了补充Eric的回答，让我提出一个可能的替代方案：使用函数依赖而不是类型族：

class EvaluableFD r c | c -> r where
  evaluate :: c -> r

data Negate n = Negate n

instance (EvaluableFD r n, Num r) => EvaluableFD r (Negate n) where
  evaluate (Negate n) = negate (evaluate n)

这使得讨论结果类型变得更容易，例如，您可以编写：

foo :: EvaluableFD Int a => Negate a -> Int
foo x = evaluate x + 12

你还可以使用 ConstraintKinds 部分应用它（这就是为什么我将参数放在那个看起来有点奇怪的顺序中）：

type GivesInt = EvaluableFD Int

您也可以使用您的班级来完成这个任务，但这可能会更加繁琐。

type GivesInt x = (Evaluable x, Result x ~ Int)

- dfeuer

---

是的，我应该在原问题中提到我尝试过的另一件事。这个也需要UndecidableInstances和FlexibleInstances，而我想避免使用它们。 - user3773003

@user3773003，我不太乐观地认为你在没有这些扩展的情况下能得到你想要的东西。当然，我可能会漏掉一些东西。 - dfeuer

@user3773003，启用FlexibleInstances没有任何副作用，而启用UndecidableInstances也基本上是无害的。 - András Kovács

@AndrásKovács，Ekmett 倾向于在可能的情况下避免使用灵活的实例（我认为是为了改善实例解析），但仅在可能的情况下。 - dfeuer