London - May 20, 2015
Oliver Charles on Kleisli Arrows of Outrageous Fortune
- Meetup: http://www.meetup.com/Papers-We-Love-London/events/222094026/
- Paper: https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf
Description
Oliver Charles presents Conor McBride's "Kleisli Arrows of Outrageous Fortune".
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.
Bio
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…
The London Chapter would like to thank uSwitch for helping to make this meetup possible.