Lightweight Functional Session Types

Session types describe communication protocols, capturing both the type and the order of messages. Recently, we presented a se-mantics for a core session-typed linear λ-calculus, GV, and proved that it enjoys a number of desirable properties beyond type sound-ness, including deadlock freedom, determinism (and hence race freedom), and termination. In this paper, we modularly extend GV with practical features. We begin by introducing FST (System F with Session Types), an extension of GV, with features including polymorphism, row typing (to support extensible records, variants, and session types), and a subkinding system (to integrate linear and unlimited types). FST preserves all of GV’s desirable properties. We then consider further extensions of FST with recursion and recursive types, which preserve all of the properties save for termination. Finally, we consider an additional extension of FST with access points (a much more expressive mechanism for initiating communication among threads) in return for giving up deadlock freedom, determinism (and indeed race freedom), and termination. Building on the formal development, we discuss the design of Session Links, a session-typing extension of the Links web programming language and a full implementation of FST. 1