?

Log in

No account? Create an account
Multi-language parametricity status update - Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

[ website | composition.al ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Multi-language parametricity status update [Mar. 20th, 2012|02:10 am]
Lindsey Kuper
[Tags|]

Last week, I went to Boston for a few days to work with Amal on our ongoing multi-language parametricity project. We got some solid work done before hitting a roadblock on Friday afternoon and realizing that we're going to have to go back and rework a number of things in order to show the second result that we want to have in our paper. Our first result -- that one can combine a static language that has parametric polymorphism with a dynamic language, and still have guaranteed parametricity in the combined language by way of a run-time "sealing" technique -- is feeling solid now, but the second result still needs a lot of work. It tries to leverage the first result to prove that parametricity is also guaranteed for contracted terms in a purely dynamic language (where the contracts are implemented by embedding dynamic terms in the static language at types that are the static counterparts to whatever contracts you want 'em to have, and then immediately embedding those terms right back in the dynamic language). You wouldn't think that proving this second result would be too much of a leap once the first result is in place, but there are some really nasty bits when you actually try to do it.

I did have a cute contracts-are-not-types realization on Thursday afternoon. In a dynamic language, there are no type variables, no type abstractions, and no type applications. So that means that when we define the relatedness of two untyped terms that have a ∀α.τ contract on them -- meaning that at runtime, they are supposed to behave like parametrically polymorphic functions -- we can't define it in terms of the relatedness of their subterms. In fact we can't even talk about their subterms, because we don't know anything about the structure of the terms to start with -- they can't be type abstractions, because those don't exist! 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 τ. At first, I was all, "Wait, what? Which type are they actually?", and then I realized that that was the wrong question.

Anyway, today I scanned and sent Amal the seventeen handwritten pages that I produced over the three days I was in Boston; they'll be a starting point for sorting out the remaining nasty bits. I'm not gonna lie: this project has been long and difficult, and I'm looking forward it to being done this year. (It will be done this year!) But I've gotten a lot out of it; Amal pointed out that if I go to OPLSS this summer, there won't be anything new to me in the material she's presenting. That was good to hear -- both because it makes me feel like I've truly learned something, and because a little break, in between trying to absorb new material from all the other OPLSS speakers, will be most welcome if I do go.

LinkReply

Comments:
[User Picture]From: gwillen
2012-03-20 07:20 am (UTC)
I wish I had the time and energy to properly grok your research. It seems fantastically interesting.
(Reply) (Thread)
[User Picture]From: lindseykuper
2012-03-20 02:55 pm (UTC)
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)
(Reply) (Parent) (Thread)
(Deleted comment)
[User Picture]From: gwillen
2012-03-20 09:26 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.)
(Reply) (Parent) (Thread)
(Deleted comment)
[User Picture]From: gwillen
2012-03-20 09:24 pm (UTC)
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.
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2012-03-20 09:37 pm (UTC)
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.
(Reply) (Parent) (Thread)
[User Picture]From: gwillen
2012-03-20 09:55 pm (UTC)
Heh!

I guess I could apply. The application page: http://www.cs.uoregon.edu/Research/summerschool/summer12/registration.html does not sound very friendly towards "others". Remember, not only do I not have an affiliation, I also don't have a PhD. Or any real formal background in the subject, beyond a single course at the undergraduate level.
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2012-03-21 02:58 am (UTC)
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.
(Reply) (Parent) (Thread)
(Deleted comment)
(Deleted comment)
[User Picture]From: lindseykuper
2012-03-20 06:31 pm (UTC)
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.
(Reply) (Parent) (Thread)
[User Picture]From: mindstalk
2012-03-20 06:14 pm (UTC)
Aww, missed you. Sounds like you had a high work/time ratio though.
(Reply) (Thread)
[User Picture]From: lindseykuper
2012-03-20 06:48 pm (UTC)
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.
(Reply) (Parent) (Thread)
From: neelk
2012-03-22 09:44 am (UTC)
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.
(Reply) (Thread)
[User Picture]From: lindseykuper
2012-03-22 07:12 pm (UTC)
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.
(Reply) (Parent) (Thread)
From: neelk
2012-03-22 07:53 pm (UTC)
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.
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2012-03-23 02:48 am (UTC)
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.)
(Reply) (Parent) (Thread)