How hard can it be to spot missing or overlapping patterns in a Haskell function definition? Surely it’s the least we can expect from a decent compiler? But when you mix in GADTs, pattern guards, view patterns, data families, strict data constructors, and pattern synonyms, matters get surprisingly tricky.

In a 2015 paper “GADTs meet their match” they explored a nice, modular account of pattern-match checking that addresses many of these tricky points. Alas, GHC’s implementation of that paper has proved less than satisfactory: it can be terribly slow, and misses cases that programmers think look obvious. So Simon and colleague Sebastian Graf have been radically refactoring the implementation.

In this talk Simon will give lots of tricky examples of pattern matching, describe how to think about coverage and overlap checking, and reflect on how thier new refactored implementation works.

However, things could still be improved. Type-level programs are notoriously tricky to write, partly because the type language is first-order, meaning that our old friends like the maps and folds cannot be expressed.

In this talk, Csongor will walk through the type-level programming facilities of modern Haskell, and present a new GHC extension which enables higher-order type programming: UnsaturatedTypeFamilies.

This talk is based on the ICFP 2019 paper Higher-Order Type-Level Programming in Haskell and is aimed at people who are curious about how deep the rabbit hole goes if we do enable every possible language extension under the sun.

In this talk, Marco shows you what happens when you take things a little bit too far. You don't have to use every GHC feature under the sun. There's a lot you can do at the type level, but is it worth it? Where do you draw the line?

What has he learned? Stick to Simple Haskell!

In this talk, Artem will aim to help listeners build a basic understanding of linking by means of examples, give an overview of the GHC's linker code, and describe current challenges and possible improvements.

A level of familiarity with C and ASM is helpful, but not required.

This is a follow-up to some work Artem has done around RTS linker in GHC: https://gitlab.haskell.org/ghc/ghc/merge_requests/348/diffs

Related materials can also be found in this blog post

In this talk, Andrey will explore a general framework in which to understand and compare build systems, in a way that is both abstract (omitting incidental detail) and yet precise (implemented as Haskell code). He will use the framework to describe the essence of a variety of different real-life build systems, including Make, Shake, Bazel, Dune and Nix. The framework is open-source and available at github.com/snowleopard/build.

This talk is based on the ICFP 2018 paper with the same title that received the ICFP Distinguished Paper Award, and will also cover more recent work, including so-called selective functors. This talk is suitable for people comfortable with the notions of monads and applicative functors.

However, when most people first come into contact with lenses, they are anything but easy and smooth. To begin with, there are so many implementations. Van Laarhoven lenses, profunctor optics, and so on. And even if you figure out which one to use, you run into the next problem: Reading the API on hackage or loading the package up in your repl often just feels like having your face rammed into a wall of random letters.

This talk will provide, not a detailed guide to the inner workings of any particular implementation of lenses, but rather an overview of the broad ideas and motivating examples for them. What is the problem? And how does the framework of lenses give us a language to talk about that problem?

By the end of the talk, the ambition is that the listener will feel empowered to take another look at that lens library they've been meaning to, or even to give it a first try if they haven't before. If all goes well, you will agree that lenses aren't that scary after all!

Michał will present a tutorial on how to roll your own data ingestion pipeline in fifteen minutes. Then he will dive into a bit of methodology so that the thirsty has a map of materials to look further into.

Things become more complicated when you consider processes that can take a probabilistic amount of time or even fail with a certain probability. How do such processes compose sequentially or in parallel?

An example of this is sending a message in a network. Transmission time follows a (continuous) probability distribution, and it is even possible that the message will never reach its receiver.

In this presentation, Lars will extend the standard notion of probability monad to include a notion of probabilistic duration, which will enable you to model things like communication in a network of nodes. Lars will answer questions like: "How long will it take a signal to reach each node in the network?" and "How does the answer depend on network topology?"

All codebases of any non-trivial size should use guaranteed correct build systems that have a global view of the dependency graph across all languages, a global read/write build cache populated by continuous integration (CI) and developers' laptops, and feature instant rebuilds when switching between branches. The ideal CI setup rebuilds all commits no matter the size in mere minutes using multiple workers in parallel, runs only those tests that were touched by a code a change, and creates build artifacts that are downloaded upon initial checkout and initial build of the code.

In this talk, Mathieu will show how to achieve that for traditionally slow-to-build Haskell, using Cabal, Stack, Nix or Bazel, and also by gainfully combining all four.

Links:

• https://haskell.build
• https://github.com/Gabriel439/haskell-nix
• https://www.microsoft.com/en-us/research/uploads/prod/2018/03/build-systems-final.pdf

In this workshop participants will be able to learn the basics of Nix, and will go from turning a cabal based project into something that Nix can build and deploy. You will look at how the Nix provided docker tooling works and how you can create a minimal docker image of your Haskell service. You will also explore Nix based development workflows and what tools you can use for that.

Workshop requirement: A Linux or OSX Laptop with Nix installed.

It won't do much (something simple like the unix ls or sort commands) - but it will fit nicely into the rest of the Unix command line ecosystem, suitable for use by SSH or in your build system or wherever.

You'll have decent logging for debugging what's going on inside, you'll have some pretty console colours, You'll poke at the filesystem, you'll have beautiful command-line option handling (with perfect help text and magic-seeming tab completion) and you'll handle exceptions and errors nicely. By the end of this, everyone will think you're a greybeard unix tool writer from the 1970s... but really it will be some amazing Haskell tech inside.

In this entirely hands-on introductory level tutorial, participants will build a simple command line tool on their laptop, using common Haskell libraries and techniques. Participants won't need much Haskell experience at all.

Participants will require a laptop with stack installed, and connectivity to the Skills Matter wifi. Don't worry if you don't have Linux - you can do this on a Windows machine or Mac too.

A guide to installing the prerequisites can be found at github.com/benclifford/hx2019-prereq.

The interpreter is a full application, with a parser, type-checker, and evaluator. It serves both as an example of how to use these features and as an existence proof that Haskell is well-suited for fancy-typed programs.

Note: This talk was prepared as a talk, not a workshop. While I very much welcome questions as we go, there is not an explicitly interactive component.

The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by recursion. Dependently-typed programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program. This talk introduces Programming Language Foundations in Agda, a new textbook that is also an executable Agda script---and also explains the role Agda is playing in IOHK's new cryptocurrency.

The textbook can be found here.

This experience report presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of low-level control programs executed on custom hardware. You implement the semantics of a custom industrial instruction-set architecture in Haskell as an EDSL and perform symbolic execution of machine code programs to generate verification conditions which are later discharged with an SMT solver.

Using this methodology, you verify the functional correctness of programs and perform worst-case execution time analysis.

Among examples are both Kleisli categories and and the pure category -> where monadic actions come from the identity monad. This is important as it gives a way to instantiate an abstract description in a pure setting (e.g. for testing). Such categories admit a free model which allows to build abstract models, and he will present the free construction. Finally, he will present an example application in which a finite state machine will be represented using such a free category. This will give a type safe presentation of a state machine, where each state transition is guarded by the type system.

This talk will be based on his (on going) work on the free-category package published on Hackage. https://hackage.haskell.org/package/free-category

The talk will present:

• how to make simple tasks which are agnostic of where the data they should pull is located (and how it is serialized), and which can with a single function call expose all the configuration they accept to the outside world (CLI, config file...)
• how to join these tasks into a pipeline, and how porcupine helps with the re-usability of the tasks
• how the pipeline will expose to the outside world all the resources it will need and all the parameters it will accept at some point, so you can bind them each time to different sources and values, in order to run the pipeline in various contexts without having to change or rebuild the code
• why you should care at all about using arrows in that context, ie. what isn't supported right now by porcupine at the time of writing but would be enabled by this type of framework

(https://github.com/tweag/porcupine)

In this talk, you'll find more digestible and fun ways to approach category theory, explaining the buzzwords as we go. Irene will build from examples, give some motivation, and see where we end up!

If you want to find out what the "category" in "category theory" means, while not falling asleep, this is the talk for you!

Whilst this is somewhat true, laziness makes it very easy to introduce space leaks into a program and use more memory than necessary. Therefore it's important to understand the tools and techniques at our disposal for analysing and correcting memory usage.

In this talk, Matthew will explore different ways to analyse the memory usage of programs. Starting with the humble heap profiler, he'll look at its different modes of operation and how to interpret the heap profiles. He'll then discuss some more precise techniques to find space leaks and possible future directions for space profiling.

This talk explains how to fix all the pain, and make records a strength of Haskell, without making them harder to use. We show how to encode records and fields in a type class, then use existing Haskell machinery to abstract over multiple field names. This type class has been added to GHC, and is automatically generated for standard Haskell records. Building on that, we provide a convenient syntax through a Haskell preprocessor.

We’ve validated our design with the DAML programming language (based on the GHC compiler) which uses these records as standard. We’re happy to report that users experiences have been very positive.

Record syntax: https://github.com/ndmitchell/record-dot-preprocessor DAML programming language: https://daml.com/

Creation and maintenance gets easier when we can focus on:

• A small amount of game-specific differences when handling a specific game.
• The commonalities of all games when handling many or all games.

In the last two years, while creating mobile games in Haskell for Android and iOS at Keera Studios, Christina has used, improved and created structures and methodologies which help to focus on the given programming task at hand. In fact, the most important and effective part of her daily work of creating easy maintainable games is stepping back, 'cleaning' the code of our apps by introducing these structures and methodologies.

In this talk, Christina will use interactive examples to show the effects of frequent code 'cleaning', like:

• Simplification of the code.
• Minimization of app specific code through the use of existing and new libraries.
• Facilitation of bug hunting.
• Increase of comprehensibility, usability, reliability and persistence.
• Facilitation of participation.
By sharing these experiences, Christina wants to provide you with techniques that help to improve the maintainability of your work and she will hopefully can make it obvious that the short term tedious task of stepping back and 'cleaning' code is a very powerful tool to be more effective in the long term.

In this talk, you will see that, by using functional reactive programming to implement and structure programs and systems, the simplicity of testing pure functional code using principled techniques can be regained, opening up for powerful cross-platform testing frameworks unparallelled by their imperative counterparts. This approach enables property-based testing based on temporal logic, fully reproducible record-andreplay (even from deployed code), and hardware-in-the-loop testing. The talk will cover the necessary basics of functional reactive programming and illustrate using non-trivial case studies.

This talk is based on joint work by Dr Ivan Perez, Research Scientist at the NIA/NASA Formal Methods group and Founder of Keera Studios, and Dr Henrik Nilsson, School of Computer Science, University of Nottingham.

This talk presents a principled approach to specifying and implementing simple application-level communication protocols. It is a lightweight form of session types: by specifying protocols via state machines and encoding them into types we can guarantee the protocols are free from deadlock and that well-typed protocol implementations respect the protocol specification. A special feature of this approach is the support for protocol pipelining, which enables effective use of network bandwidth in the presence of latency.

The talk will also touch on practical aspects such as testing using simulation, and where this approach has been used in real applications.

In this talk, Tom will discuss the esoteric language of JavaScript and use Ramda.js to introduce its novel type system. While scary at first, he'll decipher cryptic functions like curry and compose with the surprising power of dependent type signatures.

In the end, Tom will guarantee that you'll be impressed at how far you can get with the Idris that you have today!

In this talk, Tom will show how he evolved an entity/controller system in Haskell, as a series of small progressions from simpler abstractions, and how Haskell's type system allows abstracting over types to provide a very clean user experience.

It turns out that this architecture is a great idea for Haskell too. It provides an easy to understand the pattern to organise the state in long-lived or complex Haskell applications.

The Elm Architecture replaces the threading of a state monad or a stack of monad transformers through the program with a single pure update function. Its event-based approach provides a simple way to handle concurrency, making things even more fun.

Attendees will come out knowing how to organise a multi-threaded Haskell application using the Elm Architecture. We will see how to perform non-blocking IO and how to continuously update our state with computations from multiple threads; all inside one simple pure function.

In this talk Csaba will share his vision of working in an environment that leaves nothing hidden under the hood, thereby giving the programmer full control over every aspect of compilation in a user-friendly way.

He tried Microsoft's Logo-like Steve-bot and whilst it was very easy to use, like any imperative approach, composition was difficult to achieve. However, using Haskell, functions, Monoids and a prudent use of lenses, a remarkably simple domain-specific language (DSL) can be built that achieves composition. With composition, it is possible to generate some very complex structures and Tim started with castles! This talk will briefly describe the DSL and generate some structures in-game with a live demo.

There are two different approaches for implementing a GRIN back end for a programming language. The first one is to use an intermediate language called Lambda, and the second one is to compile the front end language directly to GRIN. Both approaches will be briefly examined. The second part of the talk will focus on the details of the Idris-GRIN back end which consists of three main parts: an API for GRIN code generation, a program transformation selector, and the implementation of the primitive operations of Idris. The Idris-GRIN back end is mostly written in Haskell, the rest is implemented in C and LLVM-IR. The presentation is approachable by all audiences.

The powerful type system features, in particular, make it possible to maintain type information of the embedded language expression during the whole compilation phase. While maintaining the type information does not come for free, this extra effort is in our experience well worthwhile.

In this talk, Gabriele will use the in Haskell embedded language Accelerate as case study to show, among others, how to make many of the host language features, like pattern matching and variable binding, available in the embedded language without compromising efficiency.