Profile cover photo
Profile photo
Daniel Peebles

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

compress = map(length&&&head).group.(last<$>).sort.init.(zipWith(++)<$>tails<*>inits).(Nothing:).(Just<$>)

decompress = catMaybes.head.foldr((sort.).zipWith(:))(repeat[]).(replicate=<<length).(uncurry replicate=<<)

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
Wait while more posts are being loaded