Haskell tipo istanza famiglia con vincoli di tipo

Question

Sto cercando di rappresentare espressioni con famiglie di tipi, ma non riesco a capire come scrivere i vincoli che voglio, e sto iniziando a sentire come se non fosse possibile. Ecco il mio codice:

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) 

Il tutto compila bene, ma non esprime esattamente quello che voglio. Nei vincoli dell'istanza Negate di Evaluable, dico che il tipo restituito dell'espressione all'interno di Negate deve essere un Int (con Return n ~ Int) in modo che sia possibile chiamare negare su di esso, ma che è troppo restrittivo. Il tipo restituito deve essere solo un'istanza della classe di tipo Num che ha la funzione negate. In questo modo Double s, Integer s, o qualsiasi altra istanza di Num potrebbero anche essere negati e non solo Int s. Ma non posso solo scrivere

Return n ~ Num 

, invece, perché Num è una classe tipo e Return n è un tipo. Anche non posso mettere

Num (Return n) 

invece perché Return n è un tipo non una variabile di tipo.

È quello che sto cercando di fare anche con Haskell? In caso contrario, dovrebbe essere, o sto fraintendendo qualche teoria dietro di esso? Mi sento come se Java potesse aggiungere un vincolo come questo. Fammi sapere se questa domanda potrebbe essere più chiara.

Modifica: Grazie ragazzi, le risposte stanno aiutando e stanno arrivando a quello che sospettavo. Sembra che il type checker non sia in grado di gestire ciò che mi piacerebbe fare senza UndecidableInstances, quindi la mia domanda è, è ciò che vorrei esprimere davvero indecidibile? È per il compilatore Haskell, ma è in generale? cioè potrebbe esistere un vincolo che significa "verificare che Return n sia un'istanza di Num" che è decidibile per un controllo di tipo più avanzato?

Answer 1

In realtà, si può fare esattamente ciò che lei ha citato:

{-# 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 è certamente un tipo, che può essere un'istanza di una classe proprio come Int can. La tua confusione potrebbe riguardare ciò che può essere l'argomento di un vincolo. La risposta è "qualsiasi cosa abbia il tipo corretto". Il tipo di Int è *, come il tipo di Return n. Num ha tipo * -> Constraint, quindi qualsiasi cosa di tipo * può essere la sua argomentazione. È perfettamente legale (anche se vuoto) scrivere Num Int come vincolo, nello stesso modo in cui è legale Num (a :: *).

Answer 2

Per completare la risposta di Eric, Mi permetto di suggerire una possibile alternativa: usando una dipendenza funzionale, invece di una famiglia tipo:

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) 

Questo lo rende un po 'più facile per parlare del tipo di risultato, credo.Per esempio, è possibile scrivere

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

È inoltre possibile utilizzare ConstraintKinds di applicare questa parte (che è il motivo per cui ho messo gli argomenti in questo ordine buffo):

type GivesInt = EvaluableFD Int 

Si potrebbe fare questo con la tua classe, ma sarebbe più fastidioso:

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