On implicit program constructs

Session types are a well-established approach to ensuring protocol conformance and the absence of communication errors such as deadlocks in message passing systems. Implicit parameters, introduced by Haskell and popularised in Scala, are a mechanism to improve program readability and conciseness by allowing the programmer to omit function call arguments, and have the compiler insert them in a principled manner at compile-time. Scala recently gave implicit types first-class status (implicit functions), yielding an expressive tool for handling context dependency in a type-safe manner. DOT (Dependent Object Types) is an object calculus with path-dependent types and abstract type members, developed to serve as a theoretical foundation for the Scala programming language. As yet, DOT does not model all of Scala’s features, but a small subset. Among those features of Scala not yet modelled by DOT are implicit functions. We ask: can type-safe implicit functions be generalised from Scala’s sequential setting to message passing computation, to improve readability and conciseness of message passing programs? We answer this question in the affirmative by generalising the concept of an implicit function to an implicit message, its concurrent analogue, a programming language construct for session-typed concurrent computation. We explore new applications for implicit program constructs by integrating theminto four novel calculi, each demonstrating a new use case or theoretical result for implicits. Firstly, we integrate implicit functions and messages into the concurrent functional language LAST, Gay and Vasconcelos’s calculus of linear types for asynchronous sessions. We demonstrate their utility by example, and explore use cases for both implicit functions and implicit messages. We integrate implicit messages into two pi calculi, further demonstrating the robustness of our approach to extending calculi with implicits. We show that implicit messages are possible in the absence of lambda calculus, in languages with concurrency primitives only, and that they are sound not only in binary session-typed computation, but also in multi-party context. Finally we extend DOT to include implicit functions. We show type safety of the resulting calculus by translation to DOT, lending a higher degree of confidence to the correctness of implicit functions in Scala. We demonstrate that typical use cases for implicit functions in Scala are typably expressible in DOT when extended with implicit functions.