Idrisの怠惰な評価について混乱しました

Question

公式のIdrisチュートリアルのいくつかの例を読んで遊んでいると、怠惰な評価に関してちょっと混乱しました。イドリスが先行評価を使用してチュートリアルに記載された、および遅延評価を使用して、彼らはこれが

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

適切ではない例を与えるために行くと、彼らはその後、一例を示すように進むと

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

私は読んでいる間に物事を試してみたいので、非怠け者と怠惰な人をテストするための非効率なフィボナッチ関数を作成しましたifThenElse。イドリスが先行評価を実施しなければならないことを考えると

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) 

、私はiftest1の実行がTrueに適用しても(fibo 25)によって減速することが予想されます。ただし、Trueに適用すると、iftest1とiftest2の両方が非常に高速に実行されます。だから、怠け者/熱心に対する私の理解は根本的に欠陥がありますか？

Idrisの怠惰と熱意の違いを観察する良い例は何ですか？

Answer 1

おそらくとiftest2をIdris REPLから試しました。 The REPL uses different evaluation order than compiled code：

完全に依存型言語であるため、Idrisには2つの段階があり、コンパイル時と実行時を評価します。コンパイル時には、タイプチェックを決定可能にするために、完全であることが分かっているもの（つまり、すべての可能な入力を終了してカバーするもの）だけを評価します。コンパイル時のエバリュエータはIdrisカーネルの一部であり、HOAS（高次抽象構文）形式の値表現を使用してHaskellで実装されています。ここではすべてが通常の形をしていることが分かっているので、評価方法は実際には重要ではありません。なぜなら、どちらの方法でも同じ答えが得られ、実際にはHaskellのランタイムシステムが何をしようとしても何もしないからです。

便宜上、REPLは評価のコンパイル時の概念を使用します。