Perché GHC rende la correzione così confusa?

Question

Guardando il codice sorgente di GHC posso vedere che la definizione per correzione è:

fix :: (a -> a) -> a 
fix f = let x = f x in x 

In un esempio correzione viene usato in questo modo:

fix (\f x -> let x' = x+1 in x:f x') 

questo produce fondamentalmente una sequenza di numeri che aumentano di un'unità all'infinito. Perché ciò avvenga la correzione deve essere in corso la funzione che riceva proprio a quella stessa funzione come primo parametro. Non è chiaro per me come potrebbe essere la definizione di correggere elencata sopra.

Questa definizione è come sono arrivato a capire come correzione opere:

fix :: (a -> a) -> a 
fix f = f (fix f) 

Così ora ho due domande:

1. Come si fa x mai venuto a significare correzione x nella prima definizione?
2. C'è qualche vantaggio nell'usare la prima definizione sul secondo?

Answer 1

È facile vedere come funziona questa definizione applicando il ragionamento equo.

fix :: (a -> a) -> a 
fix f = let x = f x in x 

Cosa x valutare a quando cerchiamo di valutare fix f? È definito come f x, quindi fix f = f x. Ma che cos'è x qui? È f x, proprio come prima. Quindi ottieni fix f = f x = f (f x). Ragionando in questo modo si ottiene una catena infinita di applicazioni di f: fix f = f (f (f (f ...))).

Ora, sostituendo (\f x -> let x' = x+1 in x:f x') per f si ottiene

fix (\f x -> let x' = x+1 in x:f x') 
    = (\f x -> let x' = x+1 in x:f x') (f ...) 
    = (\x -> let x' = x+1 in x:((f ...) x')) 
    = (\x -> x:((f ...) x + 1)) 
    = (\x -> x:((\x -> let x' = x+1 in x:(f ...) x') x + 1)) 
    = (\x -> x:((\x -> x:(f ...) x + 1) x + 1)) 
    = (\x -> x:(x + 1):((f ...) x + 1)) 
    = ... 

Edit: Per quanto riguarda la seconda domanda, @ is7s sottolineato nei commenti che la prima definizione è preferibile perché è più efficiente.

per scoprire perché, diamo un'occhiata al centro per fix1 (:1) !! 10^8:

a_r1Ko :: Type.Integer  
a_r1Ko = __integer 1 

main_x :: [Type.Integer] 
main_x = 
    : @ Type.Integer a_r1Ko main_x 

main3 :: Type.Integer 
main3 = 
    !!_sub @ Type.Integer main_x 100000000 

Come si può vedere, dopo le trasformazioni fix1 (1:) divennero essenzialmente main_x = 1 : main_x. Nota come questa definizione si riferisce a se stessa - questo è ciò che significa "legare il nodo".Questa auto-riferimento è rappresentato come un semplice riferimento indiretto puntatore in fase di esecuzione:

Ora diamo un'occhiata a fix2 (1:) !! 100000000:

main6 :: Type.Integer 
main6 = __integer 1 

main5 
    :: [Type.Integer] -> [Type.Integer] 
main5 = : @ Type.Integer main6 

main4 :: [Type.Integer] 
main4 = fix2 @ [Type.Integer] main5 

main3 :: Type.Integer 
main3 = 
    !!_sub @ Type.Integer main4 100000000 

Qui l'applicazione fix2 è in realtà conservato:

Il risultato è che il secondo prog ram ha bisogno di fare l'assegnazione per ogni elemento della lista (ma dal momento che l'elenco è immediatamente consumata, il programma ancora viene eseguito in modo efficace nello spazio costante):

$ ./Test2 +RTS -s 
    2,400,047,200 bytes allocated in the heap 
     133,012 bytes copied during GC 
      27,040 bytes maximum residency (1 sample(s)) 
      17,688 bytes maximum slop 
       1 MB total memory in use (0 MB lost due to fragmentation) 
[...] 

Confronti che, per il comportamento del primo programma:

$ ./Test1 +RTS -s   
      47,168 bytes allocated in the heap 
      1,756 bytes copied during GC 
      42,632 bytes maximum residency (1 sample(s)) 
      18,808 bytes maximum slop 
       1 MB total memory in use (0 MB lost due to fragmentation) 
[...] 

Answer 2

In che modo x giunge a significare fix x nella prima definizione?

fix f = let x = f x in x 

Let attacchi a Haskell sono ricorsivi

Prima di tutto, si rende conto che Haskell consente attacchi let ricorsive. Quello che Haskell chiama "let", alcuni altri linguaggi chiamano "letrec". Questo sembra abbastanza normale per le definizioni di funzione. Per esempio:

ghci> let fac n = if n == 0 then 1 else n * fac (n - 1) in fac 5 
120 

ma può sembrare piuttosto strano per le definizioni di valore. Tuttavia, i valori possono essere definiti ricorsivamente, a causa della non rigore di Haskell.

ghci> take 5 (let ones = 1 : ones in ones) 
[1,1,1,1,1] 

Vedi A gentle introduction to Haskell sezioni 3.3 e 3.4 per ulteriori elaborazioni su pigrizia di Haskell.

Thunk in GHC

In GHC, un'espressione non ancora non valutata è avvolto in un "thunk": una promessa per eseguire il calcolo. I thunk vengono valutati solo quando assolutamente devono essere. Supponiamo di voler fix someFunction. Secondo la definizione di fix, che è

let x = someFunction x in x 

Ora, che cosa vede GHC è qualcosa di simile.

let x = MAKE A THUNK in x 

Quindi ha felicemente un tonfo per voi e si muove a destra lungo fino a quando l'utente chiede di sapere che cosa in realtà è x.

valutazione Esempio

Tale espressione del thunk avviene solo per riferirsi a se stesso. Prendiamo l'esempio ones e lo riscriviamo per usare fix.

ghci> take 5 (let ones recur = 1 : recur in fix ones) 
[1,1,1,1,1] 

Quindi che aspetto avrà?
Possiamo incorporare ones come la funzione anonima \recur -> 1 : recur per una dimostrazione più chiara.

take 5 (fix (\recur -> 1 : recur)) 

-- expand definition of fix 
take 5 (let x = (\recur -> 1 : recur) x in x) 

Ora poi, che èx? Beh, anche se non siamo del tutto sicuri di cosa x è, possiamo ancora andare avanti con l'applicazione funzioni:

take 5 (let x = 1 : x in x) 

Ehi guarda, siamo tornati alla definizione che avevamo prima.

take 5 (let ones = 1 : ones in ones) 

Quindi, se si ritiene di capire come che si lavora, allora avete una buona sensazione di come fix opere.

---

C'è qualche vantaggio di utilizzare la prima definizione rispetto al secondo?

Sì. Il problema è che la seconda versione può causare una perdita di spazio , anche con le ottimizzazioni. Vedere GHC trac ticket #5205, per un problema simile con la definizione di forever. Questo è il motivo per cui ho parlato di thunk: perché let x = f x in x assegna solo un thunk: il thunk x.

Answer 3

La differenza è nella condivisione rispetto alla copia.

fix1 f = x where x = f x -- more visually apparent way to write the same thing 

fix2 f = f (fix2 f) 

Sostituendo la definizione in sé, entrambi sono ridotti come la stessa catena infinita applicazione f (f (f (f (f ...)))). Ma la prima definizione usa una denominazione esplicita; in Haskell (come nella maggior parte delle altre lingue) la condivisione è abilitata dalla possibilità di nominare le cose: un nome è più o meno garantito riferirsi a una "entità" (qui, x). La seconda definizione non garantisce alcuna condivisione - il risultato di una chiamata fix2 f viene sostituito nell'espressione, quindi potrebbe anche essere sostituito come un valore.

Ma un determinato compilatore potrebbe in teoria essere intelligente e utilizzare la condivisione anche nel secondo caso.

Il problema correlato è "combinatore Y". In tipizzato lambda calcolo dove non c'è denominazione costrutti (e quindi non sé -reference), Y combinatore emula angolo riferimento disponendo per la definizione da copiare, quindi riferendosi alla copia di sé diventa possibile. Ma nelle implementazioni che utilizzano il modello di ambiente per consentire le entità nominate in una lingua, diventa possibile il riferimento diretto per nome.

di vedere una differenza più drastica tra le due definizioni, confrontare

fibs1 = fix1 ((0:) . (1:) . g) where g (a:t@(b:_)) = (a+b):g t 
fibs2 = fix2 ((0:) . (1:) . g) where g (a:t@(b:_)) = (a+b):g t 

Vedi anche:

• In Scheme, how do you use lambda to create a recursive function?
• Y combinator discussion in "The Little Schemer"
• Can fold be used to create infinite lists?

(in particolare, provare a elaborare le ultime due definizioni nell'ultimo collegamento sopra riportato).

---

Lavorare dalle definizioni, per il tuo esempio fix (\g x -> let x2 = x+1 in x : g x2) otteniamo

fix1 (\g x -> let x2 = x+1 in x : g x2) 
= fix1 (\g x -> x : g (x+1)) 
= fix1 f where {f = \g x -> x : g (x+1)} 
= fix1 f where {f g x = x : g (x+1)} 
= x  where {x = f x ; f g x = x : g (x+1)} 
= g  where {g = f g ; f g x = x : g (x+1)} -- both g in {g = f g} are the same g 
= g  where {g = \x -> x : g (x+1)}   -- and so, here as well 
= g  where {g x = x : g (x+1)} 

e quindi una definizione ricorsiva adeguato per g è in realtà creato. (in quanto sopra, scriviamo ....x.... where {x = ...} per let {x = ...} in ....x...., per la leggibilità).

Ma la seconda derivazione procede con una distinzione cruciale di sostituire un valoreindietro, non un nome, come

fix2 (\g x -> x : g (x+1)) 
= fix2 f    where {f g x = x : g (x+1)} 
= f (fix2 f)   where {f g x = x : g (x+1)} 
= (\x-> x : g (x+1)) where {g = fix2 f ; f g x = x : g (x+1)} 
= h     where {h x = x : g (x+1) ; g = fix2 f ; f g x = x : g (x+1)} 

quindi la chiamata effettiva procede come ad esempio

take 3 $ fix2 (\g x -> x : g (x+1)) 10 
= take 3 (h 10)  where {h x = x : g (x+1) ; g = fix2 f ; f g x = x : g (x+1)} 
= take 3 (x:g (x+1)) where {x = 10 ;    g = fix2 f ; f g x = x : g (x+1)} 
= x:take 2 (g x2) where {x2 = x+1 ; x = 10 ; g = fix2 f ; f g x = x : g (x+1)} 
= x:take 2 (g x2) where {x2 = x+1 ; x = 10 ; g = f (fix2 f) ; f g x = x : g (x+1)} 
= x:take 2 (x2 : g2 (x2+1)) where {    g2 = fix2 f ; 
          x2 = x+1 ; x = 10 ;     f g x = x : g (x+1)} 
= ...... 

e vediamo che un nuovo vincolante (per g2) è stabilito qui, al posto di quello precedente (per g) essere riutilizzati con la definizione fix1.

Answer 4

Ho forse una spiegazione un po 'semplificata che deriva dall'ottimizzazione inlining. Se abbiamo

fix :: (a -> a) -> a 
fix f = f (fix f) 

poi fix è una funzione ricorsiva e questo significa che non può essere inline in luoghi in cui viene utilizzato (un INLINE pragma verrà ignorato, se dato).

Tuttavia

fix' f = let x = f x in x 

è non una funzione ricorsiva - non si è mai si definisce. Solo x all'interno è ricorsivo.Così, quando si chiama

fix' (\r x -> let x' = x+1 in x:r x') 

il compilatore può inline in

(\f -> (let y = f y in y)) (\r x -> let x' = x+1 in x:r x') 

e poi continuare a semplificare, ad esempio

let y = (\r x -> let x' = x+1 in x:r x') y in y 
let y = (\ x -> let x' = x+1 in x:y x') in y 

che è proprio come se la funzione sono stati definiti utilizzando lo standard notazione ricorsiva senza fix:

y  x = let x' = x+1 in x:y x'