Come capire se una funzione F # è pura?

Question

Supponiamo di avere queste due F # funzioni:

let sq x = x*x 

let tm = DateTime.Now 

sq Chiaramente è puro in quanto verrà sempre restituisce lo stesso valore per un dato ingresso mentre tm è impuro perché restituirà un valore diverso ogni volta che viene chiamato .

In generale c'è un modo per determinare se una particolare funzione in F # è pura o impura senza analizzare ciò che fa, in altre parole la si legge riga per riga?

In alternativa c'è un modo per annotare una funzione per dire al compilatore che la funzione è pura o impura quando la scrivi?

Infine quando si chiama una funzione che fa parte del Common Language Runtime (come DateTime) come si può dire se è pura o impura senza provarla?

Nota: da "puro" intendo la definizione da Wikipedia: http://en.wikipedia.org/wiki/Pure_function (permalink)

Nella programmazione di computer, una funzione può essere descritto come puro se entrambi queste affermazioni circa la funzione Hold:

1. La funzione valuta sempre lo stesso valore di risultato dato lo stesso valore valore/i. Il valore del risultato della funzione non può dipendere da qualsiasi informazione o stato nascosto che può cambiare come esecuzione del programma proventi o tra diverse esecuzioni del programma, né può dipendere da qualsiasi ingresso esterno dai dispositivi I/O.

2. Valutazione del risultato non causa alcun effetto osservabile semanticamente o lato uscita , come mutazione di oggetti mutabili o uscita ai dispositivi di I/O.

Answer 1

F # non fornisce tutte le funzioni e gli strumenti per la verifica che i metodi sono puri, quindi una semplice risposta è che si controlla questa proprietà da soli.

Al di fuori di F #, vale la pena notare che Code Contracts biblioteca ha una nozione di metodi puri (e possono essere marcato con PureAttribute), ma non sono del tutto sicuro che cosa è la storia di controllo lì. Penso che i Contratti di codice siano dotati di un controllo statico che analizza IL (e dovrebbe funzionare anche per F #), ma questo è un compito abbastanza difficile, quindi mi aspetterei che sia piuttosto limitato. Tuttavia, lo PureAttribute viene utilizzato su alcuni metodi BCL, quindi è possibile affermare che alcuni metodi .NET standard sono puri.

Answer 2

Tecnicamente parlando il valore 'tm' non è una funzione, ma il valore di tipo DateTime ed è immutabile, quindi ogni volta che si valuta questo valore dopo averlo creato sarà sempre lo stesso.

Answer 3

Dato che è possibile definire entrambe le funzioni pure e inpure in f #, sarei sorpreso se esistesse un algoritmo in grado di controllare il codice f # (definizioni di funzioni) per la purezza - il controllo del codice del programma per le proprietà semantiche è generalmente indecidibile dal teorema di Rice.