Idrisは本当に「厳密に評価されていますか？

Question

ハスケルから来て、私は怠惰（非厳密性）に関するIdrisの話を読んでいました。私はそれを実行し、それが働いた

myFact : Int -> Int 
myFact n = myIf (n == 1) 1 (n * myFact (n-1)) 

それをテストするための簡単な階乗関数を書いた最近のリリースノートをtrolled、そして次

myIf : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a 
myIf True t e = t 
myIf False t e = e 

に似found code！私は

myIf : (b : Bool) -> a -> a -> a 

へmyIfの型シグネチャを変更することによって、それを破ることにしました

> myFact 5 
120 : Int 

私はidris REPLを再読み込み、および無限再帰を期待して再びmyFact 5を走りました。私の驚いたことに、それは同じように働いた！

idrisは厳密性を避けるべきであると考えていますか？なぜこれは永遠に繰り返されませんでしたか？

私はイドリス0.9.15を使用していないし、今と連動債とのリリースノートのどれも、すべての変更を言及。よ（AT型チェッカーは、未知の値の存在下で式を評価するために必要な時間をコンパイルするので、必ずしもそう）時間をコンパイルし、時間評価のセマンティクスが異なる実行http://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-expect-what-s-going-on

、およびREPLは次のとおりです。

Answer 1

の説明はこちらコンパイル時の概念を利便性のために使用したり、式チェッカーで式がどのように減少するかを見るのに便利です。

しかし、ここでもう少し進んでいます。 IdrisはmyIfが非常に小さい機能であり、それをインラインにすることを決めたことを発見しました。イドリスはとにかくたかった制御構造にコンパイルされますので、だから、一般的に物事Lazyを行うことを気にすることなく、myIfのような制御構造を記述することができ

myFact x = case x == 1 of 
       True => 1 
       False => x * myFact (x - 1) 

：myFactをコンパイルしたときに、実際のようなビットに見えるの定義を持っています。同じことが起こります。 &&および||と短絡しています。