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) 

这一切都编译好，但它并没有确切地表达我想要的。在NegateEvaluable实例的约束中，我说Negate中的表达式的返回类型必须是Int（与Return n ~ Int），以便我可以在其上调用否定，但这太过于限制。返回类型实际上只需要是具有negate函数的Num类型类的实例。那样Double s，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 has kind * -> Constraint，所以什么的种类*可以是它的论据。它完全合法（虽然是空洞的）以Num Int作为约束，与Num (a :: *)合法相同。

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)