I have to rant about this.
A few weeks ago I got a brand new Acer Aspire 6920. It was way shiny. I installed Ubuntu (my first try with Ubuntu; I was a gentoo guy previously) and Vista and spent two days getting everythng just right. I was especially happy getting XMonad working with GNOME, which took a bit of work.
But two weeks ago the video card (GeForce 9500M, fwiw) in my brand new laptop died. I was doing some incredibly intensive graphical computing involving a text terminal and vim, and click — the screen just goes blank. I blindly type “cd; mplayer music/2007-04-21_06.mp3” and music starts playing. So everything was working, I just couldn’t see.
I sent the computer in to get repaired. It arrived at Acer on Wednesday, they didn’t ship it back to me until Monday (I can’t seem to type Monday anymore; it always comes out Monad), and it arrived on Tuesday. I could have been more impressed by their timeliness. I started the computer to find Windows Vista Home Premium with loads of bloatware start up. Uh… okay, so they take four days to repair the computer, then they wipe the hard drive, nevermind about all my stuff or anything. Fortunately I’m a backupoholic.
It was way shiny. I installed Ubuntu and spent a few hours setting everything up a little bit less just right. It turns out getting XMonad working with GNOME was easier than I made it out to be the first time.
We’re having a jam session tomorrow, so I thought I would install Vista so I could record with Cakewalk. Vista has that nice partition manager so I don’t have to do any incantations like installing Vista first *then* Ubuntu or whatever other bullshit we linux users used to have to go through. I put in the Vista disk, get to the partition manager, click on the unallocated space and click *New*. The shown partition table immediately changes to one big full-drive partition. No, that’s not what I wanted. I push cancel and it brings me back to the welcome screen. Okay, that’s kind of annoying, so I go through the motions again and finally make it back to the partition manager. Imagine my dismay as I see the single full-drive partition table again!
And sure enough, when I reboot, grub cannot find my boot partition anymore so I can’t boot linux.
Okay. Vista, listen carefully: Fuck you. I push *New* and with no confirmation you wipe the MBR?! Isn’t linux the one with a reputation for programs which silently do cataclysmic things? And yet, all the partition managers in linux are very careful that you don’t mess anything up, and the one in windows—the OS with the reputation for far too many annoying confirmation dialogs—takes the same care of your MBR as does a retard with a chainsaw.
Anyway, with the help the Ubuntu live distro, a nice program called TestDisk, and about two hours, I was able to restore the lost table, no progress being made toward the ability to record tomorrow. Maybe I’ll just *gasp* not record. Isn’t that the recipe for a great session anyway?
So, Sir Computer, what do you have in store for me next week?
My brand new Acer laptop’s video card died a few days ago. The computer still worked, I just couldn’t see anything. So, while it’s being fixed, I’m back to using my old piece of junk which refuses AC power while turned on. It has an old battery, so I’m limited to about an hour of usage before it forces me to take a break. Needless to say, this is not enough time to get any significant coding done.
Coq is totally awesome! I proved Rice’s theorem for the SK calculus, which was a bit more satisfying than proving that every natural is either even or odd. My proof is pretty ugly, I can see a lot of ways I could clean it up, but I forgive myself; I’m a noob.
Coq is making me very excited for dependent types. For example, toward the end of the aforementioned proof, I started to define some combinators so I could construct the “impossible program”:
Definition compose := S (K S) K. Lemma compose_really_does : forall f g x, compose f g x = f (g x). (* ... *) Qed.
I can envisage doing this kind of thing all the time in my regular programming practice. Write a little function, then prove that it does what I want it to. I’ve already begun exploring ways to use Coq for my every-day programming tasks, such as clean ways to hook into Haskell libraries with Extraction. Who knows how fruitful this endeavor will end up.
I have been making some interesting findings on the FRP front. Here’s an executive summary of each; I may or may not go into more detail in future posts.
(1) The semantics of behaviors are “functions of time”, but what the hell is time? In the real world, time has more structure than numbers. So I claim that in FRP what we’re actually constructing is causal transformations of time functions. A transformation R is causal if R(f)t = R(ft)t for all f, t, where the t subscript means “restricted to times before t”. As yet this has not led to any new implementation insights.
(2) FRP would be simple, easy to work with, and expressive even without its Event type, if only there were an efficient Monad instance for Behavior. For most of the cases where we would use Event, we substitute Behavior :. Future.
(3) Behavior has an efficient Monad instance, but it is not implementable in Haskell as it stands. It requires some support for linear types. Behavior itself is not linear per se, but each separate lexical instance is always accessed in a monotone pattern. So if multiple references were indicated by the compiler with split :: Behavior a -> (Behavior a, Behavior a), then you could destructively update each reference to the latest time it was accessed and avoid the expensive “fast-forwarding” necessary for the naive Monad instance. There are some other tricks, but that is the main idea.
(4) (What I’m currently exploring) It may be possible to get this efficiency without linear types by embedding the linearity in a monad, getting the “Behavior Monad Monad”. Ironically, the best candidate for doing this so far is the “Behavior :. Behavior Monad” (semantically). Whether or not it ends up working, I don’t think it will be very easy to work with.
I’ve written about an idea for a graphical interface to dependent types before. I just played with Coq a little bit, and it’s really fun. I spend 45 minutes proving that every number can be written as either 2n or 2n+1. A feeling of accomplishment washes over me as I finish proving the most substantial result in mathematics history!
Still, the fun of using this system only makes me want to explore this idea more! I like the presentation in the right panel, but I hate the interaction with it. I have to memorize the syntax for a bunch of tactics, typing sequential commands for something that are essentially non-sequential transformations. It’s hard to go back and forth between programming and proving, it’s hard to divert your attention elsewhere for a while. An interface where I could just right click on a hypothesis and see all the ways I could productively transform it would be great in itself.
Damnit! I want a good flexible gui library! I want reactive to be working!