## Profile

Daniel Peebles
Lives in Norwalk, CT
875 have him in circles

## Stream

### Daniel Peebles

Shared publicly  -

At #ICFP !﻿
6

### Daniel Peebles

Shared publicly  -

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."﻿
6
1

How does one write something like this? I feel that it is simpler to try and have a systematic approach of applying the Kleene Recursion Theorem

http://en.wikipedia.org/wiki/Kleene%27s_recursion_theorem#Application_to_quines

Than to try and fiddle it out by hand.﻿

### Daniel Peebles

Shared publicly  -

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.﻿
4

great! I was thinking of expanding to try to make a universe of searchable types, but it's remarkably hard to get even basic proofs done with coinduction of this sort. Eventually I'd like to come up with an Agda library that approaches the functionality yours has! If only time were more abundant :(﻿

### Daniel Peebles

Shared publicly  -

So much fun to see people making music﻿
1

Such a strange character. Seems to embody a certain stereotype of the piano teacher.﻿

### Daniel Peebles

Shared publicly  -

What would Labour Day be without some Agda﻿
3
1

"What would Labour Day be without some Agda"
...not Hard Labor Day? ;þ﻿
In his circles
334 people
Have him in circles
875 people

### Daniel Peebles

Shared publicly  -
4

I hear it's going back down next year :(﻿

### Daniel Peebles

Shared publicly  -

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?﻿
1

### Daniel Peebles

Shared publicly  -

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.﻿
10

### Daniel Peebles

Shared publicly  -

I sometimes feel like I should troll philosophy journals.﻿
1

I think you'd find philosophers to a fine enough job of that themselves :)﻿

### Daniel Peebles

Shared publicly  -

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.﻿
9
2

Noob, just use WinRAR. Duh.﻿
People
In his circles
334 people
Have him in circles
875 people
Work
Occupation
Sponge
Basic Information
Gender
Male
Story
Tagline
Nerd
Bragging rights
Survived high school
Places
Currently
Norwalk, CT
Previously
Boston, MA - Chiba, Japan - Hanover, NH - Rome, Italy - Monaco