Bằng chứng về luật functor của luồng

Question

Tôi đã viết một nội dung tương tự như Luồng. Tôi có thể chứng minh mỗi luật functor nhưng tôi không thể tìm ra một cách để chứng minh rằng nó là tổng số:

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 

Cung cấp:

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

Có một thủ thuật để chứng minh các định luật functor qua codata mà cũng vượt qua kiểm tra tổng thể?

Answer 1

Tôi đã có thể nhận được một chút trợ giúp về IRC từ Daniel Peebles (copumpkin), người đã giải thích rằng việc có thể sử dụng bình đẳng theo đề xuất trên codata thường không được cho phép. Ông chỉ ra rằng nó có thể xác định một quan hệ tương đương tùy chỉnh, như thế nào Agda xác định những người cho Data.Stream:

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

tôi đã có thể làm một bản dịch thẳng về phía trước của định nghĩa này để Idris:

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 

Và điều này dễ dàng vượt qua kiểm tra tổng thể như chúng tôi bây giờ chỉ làm coinduction đơn giản.

Thực tế này hơi thất vọng vì có vẻ như chúng tôi không thể xác định VerifiedFunctor cho loại luồng của chúng tôi.

Daniel cũng chỉ ra rằng Lý thuyết loại quan sát không cho phép bình đẳng theo đề xuất so với codata, đó là điều cần xem xét.