4 ms·
To the best of my knowledge, the insight that function application (and other control structures) can be seen as special cases of message passingh comes from th
by mafribe 11y ago
To the best of my knowledge, the insight that function application (and other control structures) can be seen as special cases of message passingh comes from the actor people [1, 2]. The first proper mathematisation is Milner's breakthrough encoding of lambda calculus in pi-calculus [3]. This lead to fine-grained investigations into what kinds of interaction patterns correspond to what kinds of functional behaviour (CBV, CBN, call/cc etc), which in turn inspired a lot of work on types for interacting processes.
I don't remember off the top of who first showed that parallel computation has no 'good' encoding into functional computation (lambda-calculus). I'll try to dig out a reference and post it here if I find it.
But the upshot of all this is that message-passing is more fundamental than functions / function application.
[1] C. Hewitt, H. Baker, Actors and Continuous Functionals.
[2] C. Hewitt, Viewing Control Structures as Patterns of Passing Messages.
[3] R. Milner, Functions as Processes.
- tel 11y agoYou can take this work much further in an "FP" kind of way by noting that the pi calculus is a good proof system for linear logic. Frank Pfenning has some lectures on this.
- mafribe 11y agoI don't fully agree with Pfenning here. The pi-calculus is not that good a proof system for linear logic: pi-calculus imposes sequentiality constraints on proofs that impede parallelism. Take for example the term x!<a> | y!<b> | x?(c).y?(d).P You have to sequentialise the two possible reductions on x and y. The culprit is the pi-calculus's input prefix, which combines two operations: blocking input and scoping of the bound variables (here c and d). This sequentialisation is not true to the spirit of linear logic proofs (think e.g. proof nets). Conversely, I don't think linear logic is a good typing system for pi-calculus for a variety of reasons: among them that linear logic does not track causality well, and because it doesn't take care of affine (at most once) interactions well.
- tel 11y agoThese are good points and I'll have to consider them. I was planning on going back through Pfenning's notes again in a bit and I'll keep a more critical eye this next time. Thanks! (Also, to be clear and with reference to other threads we've conversed on here, I think of linear logic and pi calculus, even if they aren't well-corresponding, as fantastic, unavoidable examples of non-function-application style programming.)
- discreteevent 11y agoThanks very much for that. I'll read them all. (I did a bit of reading around actors before including some Hewitt but didn't pick up on the message passing equivalence. Will read closely. The Milner paper looks very interesting)