Profile cover photo
Profile photo
Edward Yang
1,684 followers
1,684 followers
About
Edward's posts

Spent the afternoon porting gnome-settings-daemon 3.6 to Saucy, to get xmonad+fn keys/volume keys working again. I'll post the deb to my PPA once I figure out one last packaging bug.

A Haskell problem I am having some difficulty with: I am trying to generalize 'Mu' (i.e. 'newtype Mu f = In (f (Mu f))') in a way so that I can express mutually recursive data structures with it (e.g. 'data A = A | ToB B' and 'data B = B | ToA A'); that is to say, I want to be able to run the fixpoint in an arbitrary category. Any ideas? (I have a few attempts, which I will try to write up in a coherent way.)

Installation notes for Bitvise SSH Server: the biggest problem with this SSH server is that it's pseudo-tty implementation is on crack. It toggles the background color of text it outputs, often outputs extra spaces which mess up my terminal's copy-paste, has a terminfo database with a grand total of 14 entries in it, many of which are wrong. In particular, my life got a lot better when I replaced their 'screen' terminfo file with a copy from my local (modern) Ubuntu install (actually, I stuffed screen-256color although that's technically "wrong", because msys doesn't understand how to derive TERM properly and just sets it to cygwin).

Was reading "Writing Solid Code" and stumbled on this quote:

----

When was the last time you read an advertisement for a leading word processor? If the folks on Madison Avenue wrote it, it probably sounded something like this: "Whether you're writing a note to Johnny's teacher or working on the next Great American Novel, WordSmasher can handle it. Effortlessly. And to catch typing mistakes that creep into your masterpiece, there's a mind-boggling 233,000-word spelling dictionary—51,000 more words than in the nearest competitor's. So run down to your dealer and pick up a copy. WordSmasher. The most revolutionary writing tool since the ballpoint pen."

As users, we've been trained by constant marketing propaganda to believe that the bigger the spelling dictionary, the better. But that isn't true. You can find the words em, abel, and si in any paperback dictionary, but do you really want your spelling checker to allow those words when me, able and is are so common? If you see suing in something I write, the odds are astronomical that I meant using. It doesn't matter that suing is a real word; in my writing, it's an error.

Fortunately, high-quality spelling checkers will let you delete troublesome words like em from their dictionaries so that you can flag an otherwise legal word as an error. Good compilers are no different—they will let you flag otherwise legal C idioms as errors because the idioms are so often used in a mistaken way.

For my personal records: if you need to issue a Kerberos keytab that contains your password for password-less auth, the invocations are:

ktutil
add_entry -password -p ezyang@ATHENA.MIT.EDU-k 1 -e aes256-cts-hmac-sha1-96
write_kt new-keytab

If you kinit manually, klist -e will give useful information about many of these parameters.

Here's a small problem. Hughes lists are defined as functions 'f : List a -> List a' such that (fromlist xs) ys = xs ++ ys. Why isn't this type isomorphic to 'List a'? Can you come up with a type which is morally the same, and is isomorphic to 'List a'?

Post has attachment
I recently learned how to do Debian packaging, so I packaged Coq with Mtac for Ubuntu. I also packaged the Homotopy Type Theory variant of Coq: https://launchpad.net/~ezyang/+archive/coq-hott . Or if you're not feeling so adventurous, try the vanilla backport of 8.4pl2 for Raring in my general PPA https://launchpad.net/~ezyang/+archive/ppa

If you install these packages, they will replace your existing Coq installation, so folks with large developments beware! But this should make it easier for causal users to try things out (especially the Mtac PPA).

"To sum up: By now, you've had a little bit of time programming in Agda and programming in Coq. We didn't talk about the contrast between the two (you'll see more when Steve lectures in Coq). But in terms of the contrast, someone has used the line: "Coq is like playing a video game." So the question you should ask, is what kind of video game you are playing. Coq feels to me like Dragon Warrior or Final Fantasy?  Essentially, if you press the A button long enough, you'll get through the proof.  And you can write a tactic to press the A button repeatedly.  On the other hand, Agda feels to me like Tetris.  There are like five pieces, and it's all about how you arrange these pieces. We looked at all this different ways of doing things; the same tools arranged in different ways. There are tradeoffs. Sometimes in Agda, the pieces are stacked up in such an unwieldy way, and it scrolls off the screen, and you lose. But sometimes it stacks up really neatly, and you get a really elegant piece of code. This is what people should strive for when they prove things in dependently typed languages." — Dan Licata, concluding remarks for his Agda lecture series at OPLSS'13

Pro-tip: if Linux complains "VFS: Cannot open root device or unknown-block" and asks you to append the correct "root" option; it could just be missing an appropriate initrd for the kernel you booted. (This means no file system drivers, which means even though Linux can find your file system, it can't read it. Hooray for decipherable error messages.)

Post has attachment
How CAF update works in GHC.
Photo
Wait while more posts are being loaded