Oliver Charles on Kleisli Arrows of Outrageous Fortune

Описание: Papers We Love London

May 20, 2015

Paper: https://personal.cis.strath.ac.uk/con...

For a long time, it wasn't clear how to get purely functional programs to actually "do" anything. Finally, a breakthrough came by sharing ideas from category theory to bring monads into functional programming, as a way to model and manage side effects. However, little has been done to ensure that entire interaction sequences make sense. For example, many functional programming languages will allow you to open a file handle, close it, and then try and read from it - clearly a nonsensical sequence of operations! In "Kleisli Arrows of Outrageous Fortune", Conor McBride shows us how we can borrow more ideas from the literature, introducing a new formulation of indexed monads - a structure with close connections to slice categories. Given these new tools, he demonstrates that these monads can correspond to enforcing logical properties - following in the tradition of propositions-as-types, we now have the ability to begin to encode Hoare logic pre- and post-conditions on our programs.

About Oliver:

Ollie has always had an interest in functional programming and correctness from a very early age - puzzled by how easy it seemed to make things go wrong, even by accident! Currently, he's the lead Haskell developer at the London startup Fynder, and spends the rest of his free time either working on open-source Haskell libraries, or exploring the latest functional programming research. One day, he hope's write software he can truly believe in, but there's a long way to go...