?

Log in

No account? Create an account
Notes from a Medium-Sized Island [entries|archive|friends|userinfo]
Jason

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Sep. 7th, 2006|11:59 pm]
Jason
[Tags|, , , ]

Today I had went to class, had a decent advisor meeting, and then I saw Karl talk about twelf encodings of the metatheory of singleton kinds (or, equally well, singleton types). I was struck by

  • how beautiful the underlying theory of singletons is
  • again how powerful a tool hereditary canonicalization is
  • how much I prefer spine form (i.e. focusing) presentations of LF to the apparently popular approach of considering non-fully-applied atomic terms
  • how gross and write-only twelf concrete syntax tends to be. I think the only reason I can read my own code is that it is my own code, and I know it backwards and forwards already. Karl's stuff seems pretty well written as twelf code goes, but it's still a lot harder to slog through it in a talk than, like, pseudocode of an ordinary program in an ordinary programming language. Not really a fair comparison, but still.


Later read some more of Bloom, still wading through the Whitman chapter. Even though sometimes it feels like Bloom's opinion of you is 90% determined by whether you are a fan of (or in fact are one of) the select club of writers he deifies, and only like 10% by the quality of your work, he is quite a decent writer himself. I've enjoyed reading many paragraphs I violently disagree with by content, because they are so nicely written. I could listen to him mumble all day about his Anxiety of Influence, his "the American Religion", his Creative Misprision.

In the evening I was torn between going to D's and hanging out at martinivixen'n'mistergone's where they were watching the steelers season opener. Decided for the latter, mostly because I didn't feel in a noisy-bar mood. I think I kinda understood most of the football game, but the main lesson of the evening is that sk4p and mistergone are pee-your-pants funny when they get going.
LinkReply

Comments:
From: mmia
2006-09-08 02:08 pm (UTC)
Oh is that what you're reading-- The Anxiety of Influence. That was a textbook and a recommendation from a critical theory professor of mine a couple years ago.
(Reply) (Thread)
[User Picture]From: jcreed
2006-09-08 02:16 pm (UTC)
No, I'm reading "The Western Canon", but the concept of anxiety of influence is one Bloom loves to bring up over and over in his work.
(Reply) (Parent) (Thread)
From: neelk
2006-09-08 08:57 pm (UTC)
I think I like spines more, too, but for the pattern calculus thing I switched back to using the atomic/normal thing, on Jonathan's advice -- he told me to limit the number of weird things I introduces to the essential ones. He's right, but it's still kind of annoying.

As an aside, I think there's a cute little paper to be written that explains the various optimzations people do to compile curried functions in terms of focusing, because function abstraction is the only necessarily left-asynchronous operation you've got (intuitionistically, anyway), and you can stack them up and compile them in a batch.
(Reply) (Thread)