BlogFace.org

Also on the topic of sandwiches:

"Elephant and Castle" on 18th just a bit south of Market offers a reasonably good version of the Canonical Pub Burger Experience closer to my home rather than campus. Burger was low-intensity in flavor, but I think that's okay. I'm beginning to feel that Mikey's is actually a bit over-salty at times. Fries very huge and potatoey. Ambience was Union-Grill-like, but a larger establishment, and they had some English Schtick going on what with calling their fries "chips" on the menu and having bangers'n'mash and stuff. (8/10)

Gave "Lee's Hoagie House" a second shot. Had a cheesesteak this time. Damn if it wasn't just sort of delicious. I notice there is a continuum from more greasy homogenized beef mush to a drier, chewier "I sure am eating pieces of steak" steak. Lee's is at the latter end, which I want instinctually to disprefer, but unlike Steak Queen and that pizza place on Spruce, it still comes out good. Mildly expensive, though. >$8 for sandwich and a drink, whereas Frita's (sadly not to be found today) is like $5, and I think their steak is bigger. (7/10)

You know, I do like obsessively keeping old work of mine, even if I am terrible at organizing it, because I think between 2006ish and nowish I got somewhat better at Illustrator and Photoshop and stuff. (The latter link is a work-in-progress teaser for a print project for Spoons'n'Copic's living room that I am having lots of weekend fun with)

It helps I guess also that I used proper fractal-random-displacement nonsense that I learned in like 1994 (implemented by having sml output svg, of course) to generate the outlines rather than trying to draw them by hand.

Some papers I read today.

"Resource usage analysis", Igarishi and Kobayashi, from POPL'02. This was the PLClub paper of the week. I didn't care for it much at all. There's some idea in there that seems really cool as a generalization of linear uses, but I struggled in vain to really grasp it. There are too many formal concepts not really nailed down enough for me to understand what they're doing. There's not really a strong distinction between things that are definitely propositions and things that are merely functions-on-propositions that feels incredibly alarming to me aesthetically. I'm told these are the dudes who went on to do session types --- can't say I ever totally understood them, either.

"Simplicial Databases", David Spivak. Got this from a CMU talk announcement that Steve Awodey sent out. I am such a sucker for aiming big, big categorical guns at problems like these. I kind of lost track of what was going on halfway through, but it was fun going up to that point, pullbacks and slice categories and labelled simplicial categories and whatnot, all in the name of making mathematical sense out of how databases are actually done out in the real world, especially when that diverges from the nice but too-simplistic classical theory of relational algebra.

"F-ing modules", Andreas Rossberg, Claudio Russo, and Derek Dreyer. This paper is an utter breath of fresh air. I like it so much I find myself constantly worrying that I am missing some flaw in it only because of my nonexpertise in module systems research. Anyhow I find it a rarity that I am able to write a research paper in such a pleasantly direct style. It's just, I don't know, here is what we are going to do, here is why we want to do it, here is how it works, step one, two, three, there --- we're done, isn't it fucking beautiful? Maybe it is a matter of choosing your content carefully to be in reasonably-sized pieces or something, but even before finishing digesting all the middle bits, I can already say that I find it a pleasure to read, and a very nice result to boot, to wit, directly translating a generalization of the ML module system into System F_ω. I mean, if there are not the aforementioned flaws that I am too dumb to notice, it definitely has the feeling of "gosh why wasn't the ML module system explained this way all along" to it. You just kind of pop out abstract types into "monadically" managed prefixes of System F_ω existential quantifiers and dodge a ton of bullshit with selfification and the avoidance problem and stuff.

Plus, you can't beat the cute title.

That ATS post was really gumming up the LJ works. LoWri #3 is a PDF miniposter I hacked together with Dan after reading Types, Abstraction and Parametric Polymorphism in Karl's class and deciding to implement the first little bit in Agda. What we discovered is "interpreting an expression into set theory" and "proving the abstraction/parametricity theorem - that the expression is logically related to itself" are two things with precisely the same computational content. As we suspected, as Bob confirmed, and as these guys probably describe in detail but I haven't read it this means that basically it's the same thing happening in two different categories. Nifty.

So, if you're inclined, here's a PDF with pretty Agda code laid out perfectly in two parallel columns.

A while back I talked about blood donation - I'm scheduled to give blood around 1:30pm on December 10 at the cushy nice permanent blood donation place downtown. Anybody interested in joining me for the bus ride down and a good ol' fashioned blood donation? Feel free to respond off-comments.

So, because ATS is the name of any number of Hogwei Xi's typed languages, the current incarnation is called Anairiats. Simple stuff today; I'm quite a few days behind on my NaLoWriMo.( LoWri #2 - Hello Anairiats )

In conclusion I achieved nothing so far but it wasn't too hard to get the darn thing running, and I'll stop here because I wrote this like four days ago and never finished. More Anairiats games later.

http://radar.spacebar.org/f/a/weblog/comment/1/1033

It was a special shame/privilege (tried to come up with a good sounding portmanteau expressing this sentiment; failed; any luck?) to find myself looking at cplusplus.com and to see an animated Microsoft Windows VII advertisement that uses my 13 year-old font Action Jackson:



It is truly my most popular child. I looked around: It turns out that the font is actually part of Microsoft's current enterprise software branding campaign "the NEW efficiency". You'll see it in whenever they try to sell their expensive stuff by the hundreds to CTOs; e.g.



I like to imagine some guys in suits trading whitepapers. The most surreal is their launch event hooha which has extremely boring videos of señor people giving powerpoint presentations which include this branding. For example, join them for the launch event (warning, you need Silverlight and then you gotta wait to download a LOT of this animated lady that's going to be your personal liaison).

(In old, non-ironic sightings news, Tadbot spotted One Constant used on the Scribblenauts site, which game looks awesome.)

Decided to try something different from Frita's this morning; had a chicken gyro. Not bad! I am not sure if the sauce is sour cream or yogurt-based (I think it is sour cream?) but it is pretty tasty.

(class tonight is)

A UNIT ON THE CIRCULATORY SYSTEM

WHEN YOU HAVE BLOOD-NEEDLE-VEIN-not-phobia-but-very-strong-revulsion-and-dislike

(which I do)

!! ??

AAAHHHH

Another CMU-ism that I am slightly sad to be without: everyone having a UPS in their office. Some dudes fiddling around with electrical stuff here in the basement caused a brief power blip.

When my computer came back on, I had no network. Not that the internet infrastructure in the building was down, because my laptop still worked, but I had no /dev/eth0 device at all! I tried rmmodding and modprobing my network driver, e1000e, but no dice. I did two finds and a diff to determine that there was no change to all of /dev between the module being there and not. /var/log/messages revealed the module not complaining about any errors, though. In an act of desparation, I got the kernel module sources off the thumb drive I had originally installed them from, recompiled, and reinstalled. And it worked! I have no idea why. Even more mysteriously, /dev/eth0 still doesn't exist. Indeed, the module's installation or removal again causes no changes to the entire /dev tree. But eth0 does exist according to ipconfig. Is this some new fancy modern linux virtual device notion? Nobody told me about it. Grumble grumble off my lawn.

No, apparently I am just having bizarre, reality-independent notions about network devices living in /dev.

Amusing log message coming out of a Haskell compilation: (attempting to play with grapefruit)
Generating and compiling a zillion numerical type aliases, this might take a while

Yesterday food adventures:

"Steak Queen" food truck. Boasts "bests steaks on campus". Had a cheesesteak, was not impressed. Steak was sort of gristly and tasted not entirely pleasantly like stir-fry. At least it wasn't liquid-greasy. More expensive than Frita's, farther away from my office, and less tasty. (5/10)

"Gusto", ever so slightly upscale neighborhood pizza place on 22nd between Spruce and Locust. Had an italian sausage calzone, very very tasty. Only problem was that it was two people's worth of food. The onions in it were sort of meh, and achieved that floppy cooked-(but not fried-)onion texture that no right-thinking person enjoys, but the red peppers were really good, the other filling ingredients quite tasty, and the dough was just perfect. The problem with a lot of calzones I have is that the two foldy-end bits get nice and crispy and the center is mooshy and doesn't have enough bread. This fellow was rectangular and somewhat thin, so basically the crust was perfect everywhere. Also: either there was only mozzarella and no ricotta, or else very little ricotta such that I could not even tell it was there. This is exactly as it should be. (8/10)

1. Something they have lots of, behind the Green Glass Door: committees.

2. Today I had an instance of Lucky Procrastinating... a thing on my list that was just sitting there all week, passively generating worry, turned out to be a thing that the process had been entirely changed on right after I talked to the person, so good thing I didn't do anything with it, because I would have had to start over anyway. This type of thing happens a lot. I seem to have a gift for knowing what not to do.

3. Things never feel like Real Life to me. I really want them to, but they never do.

I was skimming this paper and at the top of page 3 misread

the task of the mathematician is to seek a deductive pathway from the
axioms to the propositions or to their denials.

as

the task of the mathematician is to seek a seductive pathway from the
axioms to the propositions or to their denials.

I like my version better.

Two months at this postdoc today. Woo?

Just got an email from Vivek Nigam, who is newly arrived over at the math department. He had a paper with Dale that I wanted to bug him about, so this is very welcome news.