Skip to main content
BOB 2019

Logo of BOB 2019 BOB 2019

22nd March 2019

Berlin, Germany

Part of the BOB series
Lohmann & Birkner »

Talks #1

Sessions in this room

  1. in Talks #1

    Applicative DSLs

    Monadic DSLs are ubiquitous in functional programming: Parser combinators, build systems, test data generators (like QuickCheck’s Gen) are usually monadic, and »Free Monad + Interpreter« is a well-known pattern for building DSLs. Monads allow a great deal of flexibility for DSL embedding, and come with a rich interface of generic combinators. In comparison, Applicatives seem quite restricted at first glance. On the other hand however, Applicatives compose and parallelize easily, and provide several additional benefits, as we will see. Are these worth the restrictions?

    In this talk, we are going to explore libraries like optparse-applicative that use an applicative DSL for extra benefit, and show the design of an applicative DSL by the example of an Applicative test data generator library.

  2. in Talks #1

    Inspection Testing

    A Promise Checked is a Promise Kept

    Some high-quality Haskell libraries, including old friends like text and new kids on the block like generic-lens, promise that the abstractions provided by these libraries are actually free and will be completely dissolved by the compiler. In the case of text the promise is that certain pipelines of text-processing functions will be optimizes (“fused”) to never allocate a full text value; generic-lens promises that its generically derived lenses are, after optimization, identical to handwritten ones.

    But, in practice, these promises often don’t hold. They held at some point in the past, when the author checked them manually, but later versions regressed.

    This problem can be fixed with inspection-testing, a Haskell library and plugin to the compiler that allows you to explicitly state what you expect from the compilers optimizations, and have the compiler check that it actually happens. This can be used by library authors to test their promises, but also by users to learn more about what the compiler does with their code.

    In this talk, you will discover the tale of broken promises in commonly used Haskell libraries, and you will learn how these promises can be checked automatically using inspection-testing.

  3. in Talks #1

    Across Time and Space: Building Explorative UIs Using a Many-Worlds Interpretation of State

    The functional approach to state management in the frontend was first enabled by React, pioneered by the likes of, Redux, and Elm, and has ushered in a golden era in web development. It is captured by the two signatures view :: DB -> HTML and mutate :: DB -> Tx -> DB. What might happen when we start working with more than one world, i.e. when we replace the notion of mutate with that of solve :: DB -> Tx -> [DB]? Using Clojure and Rust, we explore these ideas in the context of 3DF, a stream processing system based on differential dataflows.

  4. in Talks #1

    Logic in the Service of System Configurations

    Programming is glamorous; everyone has ideas for how it should be done better. System configuration, in contrast, lacks panache; it seems to consist mainly of fiddling with lots of little settings across devices. However, configuration actually performs a very difficult task: the devices are heterogenous, they work at different levels of abstraction (databases, servers, networks), and they form a distributed system that must act in concert to achieve a subtle (often unstated) goal. Indeed, many security and correctness problems stem not from incorrect programs (for which people constantly produce new verifiers) but rather from subtle configuration errors.

    There are several modalities of action: e.g., verification (given a configuration and a property, does the configuration match the property?); differential analysis (given two configurations, how are they different?); and synthesis (given a specification, can we generate a configuration?). All these can be unified under the rubric of mathematical logic. We will see how the tools of logic can address several of these problems in a somewhat uniform way.

    The talk will be self-contained, but does expect that the listener has a basic knowledge of logic (namely that the upside-down A is for-all and the backward E is there-exists).

  5. in Talks #1

    Designing Applications with Pluggable Layers Using Polymorphism

    The flagship product of IOHK is Cardano, the Proof-of-Stake (PoS) blockchain hosting the cryptocurrency Ada. Conceptually, the system can be divided into a stack of layers: the networking layer that distributes messages across the nodes, a cryptographic layer to handle signatures, a ledger layer that keeps track of funds and transactions, and in between, orchestrating everything, the consensus layer that implements the PoS protocol and determines how the nodes agree on a sequence of blocks.

    All of those layers are the subject of ongoing research and improvement, and we want to retain the ability to replace an individual layer, with minimal changes required on the rest of the system. In order to do that, we keep the consensus layer polymorphic in the types of the other layers. Replacing a layer then amounts to choosing another concrete instantiation.

    We show how to use Haskell’s type system to design such a polymorphic consensus layer. Features we use for that are Type Classes, Type Families, Phantom Types, and others.

  6. in Talks #1

    Wire Once, Rewire Twice

    At Symbiont, we use a “modules-as-records-of-functions” to structure our services and share code. We need the ability to create components which can easily be wired together but also changed at will for unit or integration testing even if they are very far down in the dependency tree.

    This talk will show how we approached this problem, started solving it with 2 simple type classes but then came up with a much more simple way, relying on just one data structure!

    Not only this makes reconfiguring applications a breeze but the same technique can be applied to Hedgehog generators where you can define a “compositional language” to modify existing generators for nested data structures. You can now express things like “generate a model of shoe with only the colour blue and 2 sizes

  7. in Talks #1

    State machine modelling and property based testing combined with fault injection

    Property based tests of pure programs can give us great confidence that the involved functions are correct with regard to some specification. When the programs are monadic however, i.e. use the file system or the network for example, we need to be more careful because of exceptions.

    For example some file that the program uses might have the wrong permissions or some network traffic gets lost, causing our program to crash or lose data. The problem here is that typically when we run our tests none of these exceptions occur and the tests pass. Even a conscious effort to test for exceptions might be futile, because of the sheer amount of things that can possibly go wrong in a program (nevermind combinations of failures and dependencies on timing).

    In this talk I’ll show how we can overcome these testing difficulties by using state machine modelling and property based testing together with fault injection. Fault injection is a technique that purposely introduces faults into our system, for example network package loss.

    I gave a talk last year on combining property based testing and state machine specifications to test concurrent programs. In this years talk we’ll recall the basics and focus on exceptions rather than on concurrency, but of course nothing stops us from doing both.