Proof of stream's functor laws

Question

I've been writing something similar to a Stream. I am able to prove each functor law but I can not figure out a way to prove that it's total:

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

Gives:

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

Is there a trick to proving the functor laws over codata which also passes the totality checker?

Answer 1

I was able to get a little help on IRC from Daniel Peebles (copumpkin) who explained that being able to use propositional equality over codata is just generally not something usually permitted. He pointed out that it's possible to define a custom equivalence relation, like how Agda defines ones for Data.Stream:

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

I was able to do a straight forward translation of this definition to 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

And this easily passed the totality checker as we're now just doing simple coinduction.

This fact is a little disappointing since it seems like it means we can't define a VerifiedFunctor for our stream type.

Daniel also pointed out that Observational Type Theory does allow propositional equality over codata, which is something to look into.