Skip to main content

Logo for BOB BOB 2020

28th February 2020

Berlin, Germany

Part of the BOB series
Lohmann & Birkner »

Tutorials A

Sessions in this room

  1. in Tutorials A

    Introduction to Idris (Stefan Wehr)

    Idris is a strongly typed functional programming language with dependent types. The language is inspired by Haskell with similar syntax and language features. Idris supports algebraic data types, pattern matching, control over side-effects, higher-order functions and type classes.

    But Idris also supports dependent types, meaning that terms can be used on the type-level. Thus, dependent types offer to possibility to use the rich term language to compute types, allowing programers to express many invariants on the type-level that would otherwise being checked at runtime (or not at all). A simple example of such an invariant is that an index accessing a specific element of an array must be within the bounds of the array. More complex properties are expressible as well, for example that a search tree fulfills the search tree property or that an SQL query is compatible with a certain database schema.

    The tutorial does not assume prior knowledge of Haskell. It assumes, however, good general programming skills and basic experience with functional programming.

    Takeaway bullet points
    • Learn the power of dependent types.
    • Learn the fundamental ideas of type-driven development.
    • Learn how to use types as a guideline for designing APIs.


    Please install the Idris compiler on your machine. The current version is 1.3.2. More information can be found on the Idris homepage:

    It is beneficial to install an editor plugin for Idris. There are (at least) plugins for Atom, Vim and Emacs.

    Please make sure your setup works before coming to the tutorial, otherwise we won't have enough time discussing the features of Idris. Please contact the instructor should you have problems with the installation or the setup.

  2. in Tutorials A

    Introduction to TLA+ (Annette Bieniusa)

    Concurrent and distributed programs are notoriously difficult to get right. Even tiny variations of algorithms like Peterson’s lock for mutual exclusion lead to significantly different behaviours and errors that are complex to locate.

    TLA+ is a high-level language for modelling such programs and specifying their behaviour in a rigorous way. In this tutorial, you will learn how to write concurrent and distributed algorithms in PlusCal, a pseudo-code like interface for TLA+, and how to specify correctness conditions using temporal logic. We will further apply the model-checker TLC and discuss typical pitfalls when working with TLA+.

  3. in Tutorials A

    Control Your Effects in Haskell (Mike Sperber)

    Functional programming is all about not using effects. Particularly in Haskell. Well, it turns out we sometimes do want to program with effects. When that happens, we keep them under control. With monads. Right? Unfortunately, monads compose quite poorly in Haskell, and when they do, using them is often awkward. The result is that much Haskell code takes a dive into the IO monad when really it should not. This tutorial is if you’re still willing to fight this disturbing trend.

    Strangely enough, with monads in Haskell past their 25th anniversary, this problem is only lately getting the attention it deserves. As a result, we have a handful of patterns and a quickly growing collection of effects libraries. Should you jump on one of those bandwagons or plod on with trusty old monad transformers? This tutorial will help you out!

  4. in Tutorials A

    ReasonML and React (Marco Emrich)

    Static type systems have arrived in the frontend! Typescript and Flow made them popular. ReasonML – the language by React Framework inventor Jordan Walke – goes one step further and brings a functional programming language from the ML family into the browser. ReasonML combines the semantics of OCaml with the common syntax of JavaScript.

    With the language comes a redefinition of the popular React-Framework: ReasonReact. ReasonReact finally realizes the original vision, its creator had for React - a fully functional driven frontend framework! The framework comes already equipped with hooks and reducers. It also provides a type safe way to build components in a JSX-like syntax - without the need to overspecify, thanks to Reason's excellent type inference.

    You will learn how to write Reason & ReasonReact code, which projects are worth using it and even when you should rather prefer alternatives like TypeScript or Elm.

    In this workshop we will

    • take a look at the concepts of the ReasonML-language
    • model data with the algebraic type system
    • build a simple frontend application in ReasonReact
    • write unit-tests with bs-jest