इदरिस उत्सुक मूल्यांकन

Question

में हास्केल, मैं इस तरह if लागू हो सकता है:

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

यह बर्ताव करता है मैं कैसे उम्मीद:

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

---

रैकेट में, मैं कर सकता एक दोषपूर्ण if इस तरह लागू करें:

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

यह बर्ताव करता है मैं कैसे उम्मीद:

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

यह व्यवहार surpris:

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

---

में इदरिस, मैं if इस तरह लागू हो सकता है मुझे es:

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

मैं Irdis रैकेट, जहां दोनों बहस का मूल्यांकन कर रहे हैं की तरह व्यवहार की उम्मीद है। लेकिन यह मामला नहीं है!

इडिस कैसे निर्णय लेते हैं कि चीजों का मूल्यांकन कब किया जाए?

Answer 1

हम कहते हैं कि इडिस का सख्त मूल्यांकन है, लेकिन यह इसके रन-टाइम अर्थशास्त्र के लिए है।

पूरी तरह से निर्भर भाषा होने के नाते, इडिस के दो चरण हैं जहां यह चीजों, संकलन-समय और रन-टाइम का मूल्यांकन करता है। संकलन-समय पर यह केवल उन चीजों का मूल्यांकन करेगा जो कुल मिलाकर जानना चाहते हैं (यानी सभी संभावित इनपुट को समाप्त करना और कवर करना) ताकि टाइपिंग को जांचने योग्य बनाए रखा जा सके। संकलन-समय मूल्यांकनकर्ता इडिस कर्नेल का हिस्सा है, और इसे एचएएसएएस (उच्च क्रम सार वाक्यविन्यास) शैली मानों का प्रतिनिधित्व करते हुए हास्केल में कार्यान्वित किया जाता है। चूंकि सबकुछ यहां सामान्य रूप से जाना जाता है, इसलिए मूल्यांकन रणनीति वास्तव में कोई फर्क नहीं पड़ता क्योंकि किसी भी तरह से यह वही उत्तर प्राप्त करेगा, और व्यावहारिक रूप से यह जो भी होस्केल रन-टाइम सिस्टम करने के लिए करता है।

सुविधा के लिए आरईपीएल, मूल्यांकन की संकलन-समय धारणा का उपयोग करता है। तो, आपका 'स्पिन 1000' वास्तव में कभी मूल्यांकन नहीं किया जा रहा है। यदि आप एक ही कोड के साथ निष्पादन योग्य बनाते हैं, तो मैं बहुत अलग व्यवहार देखने की उम्मीद करता हूं।

साथ ही कार्यान्वित करने के लिए आसान होने के कारण (क्योंकि हमारे पास मूल्यांकनकर्ता उपलब्ध है) यह दिखाने के लिए बहुत उपयोगी हो सकता है कि प्रकार चेकर में शब्द कैसे मूल्यांकन करते हैं। तो अगर आप के बीच अंतर देख सकते हैं:

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 

यह कठिन होगा (हालांकि असंभव नहीं) अगर हम आरईपीएल, जो lambdas के तहत कम नहीं करता है पर रन-टाइम मूल्यांकन किया करते थे।