POPL and PLaneT and type theory
Hi all, and apologies for the lack of updates; unfortunately I've been busy and haven't really had much time to tell you all what I've been up to. Anyway, over last week I was in sunny Charleston, South Carolina for POPL 2006. It was pretty great; I've got some notes, but unfortunately I don't have time right now to type them all up so I'll save that for another day. I will point you to "Environment Analysis via ΔCFA", a pretty crazy and interesting extension of Olin Shivers' CFA technique by Matthew Might and Shivers himself. I award it high marks even though it does use "via" in the title (yes, I'm aware I've done the same thing, but now I'm embarassed about it).
While I was there, though, I did manage to pick up a copy of The Reasoned Schemer, and I even got it signed by Will Byrd. (Sadly, Dan Friedman left before I got the book, and Oleg wasn't there at all as far as I could tell.) I haven't worked through very much of it yet, but what I've read so far has been fantastic. Very much in keeping with the other Schemer books, it's whimsical but fathoms deep at the same time. Great stuff, I can't wait to work through the whole thing.
Also while I was there I managed to advertise PLaneT around to all the Schemers there who hadn't heard of it. Self-promotion is pretty awkward for me, but it really surprised me to see how many people who were knowledgable about Scheme and even PLT Scheme who didn't know what it was. I think I need to figure out a better way to get people to know it exists; particularly for a tool like PLaneT it's really important that everyone know about it.
Speaking of PLaneT, I've been working on it recently; I just put out some improvements and I expect there'll be more before too long. Right now the user story is pretty good, but the developer story is lacking; there are lots of tiny little gotchas that aren't a big deal if you know what's going on but are pretty unfriendly to people who don't. Some particular examples that have happened in practice: developers not realizing that planet requires aren't like lib requires; developers writing code whose compiled form cannot be written to file; developers not realizing that planet package version numbers are different from their own provided version numbers; developers making packaging errors because they develop things as a collection and release it as a planet package; and so on. I'd rather have these problems never arise than to be able to smugly point out to the authors of broken packages that they should've read the documentation more carefully.
One more thing, a really surprisingly fun and frustrating puzzle from a type theory class I'm taking: assume you've got the simply-typed λ-calculus with base type T, but no constants that have that type. Prove that there are no terms at all of type T. Once you've done that, for more fun, add the special expression Omega with type T -> T and evaluation rule Omega --> Omega and prove the same thing again. It seems completely obvious, but I found proving it frustratingly difficult.
While I was there, though, I did manage to pick up a copy of The Reasoned Schemer, and I even got it signed by Will Byrd. (Sadly, Dan Friedman left before I got the book, and Oleg wasn't there at all as far as I could tell.) I haven't worked through very much of it yet, but what I've read so far has been fantastic. Very much in keeping with the other Schemer books, it's whimsical but fathoms deep at the same time. Great stuff, I can't wait to work through the whole thing.
Also while I was there I managed to advertise PLaneT around to all the Schemers there who hadn't heard of it. Self-promotion is pretty awkward for me, but it really surprised me to see how many people who were knowledgable about Scheme and even PLT Scheme who didn't know what it was. I think I need to figure out a better way to get people to know it exists; particularly for a tool like PLaneT it's really important that everyone know about it.
Speaking of PLaneT, I've been working on it recently; I just put out some improvements and I expect there'll be more before too long. Right now the user story is pretty good, but the developer story is lacking; there are lots of tiny little gotchas that aren't a big deal if you know what's going on but are pretty unfriendly to people who don't. Some particular examples that have happened in practice: developers not realizing that planet requires aren't like lib requires; developers writing code whose compiled form cannot be written to file; developers not realizing that planet package version numbers are different from their own provided version numbers; developers making packaging errors because they develop things as a collection and release it as a planet package; and so on. I'd rather have these problems never arise than to be able to smugly point out to the authors of broken packages that they should've read the documentation more carefully.
One more thing, a really surprisingly fun and frustrating puzzle from a type theory class I'm taking: assume you've got the simply-typed λ-calculus with base type T, but no constants that have that type. Prove that there are no terms at all of type T. Once you've done that, for more fun, add the special expression Omega with type T -> T and evaluation rule Omega --> Omega and prove the same thing again. It seems completely obvious, but I found proving it frustratingly difficult.
posted by Jacob Matthews at
20:49
0 Comments:
Post a Comment
<< Home