Lightweight linear types in system f°
Karl Mazurak, Jianzhou Zhao, Steve Zdancewic · 2010
We present System F°, an extension of System F that uses kinds to distinguish between linear and unrestricted types, simplifying the use of linearity for general-purpose programming. We demonstrate through examples how System F° can elegantly express many useful protocols, and we prove that any protocol representable as a DFA can be encoded as an F° type. We supply mechanized proofs of System F°'s soundness and parametricity properties, along with a nonstandard operational semantics that formalizes common intuitions about linearity and aids in reasoning about protocols.