Kata

In this Kata you'll learn Bisimulation.

First you need to know what is coinduction, which is dual to induction. While we enjoy equivalence on induction (the equality type is inductive) on the primal, we can have bisimulation on coinduction on the dual. This is because the inductive equality type, = in Idris, is not lazied. For lazily evaluated codatas we can't use our warm fuzzy equality type on it (which means we need another solution for equality on coinductive types, which is bisimulation).

It's a pity that Idris still don't have copatterns till now (maybe Blodwen can have it?).

You get it right? You didn't get confused right? This Kata picks Idris' built-in Stream type as the protagonist, and preloaded this code:

module Bisimulation

%default total
%access export

infixr 10 :=:
public export
codata Bisimulation : (x : Stream a) -> (y : Stream a) -> Type where
  (:=:) : {x : Stream a} -> {y : Stream a} ->
          (head x = head y) ->
          (Bisimulation (tail x) (tail y)) ->
          (Bisimulation x y)

You're given the examples of:

• How to construct a stream, and its bisimulation
• An Odd function, which takes the odd-indexed elements of a stream
  • Example: Odd [1, 2, 3, 4] gives you [2, 4] (but here the stream is infinite, this example is just for showing the idea)

You're supposed to implement the following functions:

• Even, which corresponds to Odd, Even [1,2,3,4] returns [1, 3]
• Merge, which merges two streams one by one
  • Example: Merge [1, 1] [2, 2] gives [1, 2, 1, 2] (but actual input is infinite)
• A proof that \x -> Merge (Even x) (Odd x) is equivalent to identity
  • Here we can see something similar to function extensionality :)

Checkout the successor of this Kata after you've finished!

Follow me: Merge -- Odd -- Even -- MOE!!!