Доказательство законов функторов потока

Question

Я писал что-то похожее на поток. Я могу доказать каждый закон функтора, но не могу найти способ доказать, что он тотальный:

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

Есть ли хитрость в доказательстве законов функторов над кодой, которые также проходят проверку целостности?

Answer 1

Я смог получить небольшую помощь по IRC от 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 для нашего типа потока.

Даниэль также отметил, что теория типов наблюдений допускает пропозициональное равенство по кодатам, что является чем-то, на что стоит обратить внимание.