verwirrt über faul Bewertung in Idris

Question

Lesen und spielen mit einigen Beispielen aus dem offiziellen Idris Tutorial hat mich ein bisschen verwirrt in Bezug auf faul Bewertung.

Wie in der Anleitung angegeben Idris eifrig Auswertung verwendet, und sie gehen auf ein Beispiel zu geben, wo dies nicht

ifThenElse : Bool -> a -> a -> a 
ifThenElse True t e = t 
ifThenElse False t e = e 

Und sie dann gehen angemessen wäre ein Beispiel unter Verwendung von lazy evaluation zeigen

ifThenElse : Bool -> Lazy a -> Lazy a -> a 
ifThenElse True t e = t 
ifThenElse False t e = e 

Ich mag Dinge beim Lesen ausprobieren, also habe ich eine ineffiziente Fibonacci-Funktion erstellt, um die nicht faulen und faulen ifThenElse zu testen.

fibo : Nat -> Nat 
fibo Z = Z 
fibo (S Z) = S Z 
fibo (S(S Z)) = S(S Z) 
fibo (S(S(S n))) = fibo (S(S n)) + fibo (S n) 

-- the non lazy 
ifThenElse1 : Bool -> (t: a) -> (f: a) -> a 
ifThenElse1 False t f = f 
ifThenElse1 True t f = t 

-- should be slow when applied to True 
iftest1 : Bool -> Nat 
iftest1 b = ifThenElse1 b (fibo 5) (fibo 25) 

-- the lazy 
ifThenElse2 : Bool -> (t: Lazy a) -> (f: Lazy a) -> a 
ifThenElse2 False t f = f 
ifThenElse2 True t f = t 

-- should be fast when applied to True 
iftest2 : Bool -> Nat 
iftest2 b = ifThenElse2 b (fibo 5) (fibo 25) 

Da Idris eifrig Auswertung durchführen sollte, ich die Ausführung von iftest1 erwarten würde sogar von (fibo 25) verlangsamt werden, wenn auf True angewendet. Sowohl iftest1 als auch iftest2 werden jedoch sehr schnell ausgeführt, wenn sie auf True angewendet werden. Vielleicht ist mein Verständnis von Faulheit/Eifer grundlegend fehlerhaft?

Was ist ein gutes Beispiel, um den Unterschied zwischen Faulheit und Eifer in Idris zu beobachten?

Answer 1

Sie haben wahrscheinlich versucht iftest1 und iftest2 von der Idris REPL. The REPL uses different evaluation order than compiled code:

Da Idris eine vollständig abhängige Programmiersprache ist, hat sie zwei Phasen, in denen sie Dinge, Kompilierzeit und Laufzeit auswertet. Zur Kompilierungszeit wird es nur Dinge evaluieren, 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 auch immer das Haskell-Laufzeitsystem tut.

Die REPL verwendet zur Vereinfachung den Übersetzungsbegriff der Auswertung.