Idris valutazione eager

Question

In Haskell, potrei implementare if come questo:

if' True x y = x 
if' False x y = y 
spin 0 =() 
spin n = spin (n - 1) 

Questo si comporta come mi aspetto:

haskell> if' True (spin 1000000)() -- takes a moment 
haskell> if' False (spin 1000000)() -- immediate 

---

In Racket, ho potuto implementare un if2 imperfetto in questo modo:

(define (if2 cond x y) (if cond x y)) 
(define (spin n) (if (= n 0) (void) (spin (- n 1)))) 

Questo si comporta come mi aspetto:

racket> (if2 #t (spin 100000000) (void)) -- takes a moment 
racket> (if2 #f (spin 100000000) (void)) -- takes a moment 

---

In Idris, potrei implementare if come questo:

if' : Bool -> a -> a -> a 
if' True x y = x 
if' False x y = y 
spin : Nat ->() 
spin Z =() 
spin (S n) = spin n 

Questo surpris comportamento Mi es:

idris> if' True (spin 1000)() -- takes a moment 
idris> if' False (spin 1000)() -- immediate 

mi aspettavo Irdis a comportarsi come Racket, dove entrambi gli argomenti sono valutati. Ma non è questo il caso!

Come decide Idris quando valutare le cose?

Answer 1

Diciamo che Idris ha una valutazione rigorosa, ma questa è per la sua semantica di runtime.

Essendo un linguaggio completamente tipizzato, Idris ha due fasi in cui valuta le cose, la compilazione e il tempo di esecuzione. In fase di compilazione valuterà solo le cose che sa essere totali (cioè terminando e coprendo tutti i possibili input) al fine di mantenere il controllo del tipo decidibile. Il valutatore di compilazione è parte del kernel di Idris ed è implementato in Haskell usando una rappresentazione di valori HOAS (sintassi astratta di ordine superiore). Poiché tutto è noto per avere una forma normale qui, la strategia di valutazione non conta in realtà perché in entrambi i casi otterrà la stessa risposta, e in pratica farà tutto ciò che il sistema run-time di Haskell sceglie di fare.

Il REPL, per comodità, utilizza la nozione di valutazione in fase di compilazione. Quindi, il tuo 'spin 1000' non viene mai realmente valutato. Se realizzi un eseguibile con lo stesso codice, mi aspetterei di vedere un comportamento molto diverso.

Oltre ad essere più facile da implementare (perché abbiamo a disposizione il programma di valutazione), questo può essere molto utile per mostrare come valutano i termini nel correttore di tipi. Così si può vedere la differenza tra:

Idris> \n, m => (S n) + m 
\n => \m => S (plus n m) : Nat -> Nat -> Nat 

Idris> \n, m => n + (S m) 
\n => \m => plus n (S m) : Nat -> Nat -> Nat 

Questo sarebbe più difficile (se non impossibile) se usassimo la valutazione di run-time al REPL, che non riduca in lambda.