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 codata
s 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)
- Example:
You're supposed to implement the following functions:
Even
, which corresponds toOdd
,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)
- Example:
- 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!!!
Similar Kata:
Stats:
Created | Mar 8, 2019 |
Published | Mar 8, 2019 |
Warriors Trained | 132 |
Total Skips | 6 |
Total Code Submissions | 78 |
Total Times Completed | 38 |
Idris Completions | 38 |
Total Stars | 4 |
% of votes with a positive feedback rating | 93% of 14 |
Total "Very Satisfied" Votes | 13 |
Total "Somewhat Satisfied" Votes | 0 |
Total "Not Satisfied" Votes | 1 |
Total Rank Assessments | 4 |
Average Assessed Rank | 3 kyu |
Highest Assessed Rank | 1 kyu |
Lowest Assessed Rank | 4 kyu |