सबूत में प्राइमेटिव ऑपरेशंस

Question

निर्भर प्रकार सीखने के लिए, मैं इडिस में अपने पुराने हास्केल गेम को फिर से लिख रहा हूं। वर्तमान में गेम "इंजन" बिल्टिन अभिन्न प्रकारों का उपयोग करता है, जैसे Word8। मैं कुछ संख्याओं को उन संख्याओं के संख्यात्मक गुणों को शामिल करना चाहता हूं (जैसे कि डबल नकारात्मक पहचान पहचान है)। हालांकि, आदिम अंकगणितीय परिचालन के व्यवहार के बारे में कुछ कहना संभव नहीं है। believe_me या अन्य हैंडविंग (कम से कम सबसे बुनियादी गुणों के लिए) का उपयोग करने के लिए, या Nat, Fin और अन्य "उच्च-स्तरीय" संख्यात्मक प्रकारों का उपयोग करके मेरे कोड को फिर से लिखने के लिए बेहतर होगा?

Answer 1

मैं आपको आवश्यक प्राइमेटिव गुणों के लिए postulate का उपयोग करने का सुझाव देना चाहता हूं, केवल उन चीजों का उपयोग करने के लिए सावधान रहना जो वास्तव में संख्यात्मक प्रकार के प्रश्नों के लिए सच हैं, जो मूल रूप से केवल अतिप्रवाह के बारे में सावधान रहना है)।

postulate add_commutes : (x, y : Int) -> x + y = y + x 

believe_me सबसे अच्छा है जब तक आप सबूत के कुछ गणना व्यवहार जरूरत से बचा जाता है: तो आप जैसी चीजों कह सकते हैं। लेकिन, ईमानदार होने के लिए, हम अभी भी primitives के बारे में तर्क करते समय इस सामान को काम करने की कोशिश कर रहे हैं ...

Answer 2

मुझे विश्वास है कि इस समय के लिए Nat का उपयोग करना आम तौर पर बेहतर होता है। इडिस देव, संकलन में तेजी से आदिम लोगों के साथ सबूत-अनुकूल प्रकारों को बदलने के लिए एक सामान्य तंत्र को कार्यान्वित करने की योजना बना रहे हैं, लेकिन अभी के लिए केवल Nat के लिए होता है। यदि आप वास्तव में चाहते थे तो आप believe_me कर सकते हैं, लेकिन आप उन कार्यों के साथ समाप्त हो जाएंगे जो सबूत में काम करना इतना आसान नहीं हैं। ध्यान दें कि यदि आप believe_me के साथ खेलने का निर्णय लेते हैं, तो आपको really_believe_me पर भी विचार करना चाहिए, जो स्पष्ट रूप से इसे प्रकार चेकर के लिए अधिक विश्वसनीय बनाता है।