I wish I had the time and energy to properly grok your research. It seems fantastically interesting.
If you have two weeks in July, you could come to OPLSS and learn about it!
Do you think "fantastically interesting" is actually an intrinsic property of anything? I wonder if maybe anything (well, anything sufficiently complex, I guess) can become fantastically interesting if you poke at it long enough, and that it's actually pretty arbitrary which things people end up working on.
Edited at 2012-03-20 03:03 pm (UTC)
See my response to Chris below about OPLSS. It does sound like it would be fun though.
I think thinks are interesting to people correspondingly to their backgrounds; I think my background is right for your research to seem very interesting to me. (I like types, and I like dynamic languages, and I like systems.)
I think even if I could go, I'd feel kind of bad about being "the guy from Unaffiliated"? Like I was taking up a valuable slot that an Actual Researcher could use.
There's no harm in applying. If they don't have a slot available, then they don't have a slot available, but I've never actually heard of anyone being turned away.
Our friend Graham once had a paper accepted to a conference while he was unemployed. For his affiliation, he put his home address. It was kind of awesome.
Well, they say
, "The course is open to anyone interested. Prerequisites are knowledge of programming languages at the level provided by an undergraduate survey course." So you're probably in reasonable shape, background-wise. You can always watch last year's videos
(I've been wanting to do that myself) to get an idea of what it's about.
It looks like in 2011, there were 93 participants
, and by my count, 6 were "others". So you'd probably be a member of a quite small minority group. As would I.
Lately, 17 handwritten pages is a normal week for me. Most of them end up being trash, of course.
am i correct in understanding your observation as related to the idea that intersection types "don't have proof terms"? in a dynamic language, is it sensible to think of ∀α.τ as an infinite intersection, or does that miss something key about the parametricity implied?
I'm not sure. I think it's misleading to think of a ∀α.τ contract as a type at all. It looks like a type, but it's really just a marker that tells the operational semantics when and where to generate keys and seal certain values with them, or die trying. Those keys and seals, then, rather than a type system, are the mechanism by which parametricity is enforced.
Aww, missed you. Sounds like you had a high work/time ratio though.
Yeah. I didn't even tell Joel (my uncle) that I was coming to town, because it was such a work-focused trip. Maybe that was foolish, but I'm really eager to get this project done.
Instead, we have to say that two terms that are related to each other at the ∀α.τ contract are also related to each other at the τ contract, in an extended contract environment that has a binding for any free αs in τ.
This is also what you do when you don't have sneaky step-indexing tricks at your disposal. :) E.g., in the paper I wrote with Nick Benton, Adding Equations to System F Types
, we defined our logical relation by recursion on the structure of the well-formedness derivation for types, which meant that the interpretation had to be parameterized by a substitution, as well.
Yeah, but unless I'm misunderstanding it (I'm looking at figure 6), there you're talking about the relatedness of subterms ([A/α]e and [A/α]e'). We don't get to talk about subterms; we have to talk about the relatedness of the same terms at a different contract, which is why it feels so weird.
If we had given a Curry-style version of System F (ie, no explicit type abstractions or applications), then we'd have to relate the same terms at different types. It does feel weird, but this kind of thing also happens in models of intersection types, since kind of the point of intersection types is that there's no explicit marker in the syntax that type-related things are going on.
I don't mean to say contracts are types (since, well, they're not), but at least this one bit occasionally shows up in type-ish contexts as well.
Oh, yeah, I hadn't thought about about Curry-style F. I guess it's lack of explicit syntax for type applications and abstractions that makes the same-terms-at-different-types thing necessary, and although an untyped language is obviously one way to have that, it's not the only way. (And, in light of that, it makes sense that Chris brought up intersection types in her comment up above.)