Agda

Question

पर पैरामैट्रिज्ड इंडेक्टिव प्रकार मैं केवल Dependent Types at Work पढ़ रहा हूं। परिचय प्रकार parametrised करने के लिए, लेखक का उल्लेख है कि इस घोषणा

data List (A : Set) : Set where 
    [] : List A 
    _::_ : A → List A → List A 

में List के प्रकार Set → Set है और वह A दोनों निर्माताओं, यानी करने के लिए अंतर्निहित तर्क हो जाता है।

[] : {A : Set} → List A 
_::_ : {A : Set} → A → List A → List A 

ठीक है, मैं यह थोड़ा अलग

data List : Set → Set where 
    [] : {A : Set} → List A 
    _::_ : {A : Set} → A → List A → List A 

जो दुर्भाग्य से काम नहीं करता है (मैं दो दिन या तो के लिए AGDA जानने की कोशिश कर रही है, लेकिन मैं क्या इकट्ठा यह है से फिर से लिखने की कोशिश की क्योंकि रचनाकारों को Set₀ पर पैरामीराइज्ड किया गया है और इसलिए List ASet₁ में होना चाहिए)।

दरअसल, निम्नलिखित

data List : Set₀ → Set₁ where 
    [] : {A : Set₀} → List A 
    _::_ : {A : Set₀} → A → List A → List A 

स्वीकार किया जाता है फिर भी, मैं अब {A : Set} → ... → List (List A) उपयोग करने में सक्षम हूँ (जो पूरी तरह से समझा जा सकता है)।

तो मेरा प्रश्न: List (A : Set) : Set और List : Set → Set के बीच वास्तविक अंतर क्या है?

आपके समय के लिए धन्यवाद!

Answer 1

मैं डेटा प्रकारों का नाम बदलने की स्वतंत्रता लेता हूं।

data ListI : Set → Set₁ where 
    [] : {A : Set} → ListI A 
    _∷_ : {A : Set} → A → ListI A → ListI A 

data ListP (A : Set) : Set where 
    [] : ListP A 
    _∷_ : A → ListP A → ListP A 

डेटा प्रकार में मानकों पेट से पहले जाना है, और कोलन के बाद तर्क कहा जाता है: पहला, जो Set पर सूचीबद्ध है ListI बुलाया जाएगा, और दूसरा ListP, Set एक पैरामीटर के रूप है indicies।

nilI : {A : Set} → ListI A 
nilI {A} = [] {A} 

nilP : {A : Set} → ListP A 
nilP {A} = [] {A} 

वहाँ अंतर आता है जब पैटर्न मिलान: कंस्ट्रक्टर्स ही तरह से इस्तेमाल किया जा सकता है, तो आप अंतर्निहित सेट लागू कर सकते हैं। अनुक्रमित संस्करण के लिए हमने:

null : {A : Set} → ListI A → Bool 
null ([] {A})  = true 
null (_∷_ {A} _ _) = false 

यह ListP के लिए नहीं किया जा सकता:

-- does not work 
null′ : {A : Set} → ListP A → Bool 
null′ ([] {A})  = true 
null′ (_∷_ {A} _ _) = false 

त्रुटि संदेश है

The constructor [] expects 0 arguments, but has been given 1 
when checking that the pattern [] {A} has type ListP A 

ListP भी एक डमी मॉड्यूल के साथ परिभाषित किया जा सकता है, के रूप ListD:

module Dummy (A : Set) where 
    data ListD : Set where 
    [] : ListD 
    _∷_ : A → ListD → ListD 

open Dummy public 

शायद थोड़ा आश्चर्यजनक, ListDListP के बराबर है।

-- does not work 
null″ : {A : Set} → ListD A → Bool 
null″ ([] {A})  = true 
null″ (_∷_ {A} _ _) = false 

यह ListP के लिए के रूप में ही त्रुटि संदेश देता है: हम पैटर्न नहीं तर्क पर मैच Dummy कर सकते हैं।

ListP एक parameterised डेटा प्रकार है, जो सरल से ListI है, जो एक आगमनात्मक परिवार है का एक उदाहरण है: यह indicies पर "निर्भर करता है", हालांकि एक तुच्छ रास्ते में इस उदाहरण में।

parameterised डेटा प्रकार the wiki, और here पर परिभाषित कर रहे हैं एक छोटे से परिचय है।

प्रेरक परिवारों वास्तव में परिभाषित नहीं कर रहे हैं, लेकिन वह आगमनात्मक परिवारों की जरूरत है लगता है कुछ के विहित उदाहरण के साथ the wiki में पर सविस्तार:

data Term (Γ : Ctx) : Type → Set where 
    var : Var Γ τ → Term Γ τ 
    app : Term Γ (σ → τ) → Term Γ σ → Term Γ τ 
    lam : Term (Γ , σ) τ → Term Γ (σ → τ) 

प्रकार सूचकांक की अनदेखी, इस का एक सरलीकृत संस्करण नहीं कर सका Dummy में lam कन्स्ट्रक्टर के कारण मॉड्यूल तरीके से लिखा गया हो।

एक और अच्छा संदर्भ 1997

मुबारक AGDA कोडिंग से Inductive Families पीटर Dybjer से है!