Haskell type family instance with type constraints

I am trying to represent expressions with type families, but I cannot seem to figure out how to write the constraints that I want, and I'm starting to feel like it's just not possible. Here is my code:

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)

This all compiles fine, but it doesn't express exactly what I want. In the constraints of the Negate instance of Evaluable , I say that the return type of the expression inside Negate must be an Int (with Return n ~ Int ) so that I can call negate on it, but that is too restrictive. The return type actually only needs to be an instance of the Num type class which has the negate function. That way Double s, Integer s, or any other instance of Num could also be negated and not just Int s. But I can't just write

Return n ~ Num

instead because Num is a type class and Return n is a type. I also cannot put

Num (Return n)

instead because Return n is a type not a type variable.

Is what I'm trying to do even possible with Haskell? If not, should it be, or am I misunderstanding some theory behind it? I feel like Java could add a constraint like this. Let me know if this question could be clearer.

Edit: Thanks guys, the responses are helping and are getting at what I suspected. It appears that the type checker isn't able to handle what I'd like to do without UndecidableInstances, so my question is, is what I'd like to express really undecidable? It is to the Haskell compiler, but is it in general? ie could a constraint even exist that means "check that Return n is an instance of Num" which is decidable to a more advanced type checker?

---

Actually, you can do exactly what you mentioned:

{-# 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 certainly is a type, which can be an instance of a class just like Int can. Your confusion might be about what can be the argument of a constraint. The answer is "anything with the correct kind". The kind of Int is * , as is the kind of Return n . Num has kind * -> Constraint , so anything of kind * can be its argument. It perfectly legal (though vacuous) to write Num Int as a constraint, in the same way that Num (a :: *) is legal.

---

To complement Eric's answer, let me suggest one possible alternative: using a functional dependency instead of a type family:

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)

This makes it a bit easier to talk about the result type, I think. For instance, you can write

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

You can also use ConstraintKinds to apply this partially (which is why I put the arguments in that funny-looking order):

type GivesInt = EvaluableFD Int

You could do this with your class as well, but it would be more annoying:

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

链接地址: http://www.djcxy.com/p/43140.html

上一篇: Haskell GADT typesafe评估者：不止一种类型的常数项。

下一篇: 具有类型约束的Haskell类型系列实例