2012-09-04 18 views
12

Real World Haskell ha questo esempio:GHC può avvisare se l'istanza della classe è un ciclo?

class BasicEq3 a where 
    isEqual3 :: a -> a -> Bool 
    isEqual3 x y = not (isNotEqual3 x y) 

    isNotEqual3 :: a -> a -> Bool 
    isNotEqual3 x y = not (isEqual3 x y) 

instance BasicEq3 Bool 

E quando l'eseguo in GHCI:

#> isEqual3 False False 
out of memory 

Quindi, è necessario implementare almeno uno dei 2 metodi o sarà loop. E tu hai la flessibilità di scegliere quale, che è pulito.

La domanda che ho è, c'è un modo per ottenere un avvertimento o qualcosa del genere se non ha sovrascritto abbastanza dei valori predefiniti e le impostazioni predefinite formano un ciclo? Mi sembra strano che il compilatore che è così pazzo intelligente stia bene con questo esempio.

risposta

12

Penso che sia perfettamente corretto per GHC emettere un avviso in caso di dipendenza ciclica "ininterrotta". C'è anche un biglietto su queste linee: http://hackage.haskell.org/trac/ghc/ticket/6028

Solo perché qualcosa è "indecidibile" non significa che nessuna istanza del problema possa essere risolta in modo efficace. GHC (o qualsiasi altro compilatore Haskell) ha già un bel po 'di informazioni di cui ha bisogno, e sarebbe perfettamente possibile che emettesse un avvertimento se l'utente istanziava una classe senza "interrompere" la dipendenza ciclica. E se il compilatore si sbaglia nei casi rari come esemplificato nei post precedenti, l'utente può avere un -nowarnundefinedcyclicmethods o un meccanismo simile per dire a GHC di essere tranquillo. In quasi tutti gli altri casi, l'avvertimento sarà ben accetto e aggiungerebbe alla produttività del programmatore; evitando quello che è quasi sempre un insetto stupido.

+0

Sì! Nel caso del problema dell'arresto, le lingue globali come Agda dimostrano che i problemi irrisolvibili in generale possono avere sottoinsiemi solvibili grandi e interessanti. –

+0

"" Semplicemente indecidibile "non è un criterio sufficiente per liquidare in modo inavvertito una tecnica di compilazione: la maggior parte dei problemi indecidibili che sono indecidibili nel caso generale sono abbastanza decidibili in casi specifici." http://c2.com/cgi/wiki?SufficientlySmartCompiler –

+0

Il ticket trac è stato chiuso per un motivo priva di senso: qualcuno potrebbe definire un'istanza 'Num' senza' -' o 'negate' ma dove' + 'non valuta il suo secondo argomento, quindi la sua definizione apparentemente circolare finirà bene. Questo secondo argomento, sempre scartato, è l'unico modo per uscire dalla non-terminazione senza definire '-' o' negate'. Penso che questi siano casi d'uso bizzarri, ed è bene dover specificare '-noarnundefinedcyclicmethods 'se si vuole sfuggire alle definizioni circolari usando' _'. Non ho idea di come aumentare quello su Trac. – AndrewC

12

No, ho paura che GHC non faccia nulla del genere. Anche questo non è possibile in generale.

Vedete, i metodi di una classe di tipo potrebbero essere reciprocamente ricorsivi in ​​un modo utile. Ecco un esempio forzato di una classe di questo tipo. È perfettamente corretto non definire né sumOddssumEvens, anche se le loro implementazioni predefinite sono in termini l'una dell'altra.

class Weird a where 
    measure :: a -> Int 

    sumOdds :: [a] -> Int 
    sumOdds [] = 0 
    sumOdds (_:xs) = sumEvens xs 

    sumEvens :: [a] -> Int 
    sumEvens [] = 0 
    sumEvens (x:xs) = measure x + sumOdds xs 
+0

Interessante, non ci avevo mai pensato. –

+0

In effetti, molte classi standard lo fanno ('Ord', per esempio). Ecco da dove viene la "definizione completa minima". –

+2

Intendevi mutuamente ricorsivo? Corecursive è diverso – nponeccop

2

Non credo. Mi preoccupo che ti aspetti che il compilatore risolva il problema dell'arresto! Solo perché due funzioni sono definite in termini l'una dell'altra, non significa che sia una cattiva classe predefinita. Inoltre, ho usato lezioni in passato in cui avevo solo bisogno di scrivere instance MyClass MyType per aggiungere funzionalità utili. Quindi chiedere al compilatore di avvertirti su quella classe è chiedere di lamentarsi di un altro codice valido.

[Naturalmente, usa ghci durante lo sviluppo e prova ogni funzione dopo averla scritta! Usa HUnit e/o QuickCheck, solo per assicurarsi che nessuno di questa roba finisce in codice finale.]

6

No, non è, in quanto se il compilatore potrebbe fare questa determinazione, che sarebbe equivalente a risolvere il Fermare il problema. In generale, il fatto che due funzioni si chiamino a vicenda in un pattern di "loop" non è sufficiente per concludere che effettivamente chiamare una delle funzioni risulterà in un loop.

Per usare un esempio (forzato),

collatzOdd :: Int -> Int 
collatzOdd 1 = 1 
collatzOdd n = let n' = 3*n+1 in if n' `mod` 2 == 0 then collatzEven n' 
            else collatzOdd n' 

collatzEven :: Int -> Int 
collatzEven n = let n' = n `div` 2 in if n' `mod` 2 == 0 then collatzEven n' 
             else collatzOdd n' 

collatz :: Int -> Int 
collatz n = if n `mod` 2 == 0 then collatzEven n else collatzOdd n 

(Questo è, naturalmente, non è il modo più naturale per l'attuazione del Collatz conjecture, ma illustra le funzioni mutuamente ricorsive.)

Ora collatzEven e collatzOdd dipendono l'uno dall'altro, ma la congettura di Collatz afferma che la chiamata collatz termina per tutti i positivi n. Se GHC potesse determinare se una classe che aveva collatzOdd e collatzEven come definizioni predefinite avesse o meno una definizione completa, allora GHC sarebbe in grado di risolvere la congettura di Collatz! (Questo non è ovviamente una prova della non decifrabilità del problema di stallo, ma dovrebbe illustrare perché determinare se un insieme di funzioni reciprocamente ricorsive sia ben definito non è affatto banale come potrebbe sembrare.)

In in generale, poiché GHC non può determinarlo automaticamente, la documentazione per le classi Haskell fornirà la "definizione completa minima" necessaria per creare un'istanza di una classe.

+8

Sarebbe bello se ci fosse un modo per specificare la definizione completa minima in modo tale che il compilatore potesse controllarlo, comunque. – hammar

+0

Questo è un buon punto - forse un pragma del compilatore con la definizione della classe. – AndrewC

2

Secondo la mia opinione personale, il meccanismo inadempiente è inutile e imprudente. Sarebbe facile per l'autore di classe per fornire solo le impostazioni predefinite come funzioni ordinarie:

notEq3FromEq3 :: (a -> a -> Bool) -> (a -> a -> Bool) 
notEq3FromEq3 eq3 = (\x y -> not (eq3 x y)) 

eq3FromNotEq3 :: (a -> a -> Bool) -> (a -> a -> Bool) 
eq3FromNotEq3 ne3 = (\x y -> not (ne3 x y)) 

(In realtà, queste due definizioni sono uguali, ma questo non sarebbe vero in generale). Quindi un'istanza è simile a:

instance BasicEq3 Bool where 
    isEqual3 True True = True 
    isEqual3 False False = True 
    isEqual3 _ _ = False 

    isNotEqual3 = notEq3FromEq3 isEqual3 

e non sono richiesti valori predefiniti. Quindi GHC può avvisarti se non fornisci la definizione, e qualsiasi loop spiacevole deve essere scritto esplicitamente da te nel tuo codice.

Ciò elimina la possibilità di aggiungere nuovi metodi a una classe con definizioni predefinite senza influire sulle istanze esistenti, ma non è un vantaggio enorme a mio avviso. L'approccio di cui sopra è anche in linea di massima più flessibile: potresti ad es. fornire funzioni che consentano a un'istanza Ord di scegliere qualsiasi operatore di confronto da implementare.

Problemi correlati