Perché il tipo di questa funzione (a -> a) -> a?

Question

Perché il tipo di questa funzione (a -> a) -> a?

Prelude> let y f = f (y f) 
Prelude> :t y 
y :: (t -> t) -> t 

Non dovrebbe essere un tipo infinito/ricorsivo? Stavo per cercare di esprimere a parole quello che penso dovrebbe essere il tipo, ma non posso farlo per qualche motivo.

y :: (t -> t) -> ?WTFIsGoingOnOnTheRHS? 

Non capisco come f (y f) si risolve in un valore. Quanto segue fa un po 'più di senso per me:

Prelude> let y f x = f (y f) x 
Prelude> :t y 
y :: ((a -> b) -> a -> b) -> a -> b 

Ma è ancora ridicolmente confusa. Cosa sta succedendo?

Answer 1

Beh, y deve essere di tipo (a -> b) -> c, per alcuni a, b e c non sappiamo ancora; dopo tutto, prende una funzione, f, e la applica a un argomento, quindi deve essere una funzione che accetta una funzione.

Dal y f = f x (ancora una volta, per alcuni x), sappiamo che il tipo di ritorno di y deve essere il tipo di ritorno di f stessa. Quindi, possiamo perfezionare il tipo di un po ': deve essere (a -> b) -> b per alcuni a e che non conosciamo ancora.

Per capire che cos'è a, dobbiamo solo guardare il tipo di valore passato a f. È y f, che è l'espressione che stiamo cercando di capire il tipo di adesso. Stiamo dicendo che il tipo di è (a -> b) -> b (per alcuni a, , ecc.), Quindi possiamo dire che questa applicazione di y f deve essere di tipo .

Quindi, il tipo dell'argomento su f è b. Rimettiamo tutto insieme e otteniamo (b -> b) -> b - che è, ovviamente, la stessa cosa di (a -> a) -> a.

Ecco una visione più intuitiva, ma meno preciso delle cose: stiamo dicendo che y f = f (y f), che siamo in grado di espandersi per l'equivalente y f = f (f (y f)), y f = f (f (f (y f))), e così via. Quindi, sappiamo che possiamo sempre applicare un altro f a tutto il resto, e poiché "l'intera cosa" in questione è il risultato dell'applicazione di f a un argomento, f deve avere il tipo a -> a; e poiché abbiamo appena concluso che il tutto è il risultato dell'applicazione di f a un argomento, il tipo restituito di deve essere quello di f stesso - riunito, di nuovo, come (a -> a) -> a.

Answer 2

@ ehird ha fatto un buon lavoro di spiegazione del tipo, quindi mi piacerebbe mostrare come può risolvere un valore con alcuni esempi.

f1 :: Int -> Int 
f1 _ = 5 

-- expansion of y applied to f1 
y f1 
f1 (y f1) -- definition of y 
5   -- definition of f1 (the argument is ignored) 

-- here's an example that uses the argument, a factorial function 
fac :: (Int -> Int) -> (Int -> Int) 
fac next 1 = 1 
fac next n = n * next (n-1) 

y fac :: Int -> Int 
fac (y fac) -- def. of y 
    -- at this point, further evaluation requires the next argument 
    -- so let's try 3 
fac (y fac) 3 :: Int 
3 * (y fac) 2    -- def. of fac 
3 * (fac (y fac) 2)  -- def. of y 
3 * (2 * (y fac) 1)  -- def. of fac 
3 * (2 * (fac (y fac) 1) -- def. of y 
3 * (2 * 1)    -- def. of fac 

È possibile seguire la stessa procedura con qualsiasi funzione vi piace vedere cosa accadrà. Entrambi questi esempi convergono in valori, ma ciò non sempre accade.

Answer 3

Lasciami parlare di un combinatore.Si chiama il "punto fisso combinatore" e ha la seguente proprietà:

La proprietà: il "punto fisso combinatore" prende una funzione f :: (a -> a) e scopre un "punto fisso" x :: a di tale funzione in modo tale che f x == x. Alcune implementazioni del combinatore di punti di fissazione potrebbero essere migliori o peggiori in "scoperta", ma supponendo che termini, produrrà un punto fisso della funzione di input. Qualsiasi funzione che soddisfi la proprietà può essere chiamata "combinatore di punti fissi".

Chiamare questo "combinatore di punti di correzione" . Sulla base di quanto abbiamo appena detto, sono vere le seguenti affermazioni:

-- as we said, y's input is f :: a -> a, and its output is x :: a, therefore 
y :: (a -> a) -> a 

-- let x be the fixed point discovered by applying f to y 
y f == x -- because y discovers x, a fixed point of f, per The Property 
f x == x -- the behavior of a fixed point, per The Property 

-- now, per substitution of "x" with "f x" in "y f == x" 
y f == f x 
-- again, per substitution of "x" with "y f" in the previous line 
y f == f (y f) 

Quindi eccoci. Hai definito in termini di proprietà essenziale del combinatore di punti di fissazione:
y f == f (y f). Invece di supporre che y f scopra x, si può supporre che x rappresenti un calcolo divergente, e giunga sempre alla stessa conclusione (iinm).

Poiché la funzione soddisfa la proprietà, possiamo concludere che si tratta di un combinatore di punti fissi e che le altre proprietà che abbiamo dichiarato, incluso il tipo, sono applicabili alla vostra funzione.

Questo non è esattamente una prova solida, ma spero che fornisca ulteriori informazioni.

Answer 4

Solo due punti da aggiungere alle risposte di altre persone.

La funzione che si sta definendo è solitamente denominata fix ed è una fixed-point combinator: una funzione che calcola il fixed point di un'altra funzione. In matematica, il punto fisso di una funzione f è un argomento x tale che f x = x. Questo consente già di dedurre che il tipo di fix deve essere (a -> a) -> a; "funzione che prende una funzione da a a a e restituisce un a."

Hai chiamato la funzione y, che sembra essere dopo la Y combinator, ma questo è un nome imprecisa: il combinatore Y è uno specifico combinatore punto fisso, ma non è la stessa di quella che hai definito Qui.

Non capisco come f (y f) si risolve in un valore.

Bene, il trucco è che Haskell è un linguaggio non rigido (a.k.a. "pigro"). Il calcolo di f (y f) può terminare se f non ha bisogno di valutare l'argomento y f in tutti i casi. Quindi, se stai definendo fattoriale (come illustra John L), fac (y fac) 1 valuta 1 senza valutare y fac.

Strict lingue non possono farlo, quindi in quelle lingue non è possibile definire un combinatore a virgola fissa in questo modo. In quelle lingue, il combinatore a virgola fissa da manuale è il combinatore Y corretto.