Created
March 10, 2014 01:53
-
-
Save copumpkin/9458179 to your computer and use it in GitHub Desktop.
What could this strange type be isomorphic to?
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 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
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
andfrom
have the answer...