Résumé | Asynchronous programing is a widely spread technique offering some simple concurrent programing primitives that are restricted enough so that the resulting concurrent programs are, to some extent, dead-lock free. In this talk, I shall present the notion of monadic references that allows for formally defining a model of asynchronous concurrent programming as an extension of the usual model of (say) sequential monad programing.
I shall first review the notion of monadic programing, as popularized these last twenty years in typed functional programming languages such as Haskell. Then I will define in a progressive way what is asynchronous programing, how it relates with sequential programing, along with two series of simple equations capturing first, the basic semantics of promises and second, their asynchronous nature.
Various theorems derive from such an approach, formally proving the intuition long gain by programmers that, simply said, asynchronous concurrent programing with promises is as at least as simple as sequential programing, but with additional smoothness and optimisations possibilities provided by light concurrency.
If time permits, we may eventually prove that promises of (monadic) streams of data can be defined as (monadic) streams of promises of data, offering thus safe and robust ways to duplicate (monadic) streams in pure typed functional data flow programs. |