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? i.e. 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?
FlexibleContexts
or something else, during your trial and error process? because I'm quite sure it did — just a side-note on the "is this even possible with Haskell" bit. – Erik Kaplun