Investigate laws about delegate

[Toxaris]

(for discussion)

@b-studios figured out that delegate is similar to comonadic duplicate (the dual of monadic join). @Blaisorblade asked whether our delegate satisfies the applicable comonad laws. I tried to prove delegate . delegate == fmap delegate . delegate, but I'm stuck with an occurrence of the law itself inside consume. Is there a proof technique which can help me here?

random ideas: coinduction? bisimulation? observational equivalence for all finite token streams?

[b-studios]

I have the same problem with the Scala implementation and the monad laws. You are right, what we need is is bisimilarity / reasoning by coinduction. I would phrase the prove per observation / transition, as in:

We want to show that

  delegate (delegate p) ~ fmap delegate (delegate p)

definitions:
  results (delegate p)   = pure p
  consume (delegate p) t = delegate (consume p t)

  results (fmap f p)     = fmap f (results p)
  consume (fmap f p) t   = fmap f (consume p t)

results (delegate (delegate p))
  = pure (delegate p)                       (1.1)
  = fmap delegate (pure p)                  (1.2)
  = fmap delegate (results (delegate p))    (1.3)
  = results (fmap delegate (delegate p))    (1.4)

∀t
consume (delegate (delegate p)) t
  = consume (delegate (delegate p)) t       (2.1)
  = delegate (consume (delegate p) t)       (2.2)
  = delegate (delegate (consume p t))       (2.3)
  ~ fmap delegate (delegate (consume p t))  (2.4)
  ~ fmap delegate (consume (delegate p) t)  (2.5)
  ~ consume (fmap delegate (delegate p)) t  (2.6)

Notice the switch to bisimilarity (using the coinductive hypothesis). Following Practical Coinduction p. 11, since the parser is a terminal coalgebra we can not only conclude that

delegate (delegate p) ~ fmap delegate (delegate p)

but also

delegate (delegate p) = fmap delegate (delegate p)

I am most unsure about the part with ∀t, though.

Edit: (1.2) is adopted from your proof. Why is this the case?

[Toxaris]

Step 1.2 uses the lemma that fmap f (pure x) == pure (f x) which is proven by the remark on "the Functor instance for f" in the documentation of Applicative followed by the homomorphism law, ibid.

[Toxaris]

the use of coinduction in the correctness proofs might validity the name "coalgebraic-parsing" :)

[b-studios]

Yes, at least parsers in our framework are terminal coalgebras over the functor p s = f a × t -> s. Of course we could also call them parser-objects or something similar :)

[Blaisorblade]

That all sounds cool. I've verified most steps in the proof and they're fine. I'm just confused about coinduction, but for a change I'll assume my basic doubts on it aren't insightful enough to share.

[Toxaris]

@b-studios convinced me that this coinductive proof is correct. The key is that we are reducing a property of parser p to a property on consume p t for arbitrary t.