Robert Atkey, a computer science researcher, writes about type theory, programming language semantics, and links between logic and programming such as Make as proofs.
HN commenters point to his quantitative type theory work, which Idris successor Blodwen builds on, and enjoy his posts on Make and conservation laws.
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
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-parametricity.html
[3] http://ps.informatik.uni-tuebingen.de/research/ilc/
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-parametricity-to-conservation-laws#notes
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
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/