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 "q

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 https://bentnib.org/linear-metatheory.html (a non-dependently-typed version of the thing below) https://bentnib.org/quantitative-type-theory.html https://bentnib.org/quantitative-type-theory.html