3 kyu

Tear me apart and merge the pieces together

Description:

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!!!

Theorem Proving
Lists
Fundamentals

Stats:

CreatedMar 8, 2019
PublishedMar 8, 2019
Warriors Trained132
Total Skips6
Total Code Submissions78
Total Times Completed38
Idris Completions38
Total Stars4
% of votes with a positive feedback rating93% of 14
Total "Very Satisfied" Votes13
Total "Somewhat Satisfied" Votes0
Total "Not Satisfied" Votes1
Total Rank Assessments4
Average Assessed Rank
3 kyu
Highest Assessed Rank
1 kyu
Lowest Assessed Rank
4 kyu
Ad
Contributors
  • ice1000 Avatar
  • lolisa Avatar
Ad