Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
What could this strange type be isomorphic to?
module WeirdIso where
open import Coinduction
open import Data.Nat
open import Data.Stream
open import Relation.Binary.PropositionalEquality
data Weird : Set where
A : (x : Weird) Weird
B : (x : ∞ Weird) Weird
data _≈W_ : Weird → Weird → Set where
eqA : {x y} (p : x ≈W y) A x ≈W A y
eqB : {x y} (p : ∞ (♭ x ≈W ♭ y)) B x ≈W B y
to : Weird Stream ℕ
to (A x) with to x
to (A x) | y ∷ ys = suc y ∷ ys
to (B x) = zero ∷ ♯ to (♭ x)
from : Stream ℕ Weird
from (zero ∷ xs) = B (♯ from (♭ xs))
from (suc x ∷ xs) = A (from (x ∷ xs))
to∘from≈id : x to (from x) ≈ x
to∘from≈id (zero ∷ xs) = refl ∷ ♯ to∘from≈id (♭ xs)
to∘from≈id (suc x ∷ xs) with to (from (x ∷ xs)) | to∘from≈id (x ∷ xs)
to∘from≈id (suc x ∷ xs) | ._ | p ∷ ps = cong suc p ∷ ps
from∘to≈id : x from (to x) ≈W x
from∘to≈id (A x) with to x | from∘to≈id x
from∘to≈id (A x) | y ∷ ys | q = eqA q
from∘to≈id (B x) = eqB (♯ from∘to≈id (♭ x))
@Blaisorblade

This comment has been minimized.

Copy link

commented Nov 23, 2016

What's the TL;DR. answer to the title question? Weird seems neither data nor codata since it mixes recursion and corecursion...

EDIT: Sorry thinko, the types of to and from have the answer...

@copumpkin

This comment has been minimized.

Copy link
Owner Author

commented May 26, 2017

@Blaisorblade that's right, it's Stream ℕ! There are a lot of fun things one can do with mixed data/codata. See also my gist on infinite prime numbers that uses a fancier type to express that there's an infinite stream of primes with finite non-primes between them.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.