具有类型约束的Haskell类型系列实例
我试图用类型族表示表达式，但我似乎无法弄清楚如何编写我想要的约束条件，并且我开始觉得这是不可能的。 这是我的代码：
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类型的实例。 这样Double S， Integer或任何其他Num实例也可以被否定，而不仅仅是Int 。 但我不能只写
Return n ~ Num
相反，因为Num是一个类型类，并且Return n是一个类型。 我也不能放
Num (Return n)
而是因为Return n是一个类型而不是一个类型变量。
我试图用Haskell做甚么？ 如果不是，应该是，还是我误解了它背后的一些理论？ 我觉得Java可以添加这样的约束。 让我知道这个问题是否可以更清楚。
编辑：谢谢你们，反应正在帮助我们，并得到我怀疑的东西。 看起来，类型检查器无法处理我想要做的事情，如果没有UndecidableInstances，所以我的问题是，我想表达的是真正不可判定的？ 这是对Haskell编译器的，但它是一般的吗？ 即可能存在一个约束，意味着“检查返回n是否为Num的一个实例”，这对于更高级的类型检查器是可判定的？
其实，你可以做你刚才提到的：
{-# 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 can一样是一个类的实例。 你的困惑可能是什么可以成为约束的论据。 答案是“任何正确的东西”。 Int的类型是* ， Return n类型是Return n 。 Num有种* -> Constraint ，所以任何类型的*都可以作为它的参数。 以Num (a :: *)是合法的方式，将Num Int作为约束条件完全合法（虽然是空的）。
为了补充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)