Robert Atkey

It's not a thesis, but one of my favorite acknowledgements is from Bob Atkey's paper on quantitative type theory (which assigns quantities of 0, 1, or ω to types): > This work is dedicated to Orwell the dog. Orwell was a good dog and knew well the difference between zero, one, and many. https://bentnib.org/quantitative-type-theory.pdf

Does anyone know if there has been any work in formalizing incremental compilation? It would be great to have some sort of theoretical framework to use as a guide when implementing various incremental compilation strategies. There is some (ongoing?) work on low-cost incremental computation by differentiating lambda calculi [1] [2] [3], and it seems like an incremental compiler could maybe be a good use case for it. [1] http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/ [2] http://bentnib.org/posts/2015-04-23-incremental-lambda-calculus-and-pa… [3] http://ps.informatik.uni-tuebingen.de/research/ilc/

Are you familiar with this? https://bentnib.org/conservation-laws.html

Two fun blogs posts in this vein https://bentnib.org/posts/2015-04-17-propositions-as-filenames-essence… http://conal.net/blog/posts/the-c-language-is-purely-functional

A good foundation for such a language would be one based on Quantitative Type Theory [0]. It’s a dependent type theory that records usage information in every typing judgement. The Idris successor, Blodwen [1] is being based on it. [0] https://bentnib.org/quantitative-type-theory.pdf [1] https://github.com/edwinb/Blodwen

String diagrams are a way to describe morphisms (think functions) in monoidal categories. A construction using monoidal categories (or a slight generalisation) can be used to give a categorical model for arrows. http://bentnib.org/arrows.pdf This gives rise to these diagrams: https://www.haskell.org/arrows/

Glad you posted this, had tried to do the same earlier this year. Also related, this POPL paper shows how Noether's Theorem (the idea that every symmetry yields a conservation law e.g. rotational symmetry => angular momentum conservation) can be derived from applying parametric polymorphism to Lagrangian mechanics: http://bentnib.org/conservation-laws.html This summary of the above paper is much more comprehensible: http://ezyang.tumblr.com/post/74405137526/robert-atkey-from-parametric…

Here are two resources that are recent and more tutorial, introductory and/or applied than the OP paper. https://www.fpcomplete.com/user/bartosz/understanding-algebras http://bentnib.org/interleaving.pdf

This kind of typing is quite cool, but i didn't found it so well explained. The general pattern is to type programs not only with a type, but also with some "quantity", that quantity putting constraints on what is inside. Using quantities like "zero", "one" and "lots", you can get linear or affine typing, using quantities "public" & "private" you can get the kind of data leakage typing as presented, but you could easily also do classification levels (secret, top secret etc). I'm bluffing but i believe that this can also model rust-like lifetimes. What you want is that your quantities are a partially ordered semiring (or something slightly weaker): sum of quantities (eg a + b) will be used to compute the quantity of conjunction, eg a tuple; multiplication of quantities will be used to compute composition, eg for functions, if it takes an argument of quantity one, to a result of quantity q, then for an argument of quantity a, it will return a result of quantity a * q. And obviously the ordering relation is used for subtyping, eg "private" <= "public". https://bentnib.org/linear-metatheory.html (a non-dependently-typed version of the thing below) https://bentnib.org/quantitative-type-theory.html