agda - आगाडा और इडिस के बीच मतभेद




type-theory idris (2)

मैं निर्भर रूप से टाइप किए गए प्रोग्रामिंग में गोता लगाने शुरू कर रहा हूं और पाया है कि आगाडा और इडिस भाषा हास्केल के सबसे नज़दीक हैं, इसलिए मैंने वहां शुरुआत की।

मेरा सवाल है: उनके बीच मुख्य अंतर कौन सा है? क्या टाइप सिस्टम दोनों में समान रूप से विस्तारक हैं? व्यापक तुलनात्मक और लाभों के बारे में चर्चा करना बहुत अच्छा होगा।

मैं कुछ स्पॉट करने में सक्षम हूं:

  • इड्रिस में टाइप क्लास à la Haskell है, जबकि Agda उदाहरण तर्क के साथ चला जाता है
  • इडिस में मोनैडिक और आवेदक नोटेशन शामिल है
  • उनमें से दोनों को कुछ प्रकार का रिबाइंडेबल सिंटैक्स लगता है, हालांकि वास्तव में यह सुनिश्चित नहीं है कि वे वही हैं।

संपादित करें : इस प्रश्न के Reddit पृष्ठ में कुछ और जवाब हैं: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/


इडिस और आगादा के बीच एक और अंतर यह है कि इडिस की प्रस्तावित समानता विषम है, जबकि अगदा एक सजातीय है।

दूसरे शब्दों में, इडिस में समानता की मूलभूत परिभाषा होगी:

data (=) : {a, b : Type} -> a -> b -> Type where
  refl : x = x

जबकि आगादा में, यह है

data _≡_ {l} {A : Set l} (x : A) : A → Set a where
    refl : x ≡ x

एग्डा परिभाषा में एल को अनदेखा किया जा सकता है, क्योंकि इसे ब्रह्मांड बहुरूपता के साथ करना है जिसे एडविन ने अपने जवाब में उल्लेख किया है।

महत्वपूर्ण अंतर यह है कि एग्डा में समानता प्रकार ए के दो तत्वों को तर्क के रूप में लेता है, जबकि इडिस में यह संभावित रूप से विभिन्न प्रकारों के साथ दो मान ले सकता है।

दूसरे शब्दों में, इडिस में कोई दावा कर सकता है कि विभिन्न प्रकार के साथ दो चीजें बराबर होती हैं (भले ही यह एक अप्रत्याशित दावा हो जाती है), जबकि आगादा में, बहुत कथन बकवास है।

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

शायद सबसे आसान उदाहरण वेक्टर concatenation की साझेदारी है। दी गई लंबाई-अनुक्रमित सूचियां जिन्हें वेक्टर कहते हैं, इस प्रकार परिभाषित किया गया है:

data Vect : Nat -> Type -> Type where
  Nil : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a 

और निम्नलिखित प्रकार के साथ concatenation:

(++) : Vect n a -> Vect m a -> Vect (n + m) a

हम यह साबित करना चाहते हैं कि:

concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) ->
              xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

यह कथन समान समानता के तहत बकवास है, क्योंकि समानता के बाईं तरफ Vect (n + (m + o)) a टाइप किया गया Vect (n + (m + o)) a और दायीं ओर टाइप Vect ((n + m) + o) a । यह विषम समानता के साथ एक पूरी तरह से समझदार बयान है।


मैं इसका उत्तर देने के लिए सबसे अच्छा व्यक्ति नहीं हो सकता, क्योंकि इडिस को लागू करने के बाद मैं शायद थोड़ा पक्षपातपूर्ण हूं! एफएक्यू - http://docs.idris-lang.org/en/latest/faq/faq.html - इसमें कुछ कहना है, लेकिन उस पर विस्तार करने के लिए:

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

एक और चीज इडिस का उद्देश्य अच्छी तरह से समर्थन करना है एंबेडेड डीएसएल कार्यान्वयन। हास्केल के साथ आप नोटेशन के साथ एक लंबा रास्ता प्राप्त कर सकते हैं, और आप इडिस के साथ भी कर सकते हैं, लेकिन यदि आपको आवश्यकता हो तो आप अन्य संरचनाओं जैसे अनुप्रयोग और परिवर्तनीय बाध्यकारी को भी पुनर्जीवित कर सकते हैं। आप इस पेपर में ट्यूटोरियल, या पूर्ण विवरण में अधिक जानकारी प्राप्त कर सकते हैं: http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

एक और अंतर संकलन में है। एग्डा मुख्य रूप से हास्केल, इडिस के माध्यम से सी के माध्यम से जाता है। एग्डा के लिए एक प्रयोगात्मक बैक एंड है जो सी के माध्यम से इडिस के समान बैक एंड का उपयोग करता है। मुझे नहीं पता कि यह कितना अच्छी तरह से बनाए रखा गया है। इडिस का एक प्राथमिक लक्ष्य हमेशा कुशल कोड उत्पन्न करना होगा - हम वर्तमान में हमारे मुकाबले काफी बेहतर कर सकते हैं, लेकिन हम इस पर काम कर रहे हैं।

एग्डा और इडिस में टाइप सिस्टम कई महत्वपूर्ण मामलों में काफी समान हैं। मुझे लगता है कि मुख्य अंतर सार्वभौमिकों के संचालन में है। एग्डा में ब्रह्मांड बहुरूपता है, इडिस में संचयीता है (और आप Set : Set कर सकते हैं Set : Set यदि आप इसे बहुत ही सीमित पाते हैं तो दोनों में Set : Set और यह ध्यान न रखें कि आपके सबूत असुरक्षित हो सकते हैं)।