An in-depth look at quickcheck-state-machine

Wednesday, 23 January 2019, by Edsko de Vries.
Filed under coding.

Stateful APIs are everywhere: file systems, databases, widget libraries, the list goes on. Automated testing of such APIs requires generating sequences of API calls, and when we find a failing test, ideally shrinking such a sequence to a minimal test case. Neither the generation nor the shrinking of such sequences is trivial. After all, it is the very nature of stateful systems that later calls may depend on earlier calls: we can only add rows to a database table after we create it, we can only write to a file after we open it, etc. Such dependencies need to be tracked carefully. Moreover, in order to verify the responses we get back from the system, the test needs to maintain some kind of internal representation of what it thinks the internal state of the system is: when we read from a file, we need to know what was in the file in order to be able to verify if the response was correct or not.

In this blog post we will take an in-depth look at quickcheck-state-machine, a library for testing stateful code. Our running example will be the development of a simple mock file system that should behave identically to a real file system. Although simple, the example will be large enough to give us an opportunity to discuss how we can verify that our generator is producing all test cases we need, and how we can inspect whether the shrinker is doing a good job; in both cases, test case labelling will turn out to be essential. Throughout we will also discuss design patterns for quickcheck-state-machine tests which improve separation of concerns and reduce duplication. It should probably be pointed out that this is an opinionated piece: there are other ways to set things up than we present here.

(

Upcoming Haskell events: Haskell eXchange, Courses, MuniHac

Thursday, 04 October 2018, by Andres Löh.
Filed under community, training, well-typed.

Upcoming events

In the upcoming months, Well-Typed will be participating in a number of events that we would like to advertise here:

Well-Typed’s Guide to the Haskell Type System

London, 10 October 2018

On the day before the Haskell eXchange, Adam Gundry will teach a single-day compact course on Haskell type system extensions. Learn all about GADTs, data kinds, rank-n polymorphism, type families and more.

Registration is open.

Haskell eXchange 2018

London, 11–12 October 2018

The Haskell eXchange will return to London for the seventh time, with keynotes by Simon Peyton Jones, Stephanie Weirich, Niki Vazou and Simon Marlow, and more than 30 other talks on all topics Haskell. This year’s programme includes three talks by Well-Typed: Andres Löh on Deriving Via, Duncan Coutts on the Cardano Cryptocurrency, and David Eichmann on Geometry with Denotational Design.

Registration is open.

Well-Typed’s Guide to Performance and Optimisation

London, 15–16 October 2018

After the Haskell eXchange, Andres Löh will teach a two-day course on performance and optimisation. Learn about data structures, performance pitfalls, common optimisations that GHC applies, how to read GHC’s internal Core language, and more.

Registration is open.

MuniHac 2018

Unterföhring / Munich, 16–18 November 2018

After the successful MuniHac in 2016, we will have a second MuniHac in Munich this November! Join us for three days of conversations and hacking on Haskell libraries, applications and tools. Everyone is welcome, whether beginner or expert. There are some talks, including keynotes by Ben Gamari from Well-Typed, Matthew Pickering from the University of Bristol and Ryan Scott from Indiana University. Furthermore, there will be plenty of opportunity to learn and improve. You can work on your own project or join others in theirs.

Well-Typed is co-organising this event with TNG Technology Consulting. The event is free to attend, but the number of spaces is limited, so be sure to register early.

Registration is open.

Compositional zooming for StateT and ReaderT using lens

Tuesday, 04 September 2018, by Edsko de Vries.
Filed under coding.

Consider writing updates in a state monad where the state contains deeply nested structures. As our running example we will consider a state containing multiple “wallets”, where each wallet has multiple “accounts”, and each account has multiple “addresses”. Suppose we want to write an update that changes one of the fields in a particular address. If the address cannot be found, we want a precise error message that distinguishes between the address itself not being found, or one of its parents (the account, or the wallet) not being found. Without the help of suitable abstractions, we might end up writing something monstrous like:

setUsed :: AddrId -> Update UnknownAddr DB ()
setUsed addrId@(accId@(walletId, accIx), addrIx) = do
    db <- get
    -- find the wallet
    case Map.lookup walletId db of
      Nothing ->
        throwError $ UnknownAddrParent
                   $ UnknownAccParent
                   $ UnknownWalletId walletId
      Just wallet ->
        -- find the account
        case Map.lookup accIx wallet of
          Nothing ->
            throwError $ UnknownAddrParent
                       $ UnknownAccId accId
          Just acc ->
            -- find the address
            case Map.lookup addrIx acc of
              Nothing ->
                throwError $ UnknownAddrId addrId
              Just (addr, _isUsed) -> do
                let acc'    = Map.insert addrIx (addr, True) acc
                    wallet' = Map.insert accIx acc' wallet
                    db'     = Map.insert walletId wallet' db
                put db'

In the remainder of this blog post we will show how we can develop some composable abstractions that will allow us to rewrite this as

setUsed :: AddrId -> Update UnknownAddr DB ()
setUsed addrId =
    zoomAddress id addrId $
      modify $ \(addr, _isUsed) -> (addr, True)

for an appropriate definition of zoomAddress given later.

(

8-hours remote interactive course on
"Type-level programming with GHC"

Wednesday, 27 June 2018, by Andres Löh.
Filed under training, well-typed.

We are going to introduce new courses and online versions of our courses. As a first step, next month, we’re offering an online course on type-level programming with GHC which is now open for registrations:

Type-level programming with GHC

23-24 July 2018, 0800-1200 UTC

  • Delivered by Andres Löh
  • Two half days of lectures, discussions and live coding
  • Delivered online, probably via Google Hangouts
  • Up to 6 participants (first come, first served)
  • GBP 360 including VAT (GBP 300 without VAT)
  • Register by email to
(

Semi-Formal Development: The Cardano Wallet

Thursday, 31 May 2018, by Edsko de Vries.
Filed under coding.

TL;DR: A combination of formal modelling and testing using QuickCheck is a powerful tool in the design and implementation of high assurance software. Consistency of the model can be checked by testing invariants, and the real implementation can be tested by comparing it against the model.

As part of our consulting work for IOHK, Well-Typed have been working with IOHK on the design and implementation of the new version of the Cardano cryptocurrency wallet. As a crucial component of this process, we have written a semi-formal specification of the wallet: a mathematical model of the wallet along with invariants and lemmas about how it behaves.

We refer to this specification as “semi-formal” because while it states many of the wallet’s properties, and proves some of them, it by no means proves all of them. As we will see, however, we can use QuickCheck to test such properties, producing counter-examples where they fail to hold. Not only is this an invaluable tool during the development of the specification itself, it also gives us a very principled way of testing the real implementation, even if later we do prove all the remaining properties as well.

In this blog post we will take a look at the specification and see how it drives the design and testing of the new wallet. We will show parts of the formal development, but only to give some idea about what it looks like; we will not really discuss any of its details. The goal of this blog post is not to describe the mathematics but rather the approach and its advantages.

(

Objects with special collection routines in GHC's GC

Tuesday, 15 May 2018, by Ömer Sinan Ağacan.
Filed under coding.

A generational copying garbage collector, in its most basic form, is quite simple. However, as we’ll see, not all objects can be copied, and some objects require more bookkeeping by the RTS. In this post we’re going to look at these type of objects that require special treatment from the garbage collector (GC in short). For each type of object we’ll look at how they’re allocated and collected. Each of these objects solves a particular problem:

This post is mostly intended for GHC hackers, but may also be useful for Haskell developers who develop performance-critical systems and need to know about impacts of these objects to GC and allocation pauses.

(

Haskell development job with Well-Typed

Tuesday, 27 March 2018, by Andres Löh, Duncan Coutts, Adam Gundry.
Filed under well-typed.

tl;dr If you’d like a job with us, send your application as soon as possible.

We are looking for a Haskell expert to join our team at Well-Typed. This is a great opportunity for someone who is passionate about Haskell and who is keen to improve and promote Haskell in a professional context.

About Well-Typed

We are a team of top notch Haskell experts. Founded in 2008, we were the first company dedicated to promoting the mainstream commercial use of Haskell. To achieve this aim, we help companies that are using or moving to Haskell by providing a range of services including consulting, development, training, and support and improvement of the Haskell development tools. We work with a wide range of clients, from tiny startups to well-known multinationals. We have established a track record of technical excellence and satisfied customers.

Our company has a strong engineering culture. All our managers and decision makers are themselves Haskell developers. Most of us have an academic background and we are not afraid to apply proper computer science to customers’ problems, particularly the fruits of FP and PL research.

We are a self-funded company so we are not beholden to external investors and can concentrate on the interests of our clients, our staff and the Haskell community.

About the job

The role is not tied to a single specific project or task, and allows remote work.

In general, work for Well-Typed could cover any of the projects and activities that we are involved in as a company. The work may involve:

We try wherever possible to arrange tasks within our team to suit peoples’ preferences and to rotate to provide variety and interest.

Well-Typed has a variety of clients. For some we do proprietary Haskell development and consulting. For others, much of the work involves open-source development and cooperating with the rest of the Haskell community: the commercial, open-source and academic users.

Our ideal candidate has excellent knowledge of Haskell, whether from industry, academia or personal interest. Familiarity with other languages, low-level programming and good software engineering practices are also useful. Good organisation and ability to manage your own time and reliably meet deadlines is important. You should also have good communication skills.

You are likely to have a bachelor’s degree or higher in computer science or a related field, although this isn’t a requirement.

Further (optional) bonus skills:

Offer details

The offer is initially for one year full time, with the intention of a long term arrangement. Living in England is not required. We may be able to offer either employment or sub-contracting, depending on the jurisdiction in which you live.

If you are interested, please apply via Tell us why you are interested and why you would be a good fit for Well-Typed, and attach your CV. Please indicate how soon you might be able to start.

We are more than happy to answer informal enquiries. Contact Andres Löh (, kosmikus on freenode IRC) for further information.

We will consider applications as soon as we receive them. In any case, please try to get your application to us by 27 April 2018.

Object Oriented Programming in Haskell

Thursday, 08 March 2018, by Edsko de Vries.
Filed under coding.

In object oriented programming an object is a value with a well-defined interface. The internal state of the object is closed to the outside world (encapsulation), but the behaviour of an object can be modified by redefining one or more of the functions in the object’s interface, typically through subclasses (inheritance). The internal state of the object is open to, and can be extended by, such subclasses. This is known as the open/closed principle.

For some problem domains this way of modelling is extremely suitable, and so one may wonder if we can take a similar approach in a purely functional language like Haskell, without losing purity. An obvious choice is to model an object as a record of functions that correspond to the public interface to that object. For example, we might define the “interface” of counters as

data Counter = Counter {
      tick    :: Counter
    , display :: Int

and we can define a “constructor” for this class as

mkCounter :: Int -> Counter
mkCounter n = Counter {
      tick    = mkCounter (n + 1)
    , display = n

The problem with this approach is that it does not allow us to “redefine methods” in any meaningful way. In particular, suppose we tried to define a “subclass”1 of counters which doubles the count in the display method:

twice :: Int -> Counter
twice n = (mkCounter n) {
      display = n * 2

If we tried this

display (tick (tick (tick (twice 0))))

we will get 3, not 6. In this blog post we will explain what open recursion is, provide some runnable examples that you can evaluate one step at a time to develop a better intuition for how it works, and show how it can be used to solve the problem above. These results are not new, but we hope that this blog post can serve to make them a bit more accessible to a larger audience.

We then discuss how we can extend this approach using lenses to allow “inheritance” to also extend the “state” of the object.

(

Visualizing lazy evaluation

Monday, 18 September 2017, by Edsko de Vries.
Filed under coding.

Haskell and other call-by-need languages use lazy evaluation as their default evaluation strategy. For beginners and advanced programmers alike this can sometimes be confusing. At Well-Typed a core part of our business is teaching Haskell, which we do through public courses (such as the upcoming Skills Matter courses Fast Track to Haskell, Haskell Performance and Optimization and The Haskell Type System), private in-house courses targeted at specific client needs, and of course through writing blog posts.

In order to help us design these courses, we developed a tool called visualize-cbn. It is a simple interpreter for a mini Haskell-like language which outputs the state of the program at every step in a human readable format. It can also generate a HTML/JavaScript version with “Previous” and “Next” buttons to step through a program. We released the tool as open source to github and Hackage, in the hope that it will be useful to others.

The file in the repo explains how to run the tool. In this blog post we will illustrate how one might take advantage of it. We will revisit the infamous triple of functions foldr, foldl, foldl', and show how they behave. As a slightly more advanced example, we will also study the memory behaviour of mapM in the Maybe monad. Hopefully, this show-rather-than-tell blog post might help some people understand these functions better.

(

Binary instances for GADTs
(or: RTTI in Haskell)

Thursday, 15 June 2017, by Edsko de Vries.
Filed under coding.

In this blog post we consider the problem of defining Binary instances for GADTs such as

data Val :: * -> * where
  VI :: Int    -> Val Int
  VD :: Double -> Val Double

If you want to play along the full source code for the examples in this blog post can be found on github.

(

Previous entries