Coming Up

09.05.2017 - Type-driven Development with Idris

posted 1 May 2017, 02:38 by Ed Lambda

Who: Edwin Brady
Where: Skyscanner, 15 Lauriston Place
When: 7:30pm, Tuesday 9th May, 2017

Title: Type-driven Development with Idris


This talk will be about the book "Type-driven Development with Idris" (, recently published by Manning, and there will be an opportunity to win a copy.

Idris is a general purpose functional programming language with first-class dependent types, building on state-of-the-art techniques in programming language research. Idris aims to make type-based program verification techniques accessible to programming practitioners while supporting efficient systems programming via an optimising compiler and interaction with external libraries.

In this talk, I'll use a series of examples to show how Idris can be used for verifying realistic and important properties of software, from simple properties such as array bounds checking, to more complex properties of networked and concurrent systems.

09.02.2016 - Developing a Haskell MOOC

posted 22 Jan 2016, 02:46 by Ed Lambda   [ updated 22 Jan 2016, 03:01 ]

Where Skyscanner's offices, 15 Lauriston Place. Map:
When 6:30pm Tuesday 9th February
Who Jeremy Singer, University of Glasgow

Title Developing a Haskell MOOC

The Massive Open Online Course (MOOC) is the latest trend in higher education, exposing university learning and teaching to anyone on the net. At Glasgow, we are developing a MOOC to teach Haskell to non-functional (!) programmers. Our #haskellmooc is due to launch in September 2016. In this talk I will give some background, preview our learning materials and hope to garner feedback from the audience.


12.11.2015 - Overloaded record fields for Haskell

posted 28 Oct 2015, 02:22 by Ed Lambda

When Thursday 12th November at 7pm
Where Skyscanner's offices, Quartermile One, 15 Lauriston Pl, Edinburgh
Who Adam Gundry, Well Typed.

So that Skyscanner know who they should expect entering their building, please get a free ticket from the EventBrite page.

Title Overloaded record fields for Haskell

A long-standing annoyance when using Haskell for large-scale
applications has been its rather limited record system.  In particular,
field names cannot be reused across multiple datatypes, and while the
record update mechanism is very expressive, it does not compose well.
Over the years there have been many proposals for better systems, but no
concrete progress on implementation.

This is the story of how I foolishly set out to "solve the records
problem" over the summer of 2013, and how over two years later I've
still neither quite succeeded nor failed.  I'll explain the new design
as it currently stands, showing how it decomposes into not one but three
separate language extensions, one of which provides interesting new
possibilities for writing programs that have nothing to do with records.
 While it is always dangerous to predict the future, I'll outline what
you can and can't expect to see from this work in the upcoming GHC 8.0.

13.10.2015 - optimising & scaling parallel Haskell

posted 28 Sep 2015, 11:26 by Ed Lambda   [ updated 28 Sep 2015, 11:27 ]

Title Profiling, optimising, parallelising and distributing Haskell code
When Tuesday 13th October.
Where The Outhouse pub, at 7pm.
Speaker Rob Stewart

I'll talk about those rare occasions when you don't just want to write Haskell programs,
but you also want to run them... and as quickly as possible. I'll cover code profiling and
optimisation, and go through the various ways to write parallel, and distributed, Haskell

14.07.2015 - Erlang meets Dependent Types

posted 28 Jun 2015, 12:09 by Ed Lambda   [ updated 28 Jun 2015, 12:10 ]

Speaker Sam Elliott.

When 14 July, *at SkyScanner's offices at 15 Lauriston Place*


Concurrent programming is notoriously difficult, due to needing to reason
not only about the sequential progress of any algorithms, but also about
how information moves between concurrent agents. What if programmers were
able to reason about their concurrent programs and statically verify both
sequential and concurrent guarantees about those programs’ behaviour? That
would likely reduce the number of bugs and defects in concurrent systems.

Erlang’s existing type system cannot produce particularly strong
guarantees, especially not with regards to concurrent systems. In this talk
I will describe work to integrate a dependently-typed language (Idris) with
Erlang, in order to integrate dependently-typed code with Erlang programs.
This work included both a new Idris code generator, and libraries for
reasoning about concurrent Erlang programs, including some OTP behaviours

This is a ticketed event. To get a ticket:

24.03.2015 - Vectorising the array-based SaC language

posted 10 Mar 2015, 04:40 by Ed Lambda

Who: Artem Shinkarov
Where: The Outhouse at 7pm
Title: Automatic data layout transformations enabling SIMD vectorisation

Usually programming languages use a fixed layout for logical data structures
in physical memory.  Such a static mapping often has a negative effect on
usability of vector units.  In the talk we will consider a compiler for a
programming language that allows every data structure in a program to have its
own data layout.

Such an approach comes with a number of challenges.  First, the number of
theoretically possible data layout configurations per program is very large.
We need to choose the one that will lead to the best program
vectorisation.  Secondly, we have to make sure that the chosen configuration
is sound.  Finally, the code we generate has to encode desired vectorisation
preferably in a portable way.

Our solution lies in using types to encode data layouts.  We
use a type system to verify data layout consistency in programs.  Type
inference techniques allow us to solve a data layout reconstruction problem.
We prove that type-implied transformations preserve semantics
of the original programs and we demonstrate significant performance improvements
when targeting SIMD-capable architectures.

10.02.2015 - Web programming with F#

posted 20 Jan 2015, 09:39 by Ed Lambda

When: 10th February, 2015
Who: Simon Fowler, University of Edinburgh
Title: Functional Web Programming in Links and F#

Functional programming has been shown to be a good fit for web
development. The Links functional web programming language
developed by Cooper, Lindley, Wadler and Yallop at the University
of Edinburgh allows client, server, and database code to be
written in a single language, while providing abstractions such
as formlets to allow form data to be retrieved in a structured,
elegant and type-safe manner. More recently, these ideas have
been picked up and expanded upon in IntelliFactory's WebSharper
web framework, which embeds many of the concepts in the .NET
functional-first language F#.

In this talk, I'll take a look at Links and WebSharper, comparing
the approaches taken by each. In doing so, I'll explore some of
the language features of F# which make the embedding possible,
revisit some web abstractions such as Formlets, and talk about
some more recent abstractions such as Piglets (yes, Piglets).

26.11.2014 - Scalable Erlang and Functional Java 8

posted 16 Nov 2014, 14:13 by Ed Lambda   [ updated 18 Nov 2014, 02:19 ]

Two talks:

1. Kenneth MacKenzie.
Title: RELEASE: scaling to Erlang to 10,000 cores and beyond.

Erlang is a well-known concurrency-oriented functional programming
language which has been used to build large and highly-reliable
distributed software systems. However, some difficulties arise on
very large platforms; the RELEASE project aims to overcome these and
enable Erlang to scale smoothly to systems involving many thousands of
cores. I'll give an introduction to the basics of Erlang and then describe
some of the scalability challenges that arise on large hardware
systems, and how we're attempting to tackle them. No prior knowledge
of Erlang will be assumed!

2. Mike Borozdin
Title: Functional features in Java 8

Java 8 has many interesting new features. Undoubtedly, the most exciting one out of them is functional programming. In this talk, we will see practical examples of how functional programming features in Java 8 enable you to write code in a more concise and declarative manner. We will also cover the new functionality that makes it possible – Stream API, lambda expressions, default methods, and so on.

30.10.2014: Jeremy Singer "Optimizing non-Java JVM languages"

posted 3 Oct 2014, 09:25 by Ed Lambda

When: 30th October, 7pm @ The Outhouse pub
Title: Thinking outside the box: Optimizing non-Java JVM languages

Many languages target the Java virtual machine, from Ada to Xtend [1].
In this presentation, I will focus on functional languages like Scala
and Clojure. I am particularly concerned with the use of boxed value
types, which seems more prevalent on non-Java JVM languages. Custom
micro-benchmarks exhibit significant inefficiencies due to heavy use
of boxed integer types. I will describe the implementation of tagged
pointer optimisations in the OpenJDK interpreter [3] and demonstrate
how this improves performance for boxed integer allocation and method
invocation. However, with the exception of the Programming Language
Shootout benchmarks [4] I show there are currently few open source
Scala and Clojure applications that use boxed integers extensively.
This may change in future (discuss!)

[1]  ** market
opening - port a programming language beginning with 'Z' to the JVM,
see [2]

17.06.2014: Sam Lindley "Handlers in Action"

posted 17 Jun 2014, 03:24 by Ed Lambda

Sam Lindley is giving this month's EdLambda talk on Tuesday 17th at 7pm
at The Outhouse pub. It'll be based with Ohad Kammar and Nicolas Oury:
"Handlers in action". Sam will probably focus mostly on examples from
their Haskell effect handler library, perhaps with some live hacking.

Plotkin and Pretnar’s handlers for algebraic effects occupy a sweet spot
in the design space of abstractions for effectful computation. By
separating effect signatures from their implementation, algebraic
effects provide a high degree of modularity, allowing programmers to
express effectful programs independently of the concrete interpretation
of their effects. A handler is an interpretation of the effects of an
algebraic computation. The handler abstraction adapts well to multiple
settings: pure or impure, strict or lazy, static types or dynamic types.

This is a position paper whose main aim is to popularise the handler
abstraction. We give a gentle introduction to its use, a collection of
illustrative examples, and a straightforward operational semantics. We
describe our Haskell implementation of handlers in detail, outline the
ideas behind our OCaml, SML, and Racket implementations, and present
experimental results comparing handlers with existing code.

1-10 of 33