Daniel Peebles
982 followers -
Nerd
Nerd

982 followers
Daniel's posts
At #ICFP !﻿
Post has shared content
Post has shared content
Absurdly impressive

"This is a Ruby program that generates Scala program that generates Scheme program that generates ...(through 50 languages)... REXX program that generates the original Ruby code again."﻿
Post has shared content
Everyone knows (surely!) the definition of Monad:

record Monad (C : Category) : Set where
field
F : Endofunctor C
η : Id C ⇒ F
μ : F ∘ F ⇒ F

unitˡ : μ ∘ (F ^∘ η) ≡ id
unitʳ : μ ∘ (η ∘^ F) ≡ id
assoc : μ ∘ (μ ∘^ F) ≡ μ ∘ (F ^∘ μ)

It is also known that the types in HoTT are ∞-groupoids, which are obviously categories. The question then is -- what is a monad on a HoTT type?

Taking an ∞-groupoid A instead of C, we note that:
* Morphisms on C are identities between elements of A
* Endofunctors on C are functions (A → A)
* Natural transformations are identities between the functions
* For a natural transformation (n : f ≡ g) and a functor h we have
h ^∘ n : h ∘ f ≡ h ∘ g
h ^∘ n = ap (h ∘) n

n ∘^ h : f ∘ h ≡ g ∘ h
h ∘^ n = ap (∘ h) n

and flipping the order of composition for identities, the Monad definition reduces to:

record Monad (A : Type) : Type where
field
f : A → A
η : id ≡ f
μ : f ∘ f ≡ f

unitˡ : ap (f ∘) η ∘ μ ≡ refl
unitʳ : ap (∘ f) η ∘ μ ≡ refl
assoc : ap (∘ f) μ ∘ μ ≡ ap (f ∘) μ ∘ μ

What does it mean? How is it useful? What is its topological meaning? Are there non-trivial examples of such monads?﻿
Post has attachment
Made some more progress on my seemingly impossible Agda. Still haven't figured out how to do the efficient binary conaturals, but one step at a time. I'm so happy to get a real decision procedure out of it, since I wasn't even sure it was provable in Agda until now.﻿
Post has shared content
How come every article I come across about high PPI displays has comments talking about how there's "no content" for them? Text is the content. You'll find no shortage of programmers using ugly bitmap/ultra hinted fonts for improved contrast and readability. With high PPI, one can have that and fonts that don't look like garbage.

Apparently a lot of people think that playing movies is the primary use of a general purpose computer with a good display, though. Or running games at 1920x1080 because that's what an xbox will run at or something. Luckily, Nethack is fully equipped to take advantage of high DPI devices.﻿
Post has attachment
So much fun to see people making music﻿
Post has shared content
I already posted this on twitter, but what takes two tweets only takes one G+ post, and there's a bit of a different crowd over here that might appreciate it more :)

Basically, it's a horribly inefficient implementation of the Burrows-Wheeler transform with run-length encoding on top of it. A mini super-naive version of some of the basic ideas behind bzip2, minus the Huffman coding and other tricks.﻿
Post has shared content