Producing formally verified software is expensive, as it is a time consuming, often tedious process, which requires expert skills not widely available. If we want to reduce these costs, we need to automate as much of the process as possible, and we need to make the technology more accessible to developers without specialised skills in verification. This talk explores some of the issues of verification, in particular in the context of file systems and presents a language based approach to systems code verification. Using a strict, purely functional language with linear types, and a verifying compiler results in a significant reduction of the costs involved.

Doctor Who: I think my idea’s better. Lester: What is your idea? Doctor Who: I don’t know yet. That’s the trouble with ideas: they only come a bit at a time.

(from “Revenge of the Cybermen” episode 3, by Gerry Davis)

Much of the perennial wrangling about types and type inference is predicated on the traditional man-proposes-God-disposes model of editor-compiler interaction.There often also lurks an assumption that the term language component of program texts should entirely determine what it is that programs do.Advocates of types often emphasize the bad behaviours types prevent, not any kind of goodness types sustain.This century, neither of these assumptions is necessary.I shall argue that, moreover, neither is helpful, and hence that we should stop rehashing last century’s battles on the internet.

The utopian position is to consider types as design statements, proposed in advance.The program text can be constructed by a joint effort of humans and machines.It should document the interesting parts of the explanation of what the program does, minimally the choices made by the humans which are not forced by the types.Types can describe a lot more that the machine representation of data: they can also characterize computational structure in ways which trigger code generation. Moreover, if we program in incremental interaction with a typechecker, we can work by stepwise refinement from specification to implementation.We are thus incentivized to write precise types. Of course, this position also makes the false assumption that we know what we are doing before we are doing it.

Looking to the future, I shall consider what programming language designers and programming tool developers might do to support ideas, even though the trouble is that they only come a bit at a time.

When dealing large data sets that do not fit in memory, it is crucial to limit the number of accesses and iterations over the data set. However, in a high level language it may not be immediately obvious how many iterations a particular program will require. The number of iterations becomes even less obvious in the presence of heuristic and statistics-based optimisations, as used by traditional databases: a small tweak to the query or even modifying the number of rows in a table can cause drastic changes to the query plan.

As data sets continue to grow, a high-level language with predictable runtime characteristics becomes more necessary. Programmers should not need to understand the internal workings of a database or query optimizer in order to write fast queries.

At Ambiata, we have designed and implemented Icicle, a query language specifically for single-pass queries. This means that any query in our language is assured to compile into a single iteration over the data set. We use a type system based on temporal logic to ensure that queries can be executed in a single pass without violating causality. Queries are then compiled to a stream-based intermediate language, which allows multiple queries to be merged together, removing duplicate computations. Finally, queries are compiled to high-performance C code.

In this talk, we will introduce Icicle and some example queries. We will show some example queries that would violate causality, and show how they are outlawed. We will then describe the intermediate language and the fusion system, showing how different queries over the same input data can be merged into a single pass. Finally, we show how using a carefully chosen, restricted intermediate language makes this fusion possible.

Vector / array functional programming languages have been around for a long time, beginning with the introduction of APL. Modern dialects of APL such as j, k, and q offer a radical paradigm of functional programming wherein arrays are at the forefront of computation, and through the use of specific higher-order functions known as ‘adverbs’, programmers can concisely express complex algorithms and programs without resorting to loops, and rarely resorting to explicit recursion.

This talk will provide an introduction to the paradigm of vector functional programming through the use of the q programming language, a very efficient, interpreted, dynamically-typed vector language from Kx Systems. After giving a brief history of vector languages, select syntax and semantics of the language will be introduced, emphasizing the terse notation as a facilitator of thought, as expressed in Iverson’s Turing Award paper 1. Through small examples of vector and atomic operations, to run-length encoding, key ideas such as verbs and adverbs, atomic vector operations, and array-based functional programming adhering to the “rule” of “no stinking loops” 2 will be demonstrated.

After an introduction to the language, an end-to-end example will be shown within a practical domain for vector functional programming: fast data analysis. The analysis will involve reading data from CSV files, scraping and processing data from the web, joining gathered data, and analysis — all using Q.

The attendee will leave the talk with a basic understanding of the vector functional paradigm, how it may be useful in practical domains, an understanding of array-based thinking (practical in any functional programming language), and hopefully, an appreciation — or at least openness — toward terse and precise syntax.

1 https://www.jsoftware.com/papers/tot.htm 2 https://nsl.com

At Atlassian, we are in the midst of rearchitecting our systems as microservices run in AWS to support the scale and flexibility we need. We have been building out a core identity component of our Cloud infrastructure in Scala, based on event sourcing and command-query responsibility separation (CQRS) in order to achieve this safely. With event sourcing, data is captured streams of immutable events to represent data instead of the traditional update-in-place paradigm. Streams can be easily replayed to restore system state up to any point in time to recover from bugs or failures. In combination with the CQRS pattern, we can seamlessly bring online new functionality requiring schema changes or new query patterns, and re-architect later for more scale simply by replaying and reinterpreting events into new microservices and ephemeral data stores. In this talk, we will describe the architecture of our system using AWS (DynamoDB, Kinesis and Lambda), design principles we’ve used, and most importantly technical and organisational lessons learned to help attendees avoid pitfalls we’ve come across.

Goals: By the end of the presentation, the audience should:

• have an understanding of event sourcing and CQRS including benefits and how it works
• have an understanding of design principles for event sourcing and CQRS, including event design, and surfacing eventual consistency through the application stack and in APIs.
• have an understanding of an architecture for an event sourced/CQRS-based application.
• have an appreciation of the challenges faced when building a system using techniques presented in the talk.

Transforming a large stream of data from one form into another. This seems like the ideal task for functional programming, a clear input, transform, output pipeline. However, things get very complex, very quickly. Once that stream of data is hundreds of terabytes a day, requiring co-ordination of hundreds of servers, with hundreds of software configurations, the functions transforming the data are the least of our problems. How can we use functional programming and the tools we are familiar with to get the same properties we value from our data transformation functions when writing code to manage our infrastructure and deployment?

This talk will step through the complexity of building and operating a large scale continuous deployment and co-ordination system; from server administration and change management through to wrangling Amazon Web Services. We will delve into the implementation of our production deployment system (in Haskell), looking specifically at its functional design: including a simple but effective purely functional DSL for describing deployment interactions; the techniques we utilize to ensure auditability and correctness; as well as the overall patterns we use in the end-to-end design of our daemon in order to keep this an easy to understand and maintain piece of software.

From this talk, the audience will take away a knowledge of how to apply many functional programming techniques together in an effective way to build robust commercial software. On their own these techniques appear simple, but the demonstration of them in a real production system will hopefully provide the context required for the audience to actually apply these techniques in their own code.

In this talk and subsequent jam, you’ll learn about the power of the Raft consensus protocol for replicating state over the network. Using examples in Clojure, you’ll see how to apply this in the context of a multi-user multi-instance application. You’ll see how this has future implications for the use of WebRTC.

Optics, such as lenses and prisms, are accessors / mutators for data structures, that can be elegantly composed to access / mutate positions deep within nested data structures. For some of our real world use cases we were unable to take full advantage of the composability of optics. In one case we could compose a sequence of optics to access a desired position in a data structure, but the same optic couldn’t mutate the position in the way we desired. We also found that composing a sequence of optics that each optionally access a position would obscure which optic in the sequence failed – which we needed to know in practice for error-reporting purposes. Consequently we were forced to “manually” compose optics for the desired behaviour, and the result was far less elegant or easily testable than composing sequences of optics. That is, until we wised up and designed our own composable, testable, optics that behaved the way we wanted.

This talk is a case study of how we improved the composability and testability of our components by designing optics with the behaviour we desired. We’ll walk through a simplified version of the problem we were trying to solve, the limitations we faced with vanilla optics, and how we solved the problem more elegantly by designing our own optics. The optics will be open sourced as a Scala library that complements the monocle library of optics by Julien Truffaut, et al.

Parsing is hard. It is the cause of hundreds of vulnerabilities, implementation mistakes and plain crashes in production. It got easier with techniques like parser combinators, but developers did not adopt them right away, especially in binary formats for low level contexts, like C development. Most solutions were deemed either slow or memory hungry, for right and wrong reasons.

The Rust language, developed by Mozilla, came with promises of safe, low level data manipulation, with efficient memory usage. The Nom parser combinators library was designed to check that assertion and verify that safe, zero copy, streaming parsers were a practical approach. Its development put light on an essential factor of adoption for parsing solutions: the usability and tooling are crucial.

This talk will cover the tricks provided by Rust to manage memory efficiently, its safety net for developers, and its ability to integrate with C code. Then we will approach the interaction between language theory and classical file format (best or worst) practices. I will also present the tools I wrote to make the programmer’s life easy during design, development, debugging and production.

Finch is an open source HTTP library built on top of Finagle, the RPC framework that powers Twitter’s infrastructure. Finch is a great candidate to use when building services, and compares favourably to other popular frameworks in languages such as Ruby, Go, JavaScript, Elixir, Clojure and Haskell. This talk outlines the types of problems faced when building small services, and how using a good type system can help. I introduce & outline Finch, highlighting how it addresses these concerns. Throughout, a concrete example of an API built for a startup using Finch is used.

Great you’ve written some elegant Haskell application using the latest in burrito and type system hackery. It all type checks and you adversary Senior QuickCheck can’t find any holes in your logic. Winning at life, now to push that into production and pat yourself on the back. Hold on, your beautiful Haskell code is behaving poorly, eating up all the memory and most of the CPU. That shouldn’t be, time to do a little investigation.

This talk will offer a practical look at Haskell performance, motivated by real life Haskell programs from Ambiata. We will look at things like strict and lazy data types, profiling tools and memory usage, and will offer up practical suggestions on making Haskell fast.

In the Haskell community there is a wealth of information around using types and general functional principles, much of the teaching material focuses on this which provides a solid foundation for using functional programming. However there is missing information around how to make Haskell code fast, or at least fast enough that it doesn’t matter.

We all know that functional programming makes for more testable, more reliable code. But even if we adopt insert your favourite functional language here on the server-side, and your choice of something sane that compiles to JavaScript on the client-side, the integration and testing story for a bog-standard full-stack CRUD app is, well, woeful. So OK, we’re all here at Lambda Jam patting ourselves on our puritanically stateless backs about how referentially transparent we are, but how does that help us if every time we have to put together something with a user interface we end up straight back in the spaghetti mess slowly losing our sanity to “undefined is not a function”?

For my side project, my language of choice for the server-side is Clojure, and my choice for the “something sane that compiles to JavaScript” is ClojureScript (with React for the web, and React Native for iOS and Android). Inspired by Kevin Lynagh’s keynote last year, I wrote a library to manage a UI’s behavioural state via composeable state machines: ‘bureaucracy’ (it makes the machines of state go round — ba-dom-ching!). Although it wasn’t my original goal, it turns out that by using bureacracy and by writing my UI in portable Clojure (that can run on the JVM as well as JavaScript), I can write more testable code: instead of nice functional unit tests, I write nice functional full-stack integration tests that exercise both the ClojureScript front-end code and the Clojure back-end code, without going anywhere near something so fundamentally un-FP as a Selenium test.

So I’m going to show you Get Fluent French, and break down how it’s built up out of genuinely functional pieces. And I’m going to show you how I write tests to mimic user interaction without opening a browser. And despite the fact that my user interface code runs on the JVM and in JavaScript, I’m going to do all of this without once misusing the term “isomorphic”.

Free monads, as used in the “Datatypes à la carte” pattern, are a useful way to structure code, separating of specification from implementation and enabling modularisation.

But they also come with a runtime performance penalty.

The complementary “typed tagless final interpreters” approach (popularised in the Haskell and OCaml worlds by Oleg Kiselyov) offers a performance boost over free monads, yet available sample code centers around simple expression langauges, and “real world” examples are hard to come by.

In this talk, we’ll compare and contrast the TTFI approach with Datatypes à la carte and explore how it can be used in real production code — with configuration, state, side effects and error handling.

So, you’ve written a DSL, it’s a work of art! It so perfectly models the problem at hand that even a trained house cat could generate business value. You just have one problem, your interpreter runs 100 times slower than a shell script launching JVMs in a loop.

Domain specific languages (DSLs) are able to offer the abstraction benefits of a high-level language, while when compiled, competing with low-level languages on performance. Because DSLs have a much smaller problem area, many specialised optimisations can be performed which are not feasible for a general purpose language.

In this talk, we will explain a number of optimisations which are useful for DSLs, and show our solutions to the practical issues we faced when implementing them in our query language, Icicle.

Icicle is a query language for processing large amounts of time-series data. Its type system enforces that queries require only a single pass over the data, and that multiple queries over the same data can be fused together. By using a combination of high level optimisations such as partial evaluation and common subexpression elimination, and low level optimisations such as parsing code which is specialised for the given input, our queries are faster than the equivalent hand-written C code.

From this talk, the audience will learn how the focused point of view that DSLs provide can be useful in performance critical systems, as well as a number of concrete techniques for optimising their own DSLs.

Target:

Anyone who is interested in domain specific languages (DSLs), embedded or external, and wants to know how to make them beat the pants off hand written C/C++.

The techniques presented are applicable to DSLs written in any language, although a familiarity with Haskell syntax would be a plus.

Functional programmers love to steal ideas from mathematics. Perhaps the best example of this is the venerable monoid, a concept from abstract algebra. But what about other algebraic structures? Semigroups and semilattices, related to monoids and beloved by mathematicians, are also ripe for use by programmers. We will explore these abstractions, their uses, and familiar concretions that fit. We’ll also look at the trade-off that helps us choose which is the right algebraic structure for the job.

Parsers and pretty printers are commonly defined as separate values, however, the same essential information about how the structured data is represented in a stream must exist in both values. This is therefore a violation of the DRY principle – usually quite an obvious one (a cursory glance at any corresponding FromJSON and ToJSON instances suffices to support this fact).Various methods of unifying parsers and printers have been proposed, most notably Invertible Syntax Descriptions due to Rendel and Ostermann (several Haskell implementations of this approach exist).

In this talk, attendees will learn an alternative approach to unified parsers and printers based on a familiar abstraction: prisms. We begin with an abstract parser definition based on the Cons type class (part of the lens library). The underlying prism gives rise to the functions uncons, whose type matches that of a “typical” functional parser, and cons, the dual (a printer!) From there we will examine how the fresnel library1 uses these building blocks to implement a combinator library for building parser/printer prisms out of existing prisms and isos.

We will see how fresnel has been applied in an ASN.1/DER library to correctly handle some of DER’s “special” encoding requirements. Finally, I will discuss some shortcomings of prism-based parser/printers, including the lack of useful error reporting.

1 https://github.com/frasertweedale/hs-fresnel

There are a lot of algorithms that revolve around iterating a form of information propagation until it attains a deterministic fixed point. CRDTs, Datalog, SAT solving, functional reactive programming, and constraint programming all fit into this mold.

One framework for these sorts of algorithms is the notion of a “propagator” due to Sussman and Radul, but until now little rigor has applied to know how such algorithms terminate with consistent results. Another framework is Lindsey Kuper’s work on the notion of “lattice variables” (LVars), which addresses termination, parallelism and eventual consistency well, but not iteration.

By blending these frameworks, I’ll build up a series of sufficient conditions for propagators to terminate with consistent results and proceed to show how we can use this common framework to steal insights and quirks from each individual domain to try to optimize the rest.

Languages in the ML family are great for writing domain-specific languages (DSL)s. We can use ideas from programming language theory (PLT) to make our DSLs more powerful, and we can use tools from the Haskell ecosystem to make our implementation easier to write, test, maintain and change.

This will be a lightning tour of how to build up a DSL that will get progressively more advanced throughout the talk. We’ll be exploring ways to keep the results testable (via QuickCheck) and composable along the way.

The first thing we’ll look at is operational semantics. We’ll specify the semantics of our DSL, implement the semantic rules in Haskell, and use that to derive an evaluator for our DSL. This in turns leads to a discussion of type systems. Some DSL programs can get stuck during evaluation, and type system can be used to check that a DSL program won’t get stuck.

Having both the semantic and type system specified also provides some opportunities for testing, and we can bias our implementation in order to do this in a way that will boost our confidence in the resulting DSL.

The next piece of the puzzle we will look at s parsing and pretty printing the DSL. Most importantly, we’ll cover the use of trifecta for parsing. This provides support for very good error messages, both in the parsing stage and in the type checking stage.

The last thing we’ll look at is lambda calculus, and how to embed lambda calculus into our DSL. This is a big step forward since it allows users of the DSL to abstract and reuse fragments of DSL programs. The implementation will be greatly assisted by the use of the bound library.

The remainder of the talk will be discussing various extensions and improvements that are either very useful or quite exciting.

The material will eventually appear in much more detail on https://dlaing.org. Most of the PLT material is covered in Pierce’s “Types and Programming Languages” and Harper’s “Practical Foundations of Programming Languages”.

This talk and (and subsequent Workshop / Jam) will introduce you to PureScript, a strongly-typed, Haskell-inspired programming language that compiles to JavaScript. The talk will provide a tour of the language and its ecosystem of tooling and libraries. You should leave both sessions with a grasp of PureScript fundamentals, and a self-sufficiency to tackle your own projects and experiments.

Talk Prerequisites: Basic programming experience; the talk is explicitly targeted at a range of experience levels. A familiarity with Haskell and JavaScript will help you understand more of the talk, but is not a strict requirement.

We’ll look at the remarkable technique of Church encoding, whereby any data structure or programming concept can be represented using nothing but the magic sauce of lambda functions! After the talk, you’ll know how to Church encode arbitrary structures yourself, and how it can actually yield huge performance gains, in particular when applied to free monads.

In the subsequent workshop, we’ll reinvent boolean and integer arithmetic, lists and free monads from scratch, Church encoding them in Haskell.