धारा के फंक्टर कानूनों का सबूत

Question

मैं स्ट्रीम के समान कुछ लिख रहा हूं। मैं एक functor कानून साबित करने में सक्षम हूँ, लेकिन मैं साबित होता है कि यह कुल है एक तरह से समझ नहीं कर सकते हैं:

module Stream 

import Classes.Verified 

%default total 

codata MyStream a = MkStream a (MyStream a) 

mapStream : (a -> b) -> MyStream a -> MyStream b 
mapStream f (MkStream a s) = MkStream (f a) (mapStream f s) 

streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (f x)) s = mapStream g (mapStream f s) 
streamFunctorComposition (MkStream x y) f g = 
    let inductiveHypothesis = streamFunctorComposition y f g 
    in ?streamFunctorCompositionStepCase 

---------- Proofs ---------- 
streamFunctorCompositionStepCase = proof 
    intros 
    rewrite inductiveHypothesis 
    trivial 

देता है:

*Stream> :total streamFunctorComposition 
Stream.streamFunctorComposition is possibly not total due to recursive path: 
    Stream.streamFunctorComposition, Stream.streamFunctorComposition 

वहाँ codata से अधिक functor कानूनों साबित करने के लिए एक चाल है जो कुलता परीक्षक भी पास करता है?

Answer 1

मैं Daniel Peebles (copumpkin) से आईआरसी पर थोड़ी सी सहायता प्राप्त करने में सक्षम था, जिसने समझाया कि कोडाटा पर प्रस्तावित समानता का उपयोग करने में सक्षम होने पर आमतौर पर आमतौर पर कुछ अनुमति नहीं दी जाती है। उन्होंने बताया कि यह कैसे AGDA Data.Stream के लिए लोगों को परिभाषित करता है की तरह, एक कस्टम तुल्यता संबंध निर्धारित करना संभव है:

data _≈_ {A} : Stream A → Stream A → Set where 
    _∷_ : ∀ {x y xs ys} 
     (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys 

मैं इदरिस को यह परिभाषा के एक सीधे आगे अनुवाद करने में सक्षम था:

module MyStream 

%default total 

codata MyStream a = MkStream a (MyStream a) 

infixl 9 =#= 

data (=#=) : MyStream a -> MyStream a -> Type where 
    (::) : a = b -> Inf (as =#= bs) -> MkStream a as =#= MkStream b bs 

mapStream : (a -> b) -> MyStream a -> MyStream b 
mapStream f (MkStream a s) = MkStream (f a) (mapStream f s) 

streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (f x)) s =#= mapStream g (mapStream f s) 
streamFunctorComposition (MkStream x y) f g = 
    Refl :: streamFunctorComposition y f g 

और यह आसानी से कुलता परीक्षक को पारित कर दिया क्योंकि हम अभी सरल सरलता कर रहे हैं।

यह तथ्य थोड़ा निराशाजनक है क्योंकि ऐसा लगता है कि हम अपने स्ट्रीम प्रकार के लिए VerifiedFunctor परिभाषित नहीं कर सकते हैं।

डैनियल ने यह भी बताया कि ऑब्जर्वेशनल टाइप थ्योरी कोडाटा पर प्रस्तावित समानता की अनुमति देता है, जो कुछ देखने के लिए है।