Back to Search
Start Over
Lightweight linear types in system f°
- Source :
- Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation.
- Publication Year :
- 2010
- Publisher :
- ACM, 2010.
-
Abstract
- 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.We compare System F° to other linear systems, noting that the simplicity of our kind-based approach leads to a more explicit account of what linearity is meant to capture, allowing otherwise-conflicting interpretations of linearity (in particular, restrictions on aliasing versus restrictions on resource usage) to coexist peacefully. We also discuss extensions to System F^o aimed at making the core language more practical, including the additive fragment of linear logic, algebraic datatypes, and recursion.
Details
- Database :
- OpenAIRE
- Journal :
- Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation
- Accession number :
- edsair.doi...........b97c88b650dc6202c7658b734eed31d0