Profile

Cover photo
Daniel Peebles
Lives in Norwalk, CT
917 followers|62,936 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  - 
 
 
Just a little something from a hacking spree done mostly on Friday.

I'm not too happy about having to include the number of rigid type variables in the type of the overall type judgement; in fact, maybe I should try to enforce it to be 0 in ⊢_∷_ (so that every toplevel expression has a type without rigid/free type variables).
hindleymilner-agda - Hindley Milner type system modeled in Agda
3 comments on original post
1
Add a comment...
Have him in circles
917 people
Aleh Veraskouski's profile photo
Dag Odenhall's profile photo
Joshua Hill's profile photo
Stephen Diehl's profile photo
Tyler Casson's profile photo
Thomas Fop's profile photo
Robert Wills's profile photo
Steven De Franco's profile photo
Debra Weaver'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
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, ...
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.
9
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  - 
1
2
Jason Knight's profile photoDavid Virebayre's profile photo
Add a comment...
People
Have him in circles
917 people
Aleh Veraskouski's profile photo
Dag Odenhall's profile photo
Joshua Hill's profile photo
Stephen Diehl's profile photo
Tyler Casson's profile photo
Thomas Fop's profile photo
Robert Wills's profile photo
Steven De Franco's profile photo
Debra Weaver'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