Profile

Cover photo
Daniel Peebles
Lives in Norwalk, CT
927 followers|63,373 views
AboutPostsPhotosVideos

Stream

Daniel Peebles

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

Daniel Peebles

Shared publicly  - 
4
Jens Petersen's profile photoDaniel Peebles's profile photo
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
Ashley Yakeley's profile photoDaniel Peebles'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  - 
 
 
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...
1 comment on original post
3
1
Black Mephistopheles's profile photomukesh tiwari's profile photo
 
+Daniel Peebles
  "What would Labour Day be without some Agda"
...not Hard Labor Day? ;þ
Add a comment...

Daniel Peebles

Shared publicly  - 
1
2
Jason Knight's profile photoDavid Virebayre's profile photo
Add a comment...
Have him in circles
927 people
James Cuff's profile photo
Lally Singh's profile photo
tyler dignan's profile photo
Matloub Husayn-Ali-Khan's profile photo
Joel Torres's profile photo
Maria Khan's profile photo
Amphi art Turkey's profile photo
best best's profile photo
Sergey Kucherenko's profile photo

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."
1 comment on original post
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  - 
 
 
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?
View original post
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.
View original post
8
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, ...
7 comments on original post
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.
8
2
Art Taylor's profile photoStephen Eisenhauer's profile photoJason Knight's profile photoMatúš Tejiščák'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.
1 comment on original post
2
Add a comment...
People
Have him in circles
927 people
James Cuff's profile photo
Lally Singh's profile photo
tyler dignan's profile photo
Matloub Husayn-Ali-Khan's profile photo
Joel Torres's profile photo
Maria Khan's profile photo
Amphi art Turkey's profile photo
best best's profile photo
Sergey Kucherenko'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