We take a look at the programming language Æff and $\lambda_æ$-calculus on which Æff is based. The main feature of the $\lambda_æ$-calculus is the ability to run asynchronously in conjunction with parallel execution. This is accomplished by continuing to perform operation’s continuation while it waits to receive a response in the form of an effect from another process. Once it receives the response, it processes it appropriately and execution resumes. We extend the basic version of the $\lambda_æ$-calculus with recursive promises, mobile types, and dynamic processes. Recursive promises allow the program to be able to respond to multiple effects with the same operation name. Mobile types allow you to send higher-order values between parallel processes, especially functions. Dynamic processes allow you to create new processes on the fly as needed. We prove the progress and preservation theorem for the basic and extended $\lambda_æ$-calculus. We also mention some differences between the $\lambda_æ$-calculus and the actual implementation of the Æff language.
|
