Abstract

Ideas from Girard’s linear logic have been applied to many programming language problems, ranging from alias analysis and memory management to protocol enforcement and session types. Despite these success stories, we have yet to see support for linear types in a general-purpose functional language. We conjecture that this is because traditional formulations of linear types can lead to awkward programming models or interact poorly with other language features like polymorphism.

In this talk, I will present F^o, a variant of System F that uses kinds to distinguish between linear and unrestricted types. This design is intended to be simple, familiar, and expressive: F^o lets programmers enforce their own protocol abstractions through the power of linearity and polymorphism, yet its typing discipline is lightweight enough to expose in a surface language.

I will illustrate F^o’s utility through examples and compare its support for linearity to alternative designs, namely type qualifiers and the ! modality.

This is joint work with Karl Mazurak, Jianzhou Zhao, and Aileen Zheng at the University of Pennsylvania.