हास्केल के तीर-क्लास AGDA में और -> AGDA

Question

में मेरे पास दो निकट से संबंधित प्रश्न:

सबसे पहले, कैसे हास्केल के तीर वर्ग तैयार किया जा सकता/AGDA में प्रतिनिधित्व?

class Arrow a where 
     arr :: (b -> c) -> a b c 
     (>>>) :: a b c -> a c d -> a b d 
     first :: a b c -> a (b,d) (c,d) 
     second :: a b c -> a (d,b) (d,c) 
     (***) :: a b c -> a b' c' -> a (b,b') (c,c') 
     (&&&) :: a b c -> a b c' -> a b (c,c') 

(निम्नलिखित Blog Post कहा गया है कि यह संभव हो जाना चाहिए ...)

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

Answer 1

प्रकार वर्गों आमतौर पर AGDA में रिकॉर्ड के रूप में इनकोड है, तो आप कुछ इस तरह के रूप में Arrow वर्ग सांकेतिक शब्दों में बदलना कर सकते हैं:

open import Data.Product -- for tuples 

record Arrow (A : Set → Set → Set) : Set₁ where 
    field 
    arr : ∀ {B C} → (B → C) → A B C 
    _>>>_ : ∀ {B C D} → A B C → A C D → A B D 
    first : ∀ {B C D} → A B C → A (B × D) (C × D) 
    second : ∀ {B C D} → A B C → A (D × B) (D × C) 
    _***_ : ∀ {B C B' C'} → A B C → A B' C' → A (B × B') (C × C') 
    _&&&_ : ∀ {B C C'} → A B C → A B C' → A B (C × C') 

आप समारोह प्रकार सीधे उल्लेख नहीं जा सकता है (_→_ की तरह कुछ नहीं है मान्य सिंटैक्स), आप इसके लिए अपने खुद के नाम लिख सकते हैं, जिसे फिर आप उपयोग कर सकते हैं जब एक उदाहरण लेखन:

_=>_ : Set → Set → Set 
A => B = A → B 

fnArrow : Arrow _=>_ -- Alternatively: Arrow (λ A B → (A → B)) or even Arrow _ 
fnArrow = record 
    { arr = λ f → f 
    ; _>>>_ = λ g f x → f (g x) 
    ; first = λ { f (x , y) → (f x , y) } 
    ; second = λ { f (x , y) → (x , f y) } 
    ; _***_ = λ { f g (x , y) → (f x , g y) } 
    ; _&&&_ = λ f g x → (f x , g x) 
    } 

Answer 2

जबकि Hammar के जवाब हास्केल कोड का एक सही बंदरगाह है, _=>_ की परिभाषा भी एल है -> की तुलना में नकल किया गया है, क्योंकि यह निर्भर कार्यों का समर्थन नहीं करता है। हास्केल से कोड का अनुकूलन करते समय, यदि आप एग्डा में लिखने वाले कार्यों में अपने अवशेषों को लागू करना चाहते हैं तो यह एक मानक आवश्यक परिवर्तन है।

इसके अलावा, मानक पुस्तकालय के सामान्य सम्मेलन के द्वारा, इस प्रकार के वर्ग को RawArrow कहा जाएगा क्योंकि इसे लागू करने के लिए आपको सबूत प्रदान करने की आवश्यकता नहीं है कि आपका उदाहरण तीर कानूनों को पूरा करता है; अन्य उदाहरणों के लिए RawFunctor और RawMonad देखें (नोट: फंक्शन और मोनाड की परिभाषा मानक पुस्तकालय में कहीं भी नहीं है, संस्करण 0.7 के रूप में)।

यहां एक और शक्तिशाली संस्करण है, जिसे मैंने एग्डा 2.3.2 और 0.7 मानक लाइब्रेरी के साथ लिखा और परीक्षण किया (संस्करण 0.6 पर भी काम करना चाहिए)। ध्यान दें कि मैंने केवल RawArrow के पैरामीटर और _=>_ के प्रकार की घोषणा को बदल दिया है, बाकी अपरिवर्तित है। fnArrow बनाते समय, सभी वैकल्पिक प्रकार की घोषणाएं पहले की तरह काम नहीं करतीं।

चेतावनी: मैंने केवल जांच की है कि कोड टाइपकेक और वह => समझदारी से उपयोग किया जा सकता है, मैंने यह जांच नहीं की कि RawArrow टाइप चेक का उपयोग करने वाले उदाहरण हैं या नहीं।

module RawArrow where 

open import Data.Product --actually needed by RawArrow 
open import Data.Fin  --only for examples 
open import Data.Nat  --ditto 

record RawArrow (A : (S : Set) → (T : {s : S} → Set) → Set) : Set₁ where 
    field 
    arr : ∀ {B C} → (B → C) → A B C 
    _>>>_ : ∀ {B C D} → A B C → A C D → A B D 
    first : ∀ {B C D} → A B C → A (B × D) (C × D) 
    second : ∀ {B C D} → A B C → A (D × B) (D × C) 
    _***_ : ∀ {B C B' C'} → A B C → A B' C' → A (B × B') (C × C') 
    _&&&_ : ∀ {B C C'} → A B C → A B C' → A B (C × C') 

_=>_ : (S : Set) → (T : {s : S} → Set) → Set 
A => B = (a : A) -> B {a} 

test1 : Set 
test1 = ℕ => ℕ 
-- With → we can also write: 
test2 : Set 
test2 = (n : ℕ) → Fin n 
-- But also with =>, though it's more cumbersome: 
test3 : Set 
test3 = ℕ => (λ {n : ℕ} → Fin n) 
--Note that since _=>_ uses Set instead of being level-polymorphic, it's still 
--somewhat limited. But I won't go the full way. 

--fnRawArrow : RawArrow _=>_ 
-- Alternatively: 
fnRawArrow : RawArrow (λ A B → (a : A) → B {a}) 

fnRawArrow = record 
    { arr = λ f → f 
    ; _>>>_ = λ g f x → f (g x) 
    ; first = λ { f (x , y) → (f x , y) } 
    ; second = λ { f (x , y) → (x , f y) } 
    ; _***_ = λ { f g (x , y) → (f x , g y) } 
    ; _&&&_ = λ f g x → (f x , g x) 
    }