tim: Tim with short hair, smiling, wearing a black jacket over a white T-shirt (Default)
A bit over four years ago, I arrived at Mozilla in Mountain View for an internship on the Rust team. That internship became a full-time job when it became clear to me that I was no longer welcome in my Ph.D program.

A year and a half ago, I left Mozilla. I've had plenty of critical things to say about Mozilla, and a few critical things to say about the Rust team specifically. That doesn't change the fact that working on Rust made me feel like I was part of something again, and that it turned how I felt about my career in software into a much more positive direction. There were ups and downs, but during the best times, working with the Rust team was the most positive experience of my professional life over the past 15 years. Not to get too sentimental, but there is a certain way in which it saved my life.

During my two and a half years on the team, the pressure to get to 1.0 and the uncertainty over what that would mean were constant presences. It was a goal that, I think, provided mostly positive stress, but I could feel the worries about when it was ever going to happen, if it was ever going to happen. Everyone who worked on Rust wanted it to succeed, but the problems that usually happen whenever several driven and creative people try to collaborate happened, and made it harder to come to agreement over what 1.0 was going to mean and when it should happen.

I haven't followed Rust development since I left, but hearing that Rust 1.0 has been released today means a lot to me even so. Congratulations to everyone involved, but especially to [personal profile] graydon2, without whom none of this would have happened.
tim: Tim with short hair, smiling, wearing a black jacket over a white T-shirt (Default)
These notes are about Wednesday, September 3.

The first talk I went to was Carlo Angiuli's talk on homotopical patch theory. I understood very little about the actual new work in the talk, but I'm very glad to finally have at least a vague sense of what homotopy type theory is about (though I no longer remember how much of that came from the talk, and how much came from talking to Carlo and to Ed Kmett the day before :) I was about to write down my hand-wavy summary of what I think it's about, but I realized it's too hand-wavy to even write down. But, I want to read more about it, and if you're curious, so can you!

The next talk I went to was Niki Vazou's talk on refinement types for Haskell. Refinement types are cool, but sadly, I lost the thread (totally my fault in this case) somewhere after Vazou said something about using refinement types to prove termination for themselves. At that point, I wrote down an outraged little comment on my notepad that ended with a note to myself to read the paper. The other thing about this talk that I noted, which I hate to mention -- but really, what I hate is that it's even noteworthy at all -- is that during the Q&A period, a woman asked a question at a talk given by a different woman. This was the 10th ICFP I've attended, and I'm pretty sure this was the first time I've seen that happen at ICFP.

Then I missed most of Conor McBride's talk "How To Keep Your Neighbors in order" indirectly due to listening to Ed tell his (edited, I'm sure) life story. If you get the chance, you should ask Ed his life story; he may be the closest person to a character in a Hunter S. Thompson book who you're likely to meet at a computer science conference.

Next (for me) was Simon Marlow's talk "There is no Fork: an Abstraction for Efficient, Concurrent, and Concise Data Access", which was probably the best talk title of ICFP 2014. Simon talked about his work on Haxl, motivated by wanting an implicitly concurrent language for fetching data incrementally and lazily. This reminded me a bit of what I overheard when I was working on Rust about Servo's incremental layout, but I don't remember it well enough to know if that's a red herring or not. I'll be interested to read the paper and see if there's any comparison with Erlang, as well.

Jeremy Gibbons began his talk "Folding Domain-Specific Languages: Deep and Shallow Embeddings by saying that his co-author Nicolas Wu couldn't be there because "he has taken delivery of a new baby". Which was funny, but possibly took someone else out of the picture a bit ;) The talk was helpful to me since I spent four years at Portland State hearing people talking about deep and shallow embeddings without knowing what that meant, and now I do. Deep embeddings are syntax-driven and shallow embeddings are semantics-driven (unless it's the opposite); in a shallow embedding, operations are functions in the host language and in a deep embedding, operations are types in the host language (ditto). It's a similar dichotomy to the expression problem. I wrote in my notes "Somehow you can turn context-sensitive interpretations into compositional ones (read the paper)". At that point, I was literally too tired to stand up, so I'm just pleased with myself for having remembered this much!
tim: A person with multicolored hair holding a sign that says "Binaries Are For Computers" with rainbow-colored letters (binaries)
These notes are about Tuesday, September 2.

I caught the end of Robby Findler's invited talk on behavioral software contracts. That was enough to catch a point that I found thought-provoking: that contracts aren't a subset of types, because contracts can express protocol-based properties (similarly to how session types do), which fundamentally involve assignment. I'm still mulling it over, and I should probably just watch the whole talk, but it might be the answer to a question that has plagued me for years, which is: "are contracts just type signatures that you put in a comment?" (Not meaning to participate in a holy war here -- I assume the problem is my lack of understanding.)

If that's true, it reminds me of typestate in Rust, which I implemented for my intern project and which was later removed from the language. Or, maybe, Rust's typestate wasn't as powerful as contracts are, and that's why people didn't find it useful in practice. I do remember always being really confused about the interaction between typestate and assignment -- we went back and forth between thinking that typestate predicates should only be able to refer to immutable variables, and thinking that we'd take the YOLO approach and leave it as a proof obligation for the user that mutation can't cause unsoundness. So maybe if I had understood contracts at the time, the whole thing would have gone better. In any case, I'd like to read more so that I can articulate the difference between typestate and contracts.

I caught slightly more of David Van Horn's talk on soft contract verification, though I missed part of that talk too. The principle here is to allow assigning blame when an assertion fails at runtime: then, you can write your code so as to have strong enough contracts so that your code is to blame as infrequently as possible when something goes wrong (if I understood correctly, anyway). ("Blame" is a technical term introduced by Dimoulas, Findler, Flanagan, and Felleisen, at least if I have the correct initial reference.) As in soft typing, "soft" here means that the contract checker never rejects a program -- it just introduces runtime checks when it can't convince itself of a particular safety property at compile time. This also recalls Rust typestate for me, which had a very similar approach of falling back to runtime verification (actually, in Rust, all typestate assertions were verified at runtime; we thought that would be a simpler approach, and if the feature had persisted, we might have implemented some sort of analysis pass to eliminate some of the dynamic checks). In my copious free time, I'd love to revisit Rust typestate and compare and contrast it with the work presented in these two talks, as well as gradual typing and effect systems, maybe even as a paper or experience report. (Which, of course, would involve me learning about all of those things.) I want to say that Rust typestate did have an analogous notion to blame: it was all about forcing each function to declare its precondition, so that if that precondition was violated at runtime, we knew it was the caller's fault, not the callee's. But I'd like to read the paper to see how much of a role inference plays.

As a much more trivial aside, I really liked that Van Horn used ⚖ as an operator, at least in the slides (as in, C ⚖ M). There should be more Unicode operators in papers! It's 2014; we don't need to limit ourselves to what was built into a 1990s-era version of LaTeX anymore.

In any case, the parts of Van Horn's and Findler's talks I heard made me think "this is the right way to do what we were trying to do with typestate". I want to be sure I believe that, though. I say this because their approach to handling mutation is to statically check any contracts that don't involve assignment -- other contracts revert to runtime checks, but the checks always happen, either statically or dynamically. My memory is hazy, but in the context of Rust, I think we talked about introducing additional precondition checks at each use of a variable involved in a typestate predicate, but quickly decided that would be inefficient. In any case, those two talks made me want to revisit that work, for the first time in a while!

I missed most of Norman Ramsey's talk "On Teaching How to Design Programs as well, but the paper seems worth reading too. Two things I did catch: Norman saying "Purity has all sorts of wonderful effects" (I think in terms of helping students discipline their thinking and avoid just banging on the keyboard until something works, though I don't recall the context), and him making the point that the HTDP approach makes it easier to grade assignments based on how systematic the student's design is, rather than a laundry list of point deductions.

Next, I went to Richard Eisenberg's talk "Safe Zero-Cost Coercions for Haskell". I have painful memories of this line of work dating back to 2007 and 2008, when I was reviving the GHC External Core front-end and had to figure out how to adapt External Core to represent the new System FC type system features, which (to me at the time) seemed to make the Core type system twice as complicated for unclear benefit. (External Core was removed from GHC some years later, alas.) I'm willing to say at least provisionally, though, that the work Eisenberg presented cleans up the coercion story quite a bit. I also appreciated the motivation he gave for introducing coercions into the type system at all, which I hadn't heard formulated quite like this before: you can typecheck System F just using algebraic reasoning, but when you want to introduce coercions (which you do because of GADTs and newtypes), contravariance ruins everything. I think a way to summarize the problem is that you get overlapping instances, only with type families rather than just type classes.

To solve the problem, Eisenberg and colleagues introduce two different equality relations: nominal ~, and structural ~~. This allows the type system to incorporate coercions based both on nominal type equality, and structural type equality, without having to pick just one. Then, each type parameter gets a "role", which can be either "structural" or "nominal". This allows coercion kinds (my nemesis from the External Core days) to just go away -- although to me, it seems like rather than actually taking coercions out of the kind system, this approach just introduces a second kind system that's orthogonal to the traditional one (albeit a very simple kind system). I guess it's possible that separating out concerns into two different kind systems makes the implementation and/or reasoning simpler; also, as far as I can tell, roles are more restricted than kinds in that there's no role polymorphism. (I'm not sure if there's kind polymorphism, either, although there certainly was in GHC at least at some point.) Actually, there are three roles: "nominal" (meaning "this parameter name matters and is not interchangeable with structurally equal types"), "representational" (for a type that is interchangeable with any others that are structurally equal to it), and "phantom" (type parameters that are unused on the right-hand side of a definition). I wrote in my notes "I wonder if this sheds any light on Rust traits", but right now I'm not going to elaborate on that query!

The implications of the work are that generalized newtype deriving now has a safe implementation; the type system makes it possible to only allow unwrapping when the newtype constructor is in scope. (This, too, reminds me of a Rust bug that persisted for a while having to do with "newtype dereferencing".) The results were that the new role system uncovered three legitimate bugs in libraries on Hackage, so that's pretty cool. Also, Phil Wadler asked a question at the end that began with something like, "...here's how Miranda did it..." (Not something one hears a lot!)

Finally, I stayed for Fran├žois Pottier's talk "Hindley-Milner Elaboration in Applicative Style", which I understood more than I expected to! He began by saying something that I noticed long ago, but originally chalked up to my own stupidity: Algorithm W in its original presentation, was "imperative, and messy". We want a simpler, more declarative formulation of type inference. Pottier claims that conjunctions and equations are simpler than compositions and substitutions -- I agree, but I'm not sure if that's based on something objective or if that's just what works well for my brain. He defines a constraint language that looks like λ-calculus with existential types, which allows constraint solving to be specified based on rewriting. On paper, it's a declarative specification, but the implementation of it is still imperative (for performance reasons). It sounds like it might be fun to prove that the imperative implementation implements the declarative specification, though perhaps he is already doing that!

Stay tuned for my notes on day 3, when I get around to editing them.
tim: A person with multicolored hair holding a sign that says "Binaries Are For Computers" with rainbow-colored letters (binaries)
During this year's ICFP, I took probably more notes than I've taken at any other conference I've gone to. Now some of my notes were silly ideas or random to-do items that would have distracted me if I didn't write them down, but a lot of them were actually about the talks I was listening to, surprisingly enough!

In the interest of posterity, as well as justifying to my employer why it was a good idea for them to pay $3000 for me to go to an academic conference when I'm not a researcher, I'm going to try to summarize those notes here. What follows is my attempt to turn my notes on the first day (September 1) into something half coherent. I'll do a separate post for each day. I will try to link to the video from each talk.

The first talk of the day that I caught was Daniel Schoepe talking about SELinq. Yes, this is LINQ as in LINQ. He (and his coauthors Daniel Hedin and Andrei Sabelfeld) wanted to build on top of what LINQ already does -- making database queries typed -- to annotate types with "public" or "private". This means, probably, exactly what you'd think it would mean in an everyday sort of database application: for example, they applied their work to an example from the PostgreSQL tutorial site and showed that they could implement a rule that in a database of people, demographic info, and addresses, each person's exact address is private -- so queries can get aggregate data about what regions people live in, but a query that tries to look up an individual's street address would be ill-typed. That's really cool!

Schoepe et al.'s work is based on FlowCaml, which is an information flow analysis for OCaml. Crucially, the work relies on embedding the database query language in the underlying programming language, so you can piggyback on the host language's type system. That's cute! It also relies on baking operations like list append into the language, which is a little sad. (In my never-published -- and never-finished -- dissertation proposal, I wanted to explore using a combination of proofs and types to modularize the primitive operations of a language. I wonder if an approach like that would be useful here.)

They proved a soundness theorem that guarantees non-interference, and implemented a source-to-source compiler that generates F# code. Their type inference is conservative, which doesn't violate any intuitions: that is, it's always safe to treat public data as private. In future work, they want to apply it to front-end JS web apps, and in the question and answer session, Schoepe said it shouldn't be hard to generalize the work to arbitrary lattices (not just the one with "public" and "private").

After lunch, Paul Stansifer talked about binding-safe programming. The take-away line from Paul's talk was "Roses are olfactorily equivalent under α-conversion." (This might make more sense if you keep in mind that the name of the system he implemented is "Romeo".) Everybody knows that naming is one of the hardest problems in computer science; Paul presented a type system for naming. This pleases me, since I think nothing makes sense unless it's formulated as a type system. In his system, types track binding information: specifically, in a way that allows names to be shadowed safely. The type keeps track of which "direction" shadowing should go in. The running example was expanding let* (because this is in a Lisp-ish context) into lambdas.

The next talk I took notes on was by Lars Bergstrom, on higher-order inlining. (Paul and Lars are both former colleagues of mine from Mozilla, by the way, which is why I'm referring to them by their first names.) Lars presented an analysis that determines where it's safe to inline higher-order functions. This was interesting to me since I'd always thought of inlining higher-order functions as a very naughty thing to do; the first research papers I ever read, in undergrad, were about inlining, and I did my undergrad and master's thesis work on deforestation (which depends intimately on it), so this is a belief I've held for a long time! Lars showed that it's wrong, so that was cool. The central contribution of his work is an analysis that doesn't have to compare the entire lexical environment for equality. I would have to read the paper to explain why, but Lars said that his work provides principles that replace the bag of heuristics that was the previous state of the art, and for now, I believe him.

It's safe to inline a higher-order function if you know that its environment doesn't change dynamically: that is, that inlining won't change the meaning of the function's free variables. Lars' analysis answers the question "does any control flow path pass through a sub-graph of the control flow graph that constitutes a re-binding?" An interesting thing that Lars didn't say (but perhaps it's not as deep as I think it is) is that this touches on how closures and value capture are sort of a hidden side effect even in a pure, strict functional program. His conclusion was "You can use closures in benchmarks now!"

In the Q&A, I asked whether it was imaginable to prove that the analysis improves performance, or at least doesn't make it worse -- in other words, that the higher-order inlining optimization has a predictable effect on performance. This question has haunted me ever since I worked on type-based deforestation. Lars thought this would be very ambitious because inlining is often an enabler of other optimizations, rather than improving performance on its own; though it does inherently eliminate stack frame allocation and deallocation. He said that he and colleagues want to do a correctness (i.e. semantic preservation) proof, but haven't yet.

My last set of notes for the day was on Jennifer Hackett's talk "Worker/Wrapper Makes It Faster". As Lars said in answer to my question, Jennifer's work answers the question I asked, sort of: it's about proving that optimization really does improve performance. She has a proof strategy based on defining a "precongruence": a relation that's preserved by substitution; this is because the "natural" approach to proving performance improvement, induction based on execution steps, doesn't work for lazy languages. If a relation is a precongruence, intuitively, a local improvement always translates into a global one. I would have to read the paper before I said any more, but I thought this talk was cool because it contributes the first performance guarantee for an optimization for a lazy language.

Stay tuned for my notes on day 2, once I get around to editing them!
tim: Mike Slackernerny thinking "Scientific progress never smelled better" (science)
"...programming without loops and variables sounds as weird to me as doing maths without numbers..."

"...ML is a functional programming language, used mainly for mathematical algorithms and such like."

(Undergrads trying to understand programming languages are like dogs trying to understand quantum mechanics.)

Profile

tim: Tim with short hair, smiling, wearing a black jacket over a white T-shirt (Default)
Tim Chevalier

May 2017

S M T W T F S
 123456
78 910111213
14151617181920
21222324252627
28293031   

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags