एग्डा

Question

के लिए हास्केल व्युत्पन्न तंत्र मैं सोच रहा हूं कि अगर एग्डा में कुछ भी है जो हैस्केल के deriving Eq खंड जैसा दिखता है --- तो मेरे पास भी एक संबंधित प्रश्न है।

उदाहरण के लिए,,

data Type : Set where 
    Nat : Type 
    Prp : Type 

तब मैं पैटर्न मिलान और C-c C-a द्वारा डिसाइडेबल समानता लागू कर सकते हैं मैं एक खिलौना-भाषा के लिए प्रकार है लगता है,

_≟ₜ_ : Decidable {A = Type} _≡_ 
Nat ≟ₜ Nat = yes refl 
Nat ≟ₜ Prp = no (λ()) 
Prp ≟ₜ Nat = no (λ()) 
Prp ≟ₜ Prp = yes refl 

अगर यह कर सकते हैं मैं उत्सुक हूँ हास्केल में किए गए तरीके से मशीनीकृत या स्वचालित हो जाएं:

data Type = Nat | Prp deriving Eq 

धन्यवाद-आप!

जबकि हम प्रकार के विषय पर हैं, मैं अपने औपचारिक प्रकारों को एग्डा प्रकार के रूप में महसूस करना चाहता हूं: नेट केवल प्राकृतिक संख्या है जबकि पीआरपी छोटे प्रस्ताव हैं।

⟦_⟧Type : Type → Set ? 
⟦ Nat ⟧Type = ℕ 
⟦ Prp ⟧Type = Set 

दुख की बात यह काम नहीं करती है। मैंने उठाने के साथ इसे ठीक करने की कोशिश की लेकिन असफल रहा क्योंकि मुझे स्तर उठाने का उपयोग करने के बारे में कोई जानकारी नहीं है। किसी भी मदद की सराहना की है! मुझे humouring के लिए

ऊपर समारोह का एक उदाहरण उपयोग किया जाएगा,

record InterpretedFunctionSymbol : Set where 
    field 
    arity : ℕ 
    src tgt : Type 
    reify : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type 

धन्यवाद!

Answer 1

A Cosmology of Datatypes के अध्याय "7.3.2। डेटाटाइप पर व्युत्पन्न संचालन" विवरण दिखाते हुए संचालन कैसे प्राप्त करें। हालांकि, व्युत्पन्न वहां कमजोर है।

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

यदि आपके पास बंद ब्रह्मांड है तो आप एक मजबूत Eq प्राप्त कर सकते हैं। वर्णन के समान दृष्टिकोण का उपयोग करना (समान रूप से अभिव्यक्तिपूर्ण होना चाहिए, लेकिन मैंने जांच नहीं की थी) और एक बंद ब्रह्मांड मैंने जेनेरिक showhere परिभाषित किया है, जो उदा। आप कंस्ट्रक्टर्स नाम के बाद tuples का एक वेक्टर मुद्रित करने के लिए:

instance 
    named-vec : {A : Type} -> Named (vec-cs A) 
    named-vec = record { names = "nil" ∷ "cons" ∷ [] } 

test₂ : show (Vec (nat & nat) 3 ∋ (7 , 8) ∷ᵥ (9 , 10) ∷ᵥ (11 , 12) ∷ᵥ []ᵥ) 
     ≡ "(cons 2 (7 , 8) (cons 1 (9 , 10) (cons 0 (11 , 12) nil)))" 
test₂ = prefl 

जहां VecDesc डेटा प्रकार के लिए इसी तरह की एक के रूप में परिभाषित किया गया है। Eq केस समान होना चाहिए, लेकिन अधिक परिष्कृत होना चाहिए।

यहाँ कैसे Lift इस्तेमाल किया जा सकता है:

⟦_⟧Type : Type → Set₁ 
⟦ Nat ⟧Type = Lift ℕ 
⟦ Prp ⟧Type = Set 

ex₁ : ∀ A -> ⟦ A ⟧Type 
ex₁ Nat = lift 0 
ex₁ Prp = ℕ 

ex₂ : ∀ A -> ⟦ A ⟧Type -> Maybe ℕ 
ex₂ Nat n = just (lower n) -- or (ex₂ Nat (lift n) = just n) 
ex₂ Prp t = nothing 

तो A : Set α तो Lift A : Set (α ⊔ ℓ) के लिए किसी भी ℓ। तो जब आपके पास ℕ : Set और Set : Set₁ है, तो आप से Set₁ से पर लेना चाहते हैं, जो साधारण मामलों में आपको ℓ स्पष्ट रूप से प्रदान करने की आवश्यकता नहीं है।

Lift में लिपटे डेटा प्रकार का एक तत्व बनाने के लिए आप lift (जैसे lift 0) का उपयोग करते हैं। और इस तत्व को वापस पाने के लिए आप lower का उपयोग करें, इसलिए lift और lower एक दूसरे के उलटा हैं। ध्यान दें कि lift (lower x)x के समान ब्रह्मांड में जरूरी नहीं है, क्योंकि lift (lower x) "रीफ्रेश" ℓ।

Answer 2

आगाडा में "व्युत्पन्न ईक" के व्यावहारिक कार्यान्वयन के लिए, आप https://github.com/UlfNorell/agda-prelude पर Ulf के agda-prelude पर एक नज़र डाल सकते हैं। विशेष रूप से, मॉड्यूल Tactic.Deriving.Eq में (सामान्य और अनुक्रमित) डेटा प्रकारों की एक सामान्य श्रेणी के लिए स्वचालित रूप से निर्णायक समानता उत्पन्न करने के लिए कोड होता है।