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?

In a sense, it's a bit of an odd thing to ask of codata. Functions that operate on codata are required, by the totality check, to limit their consumption thereof in some fashion. This prevents you from ever being able to actually *compute* the equality witness—it's at the end of a potentially infinite loop. Your equivalence relation neatly sidesteps the problem by decreeing streams equivalent if all their initial segments are equivalent. — dfeuer, May 26 '15 at 22:12

Brian McKenna · Accepted Answer · 2015-08-11T23:35:09.433

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.

The `Verified` classes as they stand are too picky for a *lot* of things. For example, most interesting semigroups (tries, meldable heaps, finger trees, etc.) cannot be made instances of `VerifiedSemigroup`, and the same goes for most interesting `Applicative` and `Monad` instances. It is true that one would expect somewhat better results from `Functor`, but even there, things don't really work out so well because there is no extensional equality. — dfeuer, May 26 '15 at 21:57

Proof of stream's functor laws

1 Answers1