Much recent research in programming languages is about types for interacting processes. The most well-known, but by no means only example are the session types pioneered by K. Honda. The key idea is that each process has a bunch of interaction points, and the interaction at each interaction point is constrained by a type. Such types typically
- What direction does data flow? E.g. channel x is used for input while channel y does only output.
- What kind of data is exchanged on the channel? E.g. x is used to exchange a boolean, while y exchanges pairs, the first component of which is a double, and the second component is a channel name which is used for inputing a string.
- How often is a channel used? E.g. x is linear (used exactly once), y is affine (used at most once) while z can be used an arbitrary number of times.
This setup has been investigated from many angles, and one of the most beautiful results in this space is that normal types known from lambda-calculus (e.g. function space) can be recovered precisely as special cases of such interaction types, using Milner's well-known encoding of functional computation as interaction.