Skip to content

Instantly share code, notes, and snippets.

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

This comment has been minimized.

Copy link

Blaisorblade 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...


This comment has been minimized.

Copy link
Owner Author

copumpkin 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.