| Maybe the author plans to write about it in later parts of the article, but it's misleading to assume that (1) there is no work on types for interacting processes and (2) that types always have to be based on some underlying ideas form functional programming. 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. |
One of FP's more annoying achievements is somehow convincing people that it's the only way to make programs more verifiable or more "mathematical". Imperative, stateful computation can be (and is) just as mathematical (whatever that means) and just as verifiable as pure-FP (it must be constrained in some ways, but not as extreme as requiring complete referential-transparency).
It's good to learn about applying types to process calculi. I wasn't aware of that work at all.