क्या इडिस वास्तव में "सख्ती से मूल्यांकन किया गया है?"

Question

हास्केल से आ रहा है, मैं आलसी की कहानी आलसी (गैर-कठोरता) के बारे में पढ़ रहा था। मैं हाल ही में रिलीज नोट्स trolled, और found code निम्नलिखित

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

जैसा मैं इसे

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

परीक्षण करने के लिए एक सरल भाज्य समारोह लिखा था मैं इसे भाग गया और यह काम किया!

> myFact 5 
120 : Int 

मैं

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

को myIf के प्रकार के हस्ताक्षर बदलकर इसे तोड़ने का फैसला किया मैं idris repl पुनः लोड, और myFact 5 भागा फिर से एक अनंत प्रत्यावर्तन की उम्मीद। मेरे आश्चर्य के लिए, यह अभी भी वैसे ही काम किया!

क्या कठोरता से बचने पर idris पता लगा सकता है? यह हमेशा के लिए क्यों नहीं?

मैं इडिस 0.9.15 का उपयोग कर रहा हूं और अब और लिंक किए गए नोट्स के बीच रिलीज नोट्स में से कोई भी, किसी भी बदलाव का उल्लेख नहीं करता है।

Answer 1

विवरण यहाँ है: http://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-expect-what-s-going-on

समय संकलित करें और चलाने के समय मूल्यांकन अर्थ विज्ञान अलग हैं (ताकि जरूरी है, क्योंकि पर समय प्रकार चेकर अज्ञात मूल्यों की उपस्थिति में भाव का मूल्यांकन करने की जरूरत है संकलन), और आरईपीएल है सुविधा के लिए दोनों संकलन समय धारणा का उपयोग करना और क्योंकि यह देखने के लिए उपयोगी है कि टाइपर प्रकार में अभिव्यक्ति कैसे कम हो जाती है।

हालांकि, यहां कुछ और चल रहा है। इडिस ने देखा है कि myIf एक बहुत छोटा काम है और उसने इसे रेखांकित करने का निर्णय लिया है। ,

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

तो आम तौर पर आप चीजों Lazy बनाने के बारे में चिंता किए बिना myIf तरह नियंत्रण संरचनाओं लिख सकते हैं क्योंकि इदरिस उन्हें नियंत्रण संरचना तुम वैसे भी चाहता था में संकलित होगा: तो जब myFact संकलित वास्तव में एक परिभाषा इस तरह एक सा लग रहा है। वही जाता है, उदा। && और || और लघु सर्किटिंग।