David Laing

Share

Haskell enthusiast
dlaing.org

Dave had programmed in a handful of mainstream languages for years and years. He came across Haskell along the way and made the decision to dive in. This has been followed by a lot of code, a handful of talks, and haranguing people to read various textbooks.

YOW! Lambda Jam 2015 Brisbane

Cofun with Cofree Comonads

TALK – VIEW SLIDES WATCH VIDEO

Monads, monad transformers and free monads are commonly used and understood, but the comonadic equivalents have received a lot less attention. The goal of this talk is to discuss comonads, comonad transformers, and cofree comonads.the different perspective they provide, and how they can be used as a better abstraction for some problems.

The first half of the talk will be building up the intuition for what comonads and comonad transformers are for and how you can use them.

This will be done by comparing and contrasting various comonadic entities with their monadic equivalents, poking around with some concrete instances, and demonstrating some examples of comonads and comonad transformers in use.

The second half of the talk will be about cofree comonads, how they relate to free monads, and how we can use them together to do exciting things.

We’ll start with a quick recap of free monads, which we’ll use to develop a little language which will be the basis for our running example.From this we’ll develop a corresponding cofree comonad while explaining the intuition behind them, after which we’ll show how they can be made to work together.

We’ll end with a demonstration of how this is useful, and a whirlwind tour of some of the opportunities this opens up.


Software Foundations Workshop

WORKSHOP/JAM

The Software Foundations syllabus first teaches theorem proving in Coq, without any prerequisites other than basic functional programming. It then gives a broad introduction to Programming Language Theory, completely formalised in Coq. Created by Benjamin Pierce and co-contributors at the University of Pennsylvania, it is freely available, and has been used in several university-level courses.

http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

Programming Language Theory is of interest to anyone who values working software systems, because it gives us tools for understanding the precise meanings of our programs, and the properties of the languages we use to build our programs. And theorem proving is a powerful discipline for challenging our beliefs that we know what we’re doing.

Although Software Foundations is self-contained and suited to self-study, it is easy to be intimidated by such a lengthy course on a topic and using tools that might be considered academic. However, the presenters firmly believe that formalising PLT in Coq actually makes it much more accessible for programmers. Fair warning: it’s also addictive.

In this workshop, you’ll find a supportive and collaborative environment in which newcomers to theorem proving and PLT can begin to explore this discipline, and the more experienced can refine their knowledge. The presenters will demonstrate a selection of exercises and techniques throughout the workshop, including some from early parts of the course, to help people get started, and some from latter parts, as a taste of what’s to come.

Please come prepared…

To make the most of the time available at the workshop, you should bring a laptop with some software already installed. Head over to this address, where we will provide some resources to help you get set-up for the workshop:

http://software-foundations.bfpg.org/