समानता परीक्षण

Question

यह संभव बिना या तो स्पष्ट साबित करते हुए कि, (क्या GHC स्वचालित रूप से एक हास्केल 98 प्रकार के लिए Eq उदाहरण के रूप में प्राप्त कर सकते हैं के समान) समानता का एक सरल वाक्यात्मक धारणा को परिभाषित करने के है प्रत्येक डेटा कन्स्ट्रक्टर इंजेक्शनिव है, या कुछ समान कर रहा है, जैसे कि प्रत्येक कन्स्ट्रक्टर के पीछे हटाना और cong का उपयोग करना?

दूसरे शब्दों में, प्रति रचनाकार एक सहायक कार्य शुरू करने के बजाय डेटा कन्स्ट्रक्टर की इंजेक्शनिटी का अधिक उपयोग करना संभव है?

निम्नलिखित उदाहरण के रूप में प्राकृतिक संख्याओं का उपयोग करता है।

module Eq where 

    open import Function 
    open import Relation.Binary 
    open import Relation.Binary.PropositionalEquality 
    open import Relation.Nullary 

    data ℕ : Set where 
     zero : ℕ 
     suc : ℕ → ℕ 

    -- How to eliminate these injectivity proofs? 
    suc-injective : ∀ {n m} → suc n ≡ suc m → n ≡ m 
    suc-injective refl = refl 

    _≟_ : Decidable {A = ℕ} _≡_ 
    zero ≟ suc _ = no (λ()) 
    suc _ ≟ zero = no (λ()) 
    zero ≟ zero = yes refl 
    suc n ≟ suc m with n ≟ m 
    suc n ≟ suc .n | yes refl = yes refl 
    ... | no n≢m = no (n≢m ∘ suc-injective) 

एक cong (λ { zero → zero ; (suc x) → x }) द्वारा suc-injective, एक समारोह जो suc उलट परिभाषित करने तक यानी की जगह सकता है, लेकिन है कि अभी भी निर्माता प्रति एक सहायक समारोह के बॉयलरप्लेट आवश्यकता है, और इस तरह के कार्यों को कुछ हद तक जरूरत कुल होना करने के लिए की वजह से परिभाषित करने के लिए बदसूरत हैं ।

(सामान्य चेतावनियां कर रहे हैं। लागू स्पष्ट कुछ कमी।)

Answer 1

Ulf Norell के prelude for Agda स्वचालित रूप से किसी दिए गए डेटा-प्रकार के लिए डिसाइडेबल समानता पाने के लिए एक तंत्र होता है। यह कोड एग्डा के प्रतिबिंब तंत्र पर आधारित है और रचनाकारों की इंजेक्शनशीलता साबित करने के लिए स्वचालित रूप से विस्तारित लैम्ब्डा उत्पन्न होता है। मैं कोड को देखने की सलाह देता हूं, भले ही यह हमेशा जितना आसान हो उतना आसान न हो।