Profile

Cover photo
Daniel Peebles
Lives in Norwalk, CT
897 followers|30,525 views
AboutPostsPhotosVideos

Stream

Daniel Peebles

Shared publicly  - 
 
At #ICFP !
6
Add a comment...

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
roux cody's profile photoFrerich Raabe's profile photo
 
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.
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
Daniel Peebles's profile photoAshley Yakeley's profile photo
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
Daniel Peebles's profile photoroux cody's profile photo
2 comments
 
Such a strange character. Seems to embody a certain stereotype of the piano teacher.
Add a comment...

Daniel Peebles

Shared publicly  - 
3
1
mukesh tiwari's profile photoBlack Mephistopheles's profile photo
 
+Daniel Peebles
  "What would Labour Day be without some Agda"
...not Hard Labor Day? ;þ
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")
1
2
Add a comment...
Have him in circles
897 people
Ben Millwood's profile photo
James Cuff's profile photo

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
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 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
Add a comment...

Daniel Peebles

Shared publicly  - 
1
roux cody's profile photo
 
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.
9
2
Jason Knight's profile photoStephen Eisenhauer's profile photoАрсений Алексеев's profile photoArt Taylor's profile photo
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.
2
Add a comment...
People
Have him in circles
897 people
Ben Millwood's profile photo
James Cuff's profile photo
Work
Occupation
Sponge
Basic Information
Gender
Male
Story
Tagline
Nerd
Bragging rights
Survived high school
Places
Map of the places this user has livedMap of the places this user has livedMap of the places this user has lived
Currently
Norwalk, CT
Previously
Boston, MA - Chiba, Japan - Hanover, NH - Rome, Italy - Monaco
Links