OCaml: Esiste una funzione con tipo 'a ->' a differenza della funzione di identità?

Question

Questa non è una domanda a casa, a proposito. È stato educato in classe, ma il mio insegnante non ha potuto pensarne. Grazie.

Answer 1

Come si fa a definire le funzioni di identità? Se state pensando solo la sintassi, ci sono diverse funzioni di identità, che hanno tutti il ​​tipo corretto:

let f x = x 
let f2 x = (fun y -> y) x 
let f3 x = (fun y -> y) (fun y -> y) x 
let f4 x = (fun y -> (fun y -> y) y) x 
let f5 x = (fun y z -> z) x x 
let f6 x = if false then x else x 

ci sono funzioni anche più strane:

let f7 x = if Random.bool() then x else x 
let f8 x = if Sys.argv < 5 then x else x 

Se si limita a voi stessi di un sottoinsieme puro di OCaml (che esclude F7 e F8), tutte le funzioni si può costruire verificare un'equazione osservazionale che assicura, in un certo senso, che quello che calcolano è l'identità: per ogni valore f : 'a -> 'a, abbiamo che f x = x

Questa equazione non dipende dalla funzione specifica, è determinata in modo univoco dal tipo. Esistono diversi teoremi (inquadrati in contesti diversi) che formalizzano l'idea informale che "una funzione polimorfa non può cambiare un parametro di tipo polimorfico, passarlo solo in giro". Vedi ad esempio la carta di Philip Wadler, Theorems for free!.

La cosa bella con questi teoremi è che non si applicano solo al caso 'a -> 'a, il che non è molto interessante. È possibile ottenere un teorema dal tipo ('a -> 'a -> bool) -> 'a list -> 'a list di una funzione di ordinamento, che indica che la sua applicazione commuta con la mappatura di una funzione monotona. Più formalmente, se avete qualsiasi funzione s con un tale tipo, quindi per tutti i tipi u, v, funzioni cmp_u : u -> u -> bool, cmp_v : v -> v -> bool, f : u -> v, e la lista li : u list, e se cmp_u u u' implica cmp_v (f u) (f u') (f è monotona), si ha:

map f (s cmp_u li) = s cmp_v (map f li) 

Questo è vero quando s è esattamente una funzione di ordinamento, ma trovo impressionante poter dimostrare che è vero per qualsiasi funzione s con lo stesso tipo.

Una volta che consentirà non-terminazione, sia divergente (loop a tempo indeterminato, come con la let rec f x = f x funzione di cui sopra), o aumentando eccezioni, naturalmente, si può avere tutto: si può costruire una funzione di tipo 'a -> 'b e tipi non intendo più nulla L'utilizzo di Obj.magic : 'a -> 'b ha lo stesso effetto.

Esistono modi più sicuri per perdere l'equivalenza dell'identità: è possibile lavorare all'interno di un ambiente non vuoto, con valori predefiniti accessibili dalla funzione. Si consideri ad esempio la seguente funzione:

let counter = ref 0 
let f x = incr counter; x 

È ancora che la proprietà che per ogni x, f x = x: se si considera solo il valore di ritorno, la funzione si comporta ancora come l'identità. Ma una volta considerati gli effetti collaterali, non sei più equivalente all'identità (senza effetti collaterali): se conosco counter, posso scrivere una funzione di separazione che restituisce true quando viene assegnata questa funzione f e restituisce false per pure funzioni identitarie.

let separate g = 
    let before = !counter in 
    g(); 
    !counter = before + 1 

Se il contatore è nascosto (ad esempio da un modulo di firma, o semplicemente let f = let counter = ... in fun x -> ...), e nessun altra funzione può osservare, quindi abbiamo ancora una volta non possiamo distinguere f e le funzioni di pura identità. Quindi la storia è molto più sottile in presenza dello stato locale.

Answer 2

let rec f x = f (f x) 

Questa funzione non termina mai, ma ha il tipo 'a -> 'a.

Se si accettano solo funzioni totali, la domanda diventa più interessante. Senza usare i trucchi del male, non è possibile scrivere una funzione totale di tipo 'a -> 'a, ma trucchi malvagi sono così divertente:

let f (x:'a):'a = Obj.magic 42 

Obj.magic è un abominio male di tipo 'a -> 'b che consente a tutti i tipi di imbrogli per aggirare il sistema di tipo .

Pensare che uno non sia totale o perché si bloccherà se utilizzato con tipi di box.

Quindi la vera risposta è: la funzione di identità è l'unica funzione totale di tipo 'a -> 'a.

Answer 3

un'eccezione può anche dare un tipo di 'a -> 'a:

# let f (x:'a) : 'a = raise (Failure "aaa");; 
val f : 'a -> 'a = <fun> 

Answer 4

Se ci si limita a un calcolo λ tipicamente fortemente "normalizzato" fortemente normalizzato, esiste una singola funzione di tipo ∀α α → α, che è la funzione di identità. Puoi dimostrarlo esaminando le possibili forme normali di un termine di questo tipo.

L'articolo "Theorems for Free" di Philip Wadler del 1989 spiega come funzioni con tipi polimorfici soddisfino necessariamente determinati teoremi (ad esempio, una funzione simile a una mappa commuta con la composizione).

Ci sono tuttavia alcuni problemi non intuitivi quando si tratta di molto polimorfismo. Ad esempio, esiste un trucco standard per codificare i tipi induttivi e la ricorsione con polimorfismo impredicativo, rappresentando un oggetto induttivo (ad esempio una lista) utilizzando la sua funzione di ricorsività. In alcuni casi, esistono termini appartenenti al tipo di funzione del ricorsore che non sono funzioni del ricorsore; c'è un esempio in §4.3.1 di Christine Paulin's PhD thesis.