Exploring Cloud Builds in Hadrian

Thursday, 01 August 2019, by David Eichmann.
Filed under ghc, well-typed.

GHC’s new build system, Hadrian, now supports a cloud build option: --share. With that enabled, build artifacts will be cached and shared between builds. This can improve build times, but getting this feature to function correctly is still a work in progress. This blog post explores the requirements for correctness, some examples in Hadrian, the current state of the project, and how developers can use cloud builds to improve iteration time.

(

Free training sessions at ZuriHac 2019

Friday, 07 June 2019, by christine, Adam Gundry, Duncan Coutts.
Filed under community, training, well-typed.

For the first time we will be providing free training sessions at ZuriHac. There will be two independent sessions, which will take place on Friday 14th June at 2–5pm and Saturday 15th June at 1.30–4pm, and are open to anyone who is registered for ZuriHac.

Adam Gundry: Advanced Types

Friday 14th June 2019, 2–5pm

On Friday afternoon Adam Gundry will lead the session on Advanced Types. This will assume familiarity with Haskell fundamentals such as defining your own data types and type classes. We will explore some more advanced extensions to the type system and techniques for dependently-typed programming in GHC Haskell, including:

Duncan Coutts: Evaluation and Performance

Saturday 15th June 2019, 1.30–4pm

On Saturday afternoon Duncan Coutts will lead the session on Evaluation and Performance. This is aimed at intermediate Haskell programmers who are comfortable understanding what their programs compute and are ready to move on to understanding how their programs compute. This is an important step towards being able to confidently write Haskell programs that will work within reasonable time and memory. Topics will include:

We would be delighted to welcome you at these sessions or to discuss any interesting topics with you at this fantastic Hackathon.

Other courses

If you cannot make it to ZuriHac but are still interested in our courses or other services, check our Training page, Services page, or just send us an email.

Integrated versus Manual Shrinking

Monday, 13 May 2019, by Edsko de Vries.
Filed under coding.

TL;DR: Even with integrated shrinking, you still have to think about shrinking. There is no free lunch. Also, important new Hedgehog release!

Property-based testing is an approach to software testing where instead of writing tests we generate tests, based on properties that the software should have. To make this work, we need to be able to generate test data and, when we find a counter example, we need to shrink that test data to attempt to construct a minimal test case.

In Haskell, the library QuickCheck has long been the library of choice for property based testing, but recently another library called Hedgehog has been gaining popularity. One of the key differences between these two libraries is that in QuickCheck one writes explicit generation and shrinking functions, whereas in Hedgehog shrinking is integrated in generation. In this blog post we will explain what that means by developing a mini-QuickCheck and mini-Hedgehog and compare the two. We will consider some examples where integrated shrinking gives us benefits over manual shrinking, but we we will also see that the belief that integrated shrinking basically means that we can forget about shrinking altogether is not justified. There is no such thing as a free shrinker.

(

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 info@well-typed.com
(

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 info@well-typed.com. 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 (andres@well-typed.com, 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.

Previous entries