Lambda the Ultimate

Session types greatly augment purely functional programming. Session types enable pure functions to directly model process networks and effects.

We can adapt session types to pure functions by first reorganizing function calls of form `(A, B, C) -> (X, Y)` to a form that uses distinct, labeled input and output parameters, like `fn(in A, in B, in C, out X, out Y)` which we can easily rewrite to a sequential session type `?A ?B ?C !X !Y`. I'm assuming the parameters are easily distinguished, either by distinct data type or by augmenting with named parameters (such as `a:int` vs `b:int`).

Sequential session types conveniently represent that intermediate outputs are available before all inputs are provided. A simple reordering to `?A !X ?B ?C !Y` would correspond to a conventional function type `A -> (X, (B, C) -> Y)`. However, in contrast with the conventional type, the session type is recognizably a subtype of `?A ?B ?C !X !Y` or even of `!X ?A !Y ?B !D`. Thus, we can eliminate most adapter code to relax ordering in the caller. Further, a functional language designed for session types can easily support a direct programming style, e.g. based on imperative reads and writes to single-assignment parameters, thus avoiding the noise of continuation-passing style.

Sequential sessions already demonstrate a trivial model of interaction: the caller can observe the intermediate output `X` before computing inputs `B` and `C`. We can also model 'plain old structured data' types as unidirectional sessions, e.g. a type `!x:int !y:int !z:int` is essentially a record value with labels x, y, z.

Session type systems usually also support choice and recursion.

We can adapt 'choice' to pure functions by assigning a choice-label to a choice parameter and this label determines which subset of choice-specific parameters we'll use. A simple example:

type IF = &{ add: ?x:int ?y:int !r:int
           | negate: ?x:int !r:int
           }

With this definition in scope, the session type `?method:IF` could represent an external choice of 'method'. The choice-label `add` or `negate` might be assigned to implicit parameter `method.case`, and the label chosen will determine whether we further use parameters `in method.add.x : int`, `in method.add.y : int`, and `out method.add.r : int` or `in method.negate.x : int` and `out method.negate.r : int`. This is an exclusive choice, so a compiler could safely 'overlap' memory for these five parameters, similar to a C union. But unlike a conventional union or variant, the choice determines both inputs and outputs. Choice session types can conveniently model object-oriented interfaces or singular request-response interactions.

Aside: Session type systems distinguish external choice (&) vs internal choice (⊕). In the adaptation to functional programming, whether a choice is external or internal is based on whether the 'choice parameter' like 'method' in is input or output. However, it's convenient to represent some choices from the 'external choice' perspective. Thus, use of `&` above allows the type to be syntactic sugar for `{ add: !x:int !y:int ?r:int | negate: !x:int ?r:int }`. When we later provide this type as input, via `?method:IF`, the label is input and all the `!` and `?` types are flipped.

Recursive session types can further augment our functions with unbounded trees or streams of interactions. Conceptually, they allow functions to have an unbounded set of parameters, each with a unique 'path' name. A demand-driven stream type might have a form: `type Stream x = &{quit | more: !hd:x ?tl:Stream x}`. Whether a demand-driven stream has more elements is chosen by the receiver, not the sender. (Session types can also model normal streams, push-back streams, and others.) In context of recursion, our pure function logically has parameters of form `more.tl.more.tl.more.hd`, where `(more.tl)*` may recur in the parameter name an arbitrary number of times.

Use of recursive session types is similar to conventional functional programming with tree-structured data. A compiler or garbage collector can recycle memory for parameters that become irrelevant to further computation. Session types can represent many useful evaluation strategies such as call-by-need or bounded-buffer pushback. Intriguingly, session types can model 'algebraic effects' via recursive streams of request-response choice sessions.

Beyond sequencing, choice, and recursion, we can also extend functional programming with 'concurrent' sessions to represent partitioned data dependencies. For example, with function type `(A,B,C) -> (X,Y,Z)` it's possible to have a data dependency graph of form `(A,B) -> X; (A,C) -> Y; (B,C) -> Z`. It can be convenient to represent this precise data dependency graph in our session type. Fortunately, it's a simple extension to add concurrent types (though concise description, avoiding redundant expression of dependencies like `A`, is non-trivial).

Session types give us a rich model for interaction with pure function calls.

Implicitly, these interactions are between the 'call' and 'caller'. Fortunately, it is not difficult for a session-typed functional programming language to support 'delegation' such that we tunnel handling of interactions to another function call. When we begin to delegate long-lived sessions (e.g. recursive streams) between functions, the program begins to take a form of a 'process network' where pure functions are the processes and delegation models the wiring between them. Use of session types and delegation for purely functional process networks will subsume Kahn Process Networks (KPNs), which are limited to simple streams as the only interaction between processes. With session types, we can effectively model processes that rendezvous, coroutines, processes that have clear bounds on input and output, clear termination behavior.

As a summary, session types for purely functional programming supports:

• a more convenient alternative to continuation passing style
• function types able to directly represent object-oriented interfaces
• a surgically precise alternative to 'call-by-need' vs 'call-by-value'
• streaming request-response interactions for rendezvous or effects
• process networks that tunnel interactive sessions between function calls
• process models and interactions more flexible than Kahn Process Networks
• opportunity to fuse loops and optimize dataflow within the network
• type safety, subtyping, and progress guarantees for all of the above

Session types greatly improve this does not compromise functional abstraction or functional purity, except insofar as unbounded interactions with functions are not what we usually imagine from the mathematical connotations of 'function'.

I have not searched hard for prior art on the subject of session types exposing partial evaluation of pure functions as a basis for interaction and deterministic concurrency. I would not be surprised to discover all this is known in obscure corners of academia. But to me, who has recently 'discovered' this combination, this seems like one of those 'obvious in hindsight' features with an enormous return on investment, which all new functional programming languages should be seriously pursuing.