← Fun in Birmingham, March 2011Brighton, November 2012 →

Thanks for coming!

We all had a lot of fun this afternoon. Some of us stayed for dinner and requested the receipt.

Links to the slides are now available with the abstracts below.

Daniel James Says

The Next Meeting...

... of Fun in the Afternoon will be held at the University of Oxford on Tuesday the 28th of February. Everyone is welcome!

0

Registration

While not mandatory, it would really help us out if you filled out our short registration form.

Location

We will be hosting the event in the Department of Computer Science. Please use the reception entrance, which you will find on Parks Road. Please indicate that you have come for “Fun in the Afternoon” and you will be directed appropriately.

You will find a number of establishments indicated on the map below where you can purchase lunch. You may bring your lunch to the department and there is some seating available in the atrium.

Talks will be held in Lecture Theatre B and the atrium will be used as our social space during breaks.


View Fun in the Afternoon at the University of Oxford in a larger map

Schedule

12:00–13:30Gather with lunch in the atrium of the Computer Science Dept.
13:30–13:35Welcome
13:35–14:10Richard Bird: How to Link a List
14:10–14:40Tea and coffee break
14:40–15:15Josh Ko: Numerical representations à la ornamentation
15:15–15:50Matthias Görgens: Sneaking in Haskell
15:50–16:20Tea and coffee break
16:20–16:55Edwin Brady: Idris
16:55–17:30Duncan Coutts: Cloud Haskell
17:30–18:30Pub
18:30–Dinner

Abstracts

How to Link a List

Richard Bird

Department of Computer Science, University of Oxford

| Slides |

We discuss two ways to build a circular, doubly-linked list in Haskell. One way extends quite nicely to building a torus whose node-values are given by an array.

You may like to try this as an exercise before the talk.

Numerical representations à la ornamentation

Josh Ko

Department of Computer Science, University of Oxford

| Slides | Keynote |

The shape of a binomial heap resembles the binary representation of its size, and operations on binomial heaps look similar to those on binary numbers. This kind of containers whose implementations correspond closely to various positional number systems are called numerical representations by Okasaki in his seminal book on purely functional data structures. With McBride’s ornaments, such correspondence between container types and number types can be easily formalised. This talk will be a sketch of the formalisation, as a small and fun example of datatype-generic programming with dependent types.

Sneaking in Haskell

Matthias Görgens

Citrix Systems Research & Development Ltd.

We are working in an enterprise on an enterprise product. And we managed to sneak Haskell in. Here’s how and why. The enterprise is Citrix and the enterprise product is XenClient, a client side hypervisor aimed at helping IT departments cope with laptops.

Idris

Resource-safe Systems Programming

with Dependent Types

Edwin Brady

School of Computer Science, University of St Andrews

| Slides | Demo |

In this talk I will describe a new implementation of Idris, a Haskell-like functional language with dependent types. In particular, I will describe Idris’ new overloading notation which facilitates programming, modularity and reuse in Embedded Domain Specific Languages (EDSLs) and show how to use it to reason about safe resource usage and state management. The notation allows us to separate the structural language constructs from primitive operations, and lift precisely-typed functions into the EDSLs. In this way, we implement a generic framework for constructing state-aware EDSLs for systems programming.

Cloud Haskell

Duncan Coutts

Well-Typed LLP

| Slides |

Cloud Haskell is an exciting new realisation of an old idea for writing concurrent/distributed programs. It shamelessly steals the Erlang concurrency model of asynchronous message passing between lightweight processes, but implements it as a library in Haskell plus one small language extension. One of the key contributions was to find a modest language extension that allows everything else to be implemented as a library. This ability to implement the system in a library rather than directly in a language runtime system is a major advantage: it allows for much greater flexibility in implementations and means we do not need to write a new runtime system or do major surgery on our existing one. We get to keep our favourite language, libraries and tools but gain the ability to write programs for whole clusters or other more exotic environments.

Jeff Epstein, Andrew Black, and and Simon Peyton Jones introduced all this last year at the Haskell Symposium. In this talk we will describe their approach. We will talk a bit about some new implementation work we are doing to enable using network backends other than just TCP/IP, such as shared memory or HPC network hardware. Finally, we may speculate on where this technology could be pushed in the future.