Daniel's posts

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

"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?

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

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.

*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 sometimes feel like I should troll philosophy journals.

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.

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

What would Labour Day be without some Agda

Wait while more posts are being loaded