[PL-sem-jr] Talk monday 8/16, 14:00

[Vincent St-Amour]

Mon 8/16 Room WVH166 14:00-16:00

Aaron - What I almost did this summer

One application of linear types is performing imperative update in a
pure setting: when a term has the sole reference to an object, it can
update that object without destroying referential transparency.
Historically, these updates are written in an explicit fashion and are
meant for large objects such as arrays.  What if, instead, we tied
updates to pattern matching on algebraic data, giving a form of heap
recycling?

I'll show how this technique, plus a few other tricks, makes it
possible to write hairy imperative programs in an appealing,
functional style.  Along the way we will see zippers, derivatives,
dissections, and Deutsch-Schorr-Waite algorithms.

Ultimately this work was halted a month into my internship, after we
discovered closely-related prior work.  But there are some new ideas
here, and room to go forward.