Haskell-Typ Familieninstanz mit Typbeschränkungen

Question

Ich versuche, Ausdrücke mit Typfamilien darzustellen, aber ich kann nicht herausfinden, wie ich die Einschränkungen schreiben soll, die ich möchte, und ich fange an zu glauben, dass es einfach nicht möglich ist. Hier ist mein 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) 

Das alles kompiliert gut, aber es drückt nicht genau das aus, was ich will. In den Einschränkungen der Negate Instanz von Evaluable, sage ich, dass der Rückgabetyp des Ausdrucks innerhalb Negate ein Int (mit Return n ~ Int) sein muss, so dass ich darauf negieren kann, aber das ist zu restriktiv. Der Rückgabetyp muss eigentlich nur eine Instanz der Num Typklasse sein, die die negate Funktion hat. Auf diese Weise Double s, Integer s oder jede andere Instanz von Num könnte auch negiert werden und nicht nur Int s. Aber ich kann nicht nur schreiben

Return n ~ Num 

statt, weil Num eine Typklasse und Return n ist ein Typ. Ich kann auch nicht setzen

Num (Return n) 

statt, weil Return n ein Typ ist kein Typ Variable.

Was versuche ich mit Haskell überhaupt noch zu erreichen? Wenn nicht, sollte es sein, oder verkenne ich eine Theorie dahinter? Ich habe das Gefühl, dass Java eine Einschränkung wie diese hinzufügen könnte. Lassen Sie mich wissen, ob diese Frage klarer sein könnte.

Edit: Danke Jungs, die Antworten helfen und bekommen, was ich vermutete. Es scheint, dass der Typ-Checker nicht in der Lage ist, mit dem, was ich ohne UndecidableInstances machen möchte, fertig zu werden, also ist meine Frage, möchte ich wirklich unentscheidbar ausdrücken? Es ist für den Haskell-Compiler, aber ist es überhaupt? h., könnte eine Einschränkung sogar existieren, die bedeutet "überprüfe, dass Return n eine Instanz von Num ist", die zu einem fortgeschritteneren Typ-Checker entscheidbar ist?

Answer 1

Eigentlich kann man genau das tun, was Sie erwähnt:

{-# 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 sicherlich ist ein Typ, der eine Instanz einer Klasse Int kann wie sein kann. Ihre Verwirrung könnte darin bestehen, was das Argument einer Einschränkung sein kann. Die Antwort ist "alles mit der richtigen Art". Die Art von Int ist *, ebenso die Art von Return n. Num hat Art * -> Constraint, also alles der Art * kann sein Argument sein. Es ist vollkommen legal (wenn auch nichtssagend), Num Int als Einschränkung zu schreiben, genauso wie Num (a :: *) legal ist.

Answer 2

Um Erics Antwort zu ergänzen, lassen Sie mich eine mögliche Alternative vorschlagen: eine funktionale Abhängigkeit anstelle einer Art Familie mit:

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) 

Dies macht es ein wenig einfacher über das Ergebnis Art zu sprechen, denke ich.Zum Beispiel können Sie schreiben

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

Sie auch ConstraintKinds diese teilweise anwenden können (weshalb ich die Argumente in dieser komisch aussehenden Ordnung zu bringen):

type GivesInt = EvaluableFD Int 

Sie können dies tun, mit Ihre Klasse auch, aber es wäre ärgerlicher:

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