Start a hangout

## Profile

Daniel Peebles

Lives in Richmond, VA

968 followers|64,059 views

AboutPostsPhotosVideos

## Stream

### Daniel Peebles

Shared publicly -4

2 comments

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

Add a comment...

### 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

2 comments

+Ashley Yakeley 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 :(

Add a comment...

### Daniel Peebles

Shared publicly -So much fun to see people making music

1

2 comments

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

Add a comment...

### Daniel Peebles

Shared publicly -What would Labour Day be without some Agda

Aaand we're done. But I think this is cheating, since we're heavily exploiting the fact that the type system and the scoping rules of the language we're implementing readily fits into the host type sy...

3

1

Add a comment...

### Daniel Peebles

Shared publicly -A short, potent, emotionally wrenching zombie movie. Utterly worth the 7 minutes.

CARGO - Tropfest Australia 2013 Finalist (TSI "Balloon")

CARGO - Tropfest Australia 2013 Finalist (TSI "Balloon")

1

2

Add a comment...

In his circles

335 people

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

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

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

Than to try and fiddle it out by hand.

Add a comment...

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

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

Add a comment...

### 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

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.

9

Add a comment...

### Daniel Peebles

Shared publicly -I sometimes feel like I should troll philosophy journals.

"No". That was my answer till this afternoon! "Mathematics without proofs isn't really mathematics at all" probably was my longer answer. Yet, I am a mathematics educator who was one of the panelists of a discussion on "proof" this afternoon, alongside two of my mathematician colleagues, ...

1

roux cody

+

1

2

1

2

1

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

Add a comment...

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

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.

8

2

4 comments

Noob, just use WinRAR. Duh.

Add a comment...

### Daniel Peebles

Shared publicly -Time for some Scala fun.

Amongst Haskell folk, it's well known that certain operations on free monads (as implemented by ADTs) are inefficient. One good example is left-nested binds:

(m >>= f) >>= g

This traverses to the leaves of m, applies f, then re-traverses to the leaves of the result to apply g. But, it's merely inefficient, typically.

In Scala, the same case is actually worse, because it eats stack very quickly, and running out of that will just kill your program, rather than it being slow.

However, there are a lot of situations where you don't really care about this. For instance, do-notation naturally generates right-nested binds, as long as you write in a style that looks tail recursive. And when your data types are sufficiently 'lazy', this works out well. Even in Scala.

But, there's a mistake that's easy to miss. In Haskell, you write your pseudo tail-recursive code like:

go x = do y <- some ; stuff ; go (f x y)

Now if you translate to Scala, you write:

go(x : T) = for { y <- some ; _ <- stuff ; r <- go(f(x, y)) } yield r

But this does not generate the right code, it generates something like:

go(x : T) = some.flatMap(y => stuff.flatMap(_ => go(f(x,y)).map(r => r)))

Which is exactly the kind of bad recursive definition that eats your stack on large examples (maybe map is even defined using flatMap). So it's impossible to write the right code for this case using the comprehension syntax.

Amongst Haskell folk, it's well known that certain operations on free monads (as implemented by ADTs) are inefficient. One good example is left-nested binds:

(m >>= f) >>= g

This traverses to the leaves of m, applies f, then re-traverses to the leaves of the result to apply g. But, it's merely inefficient, typically.

In Scala, the same case is actually worse, because it eats stack very quickly, and running out of that will just kill your program, rather than it being slow.

However, there are a lot of situations where you don't really care about this. For instance, do-notation naturally generates right-nested binds, as long as you write in a style that looks tail recursive. And when your data types are sufficiently 'lazy', this works out well. Even in Scala.

But, there's a mistake that's easy to miss. In Haskell, you write your pseudo tail-recursive code like:

go x = do y <- some ; stuff ; go (f x y)

Now if you translate to Scala, you write:

go(x : T) = for { y <- some ; _ <- stuff ; r <- go(f(x, y)) } yield r

But this does not generate the right code, it generates something like:

go(x : T) = some.flatMap(y => stuff.flatMap(_ => go(f(x,y)).map(r => r)))

Which is exactly the kind of bad recursive definition that eats your stack on large examples (maybe map is even defined using flatMap). So it's impossible to write the right code for this case using the comprehension syntax.

2

Add a comment...

People

In his circles

335 people

Work

Occupation

Sponge

Basic Information

Gender

Male

Story

Tagline

Nerd

Bragging rights

Survived high school

Places

Currently

Richmond, VA

Previously

Norwalk, CT - Boston, MA - Chiba, Japan - Hanover, NH - Rome, Italy - Monaco

Links

YouTube

Other profiles