Idris eifrig Bewertung

Question

In Haskell, könnte ich if wie folgt implementieren:

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

Diese verhält, wie ich erwarte, dass:

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

---

In Racket, konnte ich implementieren Sie eine fehlerhafte if wie folgt:

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

Diese verhält, wie ich erwarte, dass:

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

---

In Idris, könnte ich if wie folgt implementieren:

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

Dieses Verhalten surpris ES mich:

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

ich Irdis wie Racket verhalten erwartet, wo beide Argumente sind ausgewertet. Aber das ist nicht der Fall!

Wie entscheidet Idris, wann die Dinge bewertet werden?

Answer 1

Wir sagen Idris hat strenge Bewertung, aber das ist für seine Laufzeit Semantik.

Idris ist eine vollständig abhängige Programmiersprache und hat zwei Phasen, in denen es Dinge, Kompilierzeit und Laufzeit auswertet. Zur Kompilierungszeit wird es nur Dinge auswerten, von denen es weiß, dass sie vollständig sind (d. H. Alle möglichen Eingaben beenden und abdecken), um die Typüberprüfung entscheidbar zu halten. Der Kompilierzeit-Evaluator ist Teil des Idris-Kernels und wird in Haskell unter Verwendung einer HOAS-Stildarstellung (höhere abstrakte Syntax) von Werten implementiert. Da hier bekannt ist, dass alles eine normale Form hat, spielt die Auswertungsstrategie keine Rolle, da sie in jedem Fall die gleiche Antwort erhält und in der Praxis das tut, was das Haskell-Laufzeitsystem wählt.

Die REPL verwendet zur Vereinfachung den Übersetzungsbegriff der Auswertung. Also wird Ihr 'Spin 1000' nie wirklich ausgewertet. Wenn Sie eine ausführbare Datei mit demselben Code erstellen, würde ich ein sehr unterschiedliches Verhalten erwarten.

Neben der einfacheren Implementierung (da der Evaluator verfügbar ist) kann dies sehr hilfreich sein, um zu zeigen, wie Terme im Type Checker ausgewertet werden. So können Sie den Unterschied zwischen sehen:

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 

Dies wäre schwieriger (wenn auch nicht unmöglich), wenn wir die Laufzeitauswertung in der REPL verwendet, die nicht unter Lambda-Ausdrücke nicht verringert.