Writing a High-Assurance Blockchain Implementation

Posted on November 2, 2017

In his blog post Cryptocurrencies need a safeguard to prevent another DAO disaster, Duncan Coutts discussed the need for high assurance development of cryptocurrencies and their underlying blockchain protocols. He also sketched one way in which one might go about this, but did not give much detail. In this follow-up blog post I delve into computer science theory a bit more, and in particular will take a closer look at process algebras. I will have no choice but omit a lot of detail still, but hopefully we can develop some intuition and provide a starting point for reading more.

Read more at iohk.io

(Video) Static Pointers, Closures and Polymorphism

Posted on October 12, 2017

A static pointer can be thought of as the address of symbol in a program. Their primary use lies in the fact that they can always be serialized and hence sent across a network; thus, while we cannot send a Haskell function over a network, we /can/ send a static pointer to that function. This makes them very useful in distributed frameworks such as Cloud Haskell (an library for Erlang-like distributed programs) and Sparkle (Haskell bindings to the Apache Spark cluster computing framework). In this talk, you will learn how static pointers work, what kind of infrastructure we can define on top to make working with static pointers more practical, and outline some use cases.

Watch the presentation at skillsmatter.com

Visualizing lazy evaluation

Posted on September 18, 2017

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. We therefore 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. In this blog post we will illustrate how one might take advantage of this tool. 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.

Read more at well-typed.com

Binary instances for GADTs (or: RTTI in Haskell)

Posted on June 15, 2017

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

Read more at well-typed.com

Linearity, Uniqueness, and Haskell

Posted on January 8, 2017

There is a group of people consisting of Tweag I/O, ghc head-quarters and JP Bernardy working on a proposal for adding linear types to Haskell. In this blog post I will attempt to put this proposal in some context. I will explain what linearity is and how it relates to its close cousin uniqueness typing, and I will compare the proposal to some other ways of doing things. My hope is that this will make the work more accessible.

Read more

Sharing, Memory Leaks, and Conduit and friends

Posted on September 29, 2016

TL;DR: Sharing conduit values leads to memory leaks. Make sure to disable the full laziness optimization in the module with your top-level calls to runConduit or ($$) (skip to the end of the conclusion for some details on how to do this). Similar considerations apply to other streaming libraries and indeed any Haskell code that uses lazy data structures to drive computation.

Read more at well-typed.com

Efficient Amortised and Real-Time Queues in Haskell

Posted on January 15, 2016

A queue is a datastructure that provides efficient—O(1)—operations to remove an element from the front of the queue and to insert an element at the rear of the queue. In this blog post we will discuss how we can take advantage of laziness to implement such queues in Haskell, both with amortised and with worst-case O(1) bounds.

The results in this blog post are not new, and can be found in Chris Okasaki’s book “Purely Functional Data Structures”. However, the implementation and presentation here is different from Okasaki’s. In particular, the technique we use for real-time datastructures is more explicit and should scale to datastructures other than queues more easily than Okasaki’s.

Read more at well-typed.com

Dependently typed servers in Servant

Posted on December 2, 2015

Suppose we have a webserver that can perform different kinds of operations on different kinds of values. Perhaps it can reverse or capitalize strings, and increment or negate integers. Moreover, it can echo back any value. However, it does not make sense to try to reverse an integer or increment a string.

This is an example of a dependently typed server: the value that we are given as input determines the type of the rest of the server. If we get a string as input, we expect a string operation as the second argument and the response is also a string; if we get an integer as input, we expect an integer operation as the second argument and the response is also an integer.

Read more at well-typed.com

Lightweight Checked Exceptions in Haskell

Posted on July 31, 2015

Consider this function from the http-conduit library:

-- | Download the specified URL (..)
-- This function will 'throwIO' an 'HttpException' for (..)
simpleHttp :: MonadIO m => String -> m ByteString

Notice that part of the semantics of this function—that it may throw an HttpException—is encoded in a comment, which the compiler cannot check. Wouldn’t it be much nicer if we could simply express in the type that simpleHttp may throw a HttpException? In this blog post I will propose a very lightweight scheme to do precisely that.

Read more at well-typed.com

Parametricity Tutorial

Posted on May 23, 2015

A powerful feature of Haskell’s type system is that we can deduce properties of functions by looking only at their type. For example, a function of type

f :: ∀a. a -> a can only be the identity function: since it must return something of type a, for any type a, the only thing it can do is return the argument of type a that it was given (or crash).

To reason about the properties of functions based only on their types we make use of the theory of parametricity, which tells how to derive a so-called “free theorem” from a type. This blog post is a tutorial on how to do this; it won’t explain why the theory works, only how it works. A Haskell practitioner’s guide to parametricity, if you will.

Part 1: Constant types, functions and polymorphism
Part 2: Type constructors and type classes

Qualified Goals in the Cabal Solver

Posted on March 27, 2015

When you ask cabal-install to install one or more packages, it needs to solve a constraint satisfaction problem: select a version for each of the packages you want to install, plus all their dependencies, such that all version constraints are satisfied. Those version constraints come both from the user (“please install lens version 4”) and from the packages themselves (“this package relies on mtl between version 2.1 and 2.2”). Internally cabal-install uses a modular constraint solver, written by Andres Löh. It was first presented at the Haskell Implementor’s Workshop in 2011, and is based on the paper Modular lazy search for Constraint Satisfaction Problems.

For the Industrial Haskell Group, Well-Typed has recently extended the constraint solver to deal with qualified goals. In this blog post we will explain how this constraint solver works by means of a running example, and look at how the new qualified goals change things.

Read more at well-typed.com

Comprehensive Haskell Sandboxes, Revisited

Posted on March 9, 2015 (last updated April 2, 2015)

For the last few years I’ve been using a system of symlinks as Haskell sandboxes. This worked well, but has one important drawback: symlinks are basically user-global state, and hence it is not possible to have multiple sandboxes active at the same time. However, as Haskell tools are getting better and better we can actually simplify the entire setup dramatically. Here’s a summary of my new approach:

Read more

Switching from Vim to Atom
(A Haskeller's Perspective)

Posted on March 7, 2015 (last updated Aug 23, 2016)

I have been a Vim user for many many years, but have long wanted to switch to an editor that was more easily hackable. I tried Emacs and Sublime, but both had various hurdles that were just too annoying for me and both times I switched back to vim very quickly. However, I started using Atom a while back, and I have to say, I liked it from the start. I very quickly felt almost as productive as I was in vim, and in some ways I already much prefer Atom. (And since it’s JavaScript, we can write plugins in Haskell!)

Below are some tips that helped me transition from Vim to Atom.

Read more

Writing Atom plugins in Haskell using ghcjs

Posted on February 14, 2015

Atom is an editor developed by the people behind GitHub. Written in JavaScript, it is expressly designed to be hackable, and hackable it is; I find writing Atom plugins a rather pleasant experience, even though this means writing CoffeeScript. Nonetheless, one of the things that initially attracted me to Atom is the existence of ghcjs, and hence the possibility of writing Atom plugins in Haskell. Why bother? Well, Haskell versus JavaScript, need I say more? Moreover, it means we can use almost any existing Haskell library in our Atom plugins; for instance, my Cabal extension calls into the Cabal library to parse .cabal files.

Read more

Monads: From Web 2.0 to Hardware Drivers

Posted on February 3, 2015

Monads are often considered to be a stumbling block for learning Haskell. Somehow they are thought of as scary and hard to understand. They are however nothing more than a design pattern, and a rather simple one at that. Monads give us a standardized way to glue a particular kind of computations together, passing the result of each computation to the next. As such they are useful well beyond functional programming.

Read more at well-typed.com

Core JavaScript Semantics

Posted on January 17, 2015

This post is a summary of the core JavaScript semantics, based on the papers The Essence of JavaScript and A Tested Semantics for Getters, Setters, and Eval in JavaScript from the semantics of JavaScript project at Brown University. Note that throughout this post “reference” has a very precise meaning as a pointer to a memory location; think ML-style references (or, if you must, C++-style references).

Read more

Simple SMT solver for use in an optimizing compiler

Posted on December 31, 2014

This is a second blog post in a series about engineering optimizing compilers; the previous was Quasi-quoting DSLs for free. In this blog we will see how we might write a very simple SMT solver that will allow us to write an optimization pass that can turn something like

if a == 0 then
  if !(a == 0) && b == 1 then
    write 1
    write 2
  write 3


if a == 0 then
  write 2
  write 3

without much effort at all. Read more at well-typed.com

Quasi-quoting DSLs for free

Posted on October 19, 2014

Suppose you are writing a compiler for some programming language or DSL. If you are doing source to source transformations in your compiler, perhaps as part of an optimization pass, you will need to construct and deconstruct bits of abstract syntax. It would be very convenient if we could write that abstract syntax using the syntax of your language. In this blog post we show how you can reuse your existing compiler infrastructure to make this possible by writing a quasi-quoter with support for metavariables. As we will see, a key insight is that we can reuse object variables as meta variables.

Read more at well-typed.com

Haskell CPP macros

Posted on September 13, 2014

Listing these here mostly because whenever I need to use them I seem to be unable to find them and have to dig for them in previous code I wrote.

Checking for minimal package versions

This relies on macros generated by Cabal. Example:

#if MIN_VERSION_process(1,2,0)
    -- something
    -- something else

Read more

Dealing with Asynchronous Exceptions during Resource Acquisition

Posted on August 28, 2014

Consider the following code: we open a socket, compute with it, and finally close the socket again. The computation happens inside an exception handler (try), so even when an exception happens we still close the socket:

example1 :: (Socket -> IO a) -> IO a 
example1 compute = do -- WRONG
  s <- openSocket 
  r <- try $ compute s
  closeSocket s
  case r of
    Left ex -> throwIO (ex :: SomeException)
    Right a -> return a

Although this code correctly deals with synchronous exceptions–exceptions that are the direct result of the execution of the program–it does not deal correctly with asynchronous exceptions–exceptions that are raised as the result of an external event, such as a signal from another thread.

Read more at well-typed.com

Debugging Haskell at assembly level
by scripting lldb in Python

Posted on August 1, 2014

Haskell programmers tend to spend far less time with debuggers than programmers in other languages. Partly this is because for pure code debuggers are of limited value anyway, and Haskell’s type system is so strong that a lot of bugs are caught at compile time rather than at runtime. Moreover, Haskell is a managed language – like Java, say – and errors are turned into exceptions. Unlike in unmanaged languages such as C “true” runtime errors such as segmentation faults almost never happen.

Read more at well-typed.com

Understanding the RealWorld

Posted on June 12, 2014

In my previous blog post Understanding the Stack I mentioned that “RealWorld tokens disappear” in the generated code. This is not entirely accurate. Simon Marlow gives a very brief explanation of this on the old glasgow-haskell-users mailing list. In this blog post we will explore this in more depth and hopefully come to a better understanding of the RealWorld, though perhaps not of the real world.

Read more at well-typed.com

Understanding the Stack

Posted on May 21, 2014

One of our clients sent us a bug report, which consisted of a 700 line Haskell program with a complaint that “it deadlocks”. After studying the code I concluded that, for the sake of the bug report, it could be summarized as

print a bunch of stuff, then crash with a stack overflow

So I wanted to replace the original code with code that did just that: print a bunch of stuff, then crash with a stack overflow. No big deal:

Read more at well-typed.com

Haskell (including GTK) on Mavericks

Posted on April 27, 2014

This post is out of date. See Comprehensive Haskell Sandboxes, Revisited instead.

Installing GTK

Although the GTK libraries can be installed through fink, macports, or brew, I’ve never had much luck with any of them. I recently tried installing them through brew and although they appeared to install ok, as soon as I tried to run a Haskell GTK application it segfaulted with a null pointer exception somewhere in libcairo. I therefore prefer to install from source. This is a fairly painless process; some hints are in my Comprehensive Haskell Sandboxes post. You can follow those instructions or just follow the instructions on the GTK+ website. The only important thing is that you need set set LDFLAGS so that it can find -lpython:

export LDFLAGS=-L/System/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/config

Read more

Pointwise Lenses

Posted on April 24, 2014

Lenses are a current hot topic in the Haskell community, with a bunch of packages providing implementations (data-accessor, fclabels, lens, amongst others). Although we will recall definitions, this post is not meant as an introduction to lenses. If you have not worked with lenses before, the talk from Simon Peyton Jones or the blog post by Sebastiaan Visser about fclabels are good starting points.

In this blog post we will propose a generalization to the lens representation used in fclabels and in many other packages (with various minor variations); we will consider the relation to the representation used in lens in a separate section.

Read more at well-typed.com

Performance profiling with ghc-events-analyze

Posted on February 12, 2014

ghc-events-analyze is a new simple Haskell profiling tool that uses GHC’s eventlog system. It helps with some profiling use cases that are not covered by the existing GHC profiling modes or tools. It has two major features:

Read more at well-typed.com

sendmail (postfix) on OSX

Posted on October 9, 2013

Scenario: you want to be able to run sendmail from the command line and have it deliver mail to mail servers other than localhost. It’s not particularly difficult once you know what to do but it was a bit of a pain to figure out. So, mostly for my own benefit:

  1. Fix configuration and permissions
  2. Set up SASL authentication for your favourite SMTP server
  3. Tell postfix which users are local (none)

(Video) Lazy I/O and Alternatives in Haskell

Posted on July 10, 2013

Haskell is one of the few programming languages that use lazy evaluation: computations get performed only when their result is demanded. It is however not so straightforward to combine lazy evaluation with side effects, such as reading from a file.

Lazy I/O is the standard solution to this in the current base libraries, but has its problems. We explain how lazy I/O works, what the problems are, and explore some of the solutions that are being proposed at the moment: iteratees, pipes, stream I/O, etc.

Watch the presentation at skillsmatter.com

The darker corners of throwTo

Posted on June 11, 2013

We will assume

import System.IO.Unsafe (unsafePerformIO, unsafeInterleaveIO)
import System.IO.Error (catchIOError)
import Control.Concurrent (throwTo, myThreadId, threadDelay)
import Control.Concurrent.Async (async, cancel, wait)
import qualified Control.Exception as Ex

in the remainder of this post.

Whatever work the target thread was doing when the exception was raised is not lost: the computation is suspended until required by another thread.

We can observe this directly when using unsafePerformIO :

Read more

Brief Intro to Quasi-Quotation (Show me the types already)

Posted on May 9, 2013

This posts serves as a brief introduction to quasi-quotation in Haskell, because I couldn’t make much sense of the existing documentation, which gets bogged down in unnecessary details about writing parsers, the use of SYB, etc. Also, although quasi-quotation borrows syntax from Template Haskell, the TH expression [|e|] and the QQ [qq|e|] are false friends at best.

Read more

Comprehensive Haskell Sandboxes

Posted on February 10, 2013

For an alternative approach, see Comprehensive Haskell Sandboxes, Revisited instead.

Serious Haskell developers will want to test their packages against different versions of ghc, different versions of libraries, etc. It is therefore useful to have multiple Hackage development environments, or sandboxes. A comprensive sandbox contains:

Moreover, good sandboxes are

  1. isolated from each other: only the active sandbox can be modified
  2. relocatable: it should be possible to copy the sandbox ~/env/ghc762 to ~/env/client1 to use as the basis for a new sandbox, or to copy the entire set of sandboxes (~/env) from one machine to another (suitably similar) machine (this means that paths in config files or baked into executables should never mention the name of the sandbox)
  3. self-contained: there should be no need for a system wide install of ghc
  4. transparent: we should be able to use the standard tools (ghc, cabal) as they are

There are existing tools for Haskell sandboxes (such as cabal-dev or hsenv), but none satisfy all of the above requirements (to the best of my knowledge). However, it is easy enough to set up our own.

Read more

Performance problems with -threaded?

Posted on February 6, 2013

Consider the following two implementations of a very simple ping/pong server and client, one written in C and one written in Haskell:

Neither of them has been particularly optimized, that’s not the point of this post. The point of this post will become evident when we measure the latency for the following three programs:

  1. The C program compiled with -O2
  2. The Haskell program compiled with -O2
  3. The Haskell program compiled with -O2 and -threaded

Read more

ThreadScope 0.2.2 binary for Mac OS X 10.8.2

Posted on January 24, 2013

This is an application bundle which should hopefully Just Work without any additional libraries (in particular, you should not have to install any GTK libraries).


Communication Patterns in Cloud Haskell (Part 4)

Posted on October 15, 2012


In Part 3 of this series we showed how to write a simple distributed implementation of Map-Reduce using Cloud Haskell. In this final part of the series we will explain the K-Means algorithm and show how it can be implemented in terms of Map-Reduce.

K-Means is an algorithm to partition a set of points into n clusters. The algorithm iterates the following two steps for a fixed number of times (or until convergence):

Read more at well-typed.com

Communication Patterns in Cloud Haskell (Part 3)

Posted on October 12, 2012


In Part 1 and Part 2 of this series we described a number of ways in which we might compute the number of prime factors of a set of numbers in a distributed manner. Abstractly, these examples can be described as

a problem (computing the number of prime factors of 100 natural numbers) is split into subproblems (factorizing each number), those subproblems are solved by slave nodes, and the partial results are then combined (summing the number of factors)

Read more at well-typed.com

Communication Patterns in Cloud Haskell (Part 2)

Posted on October 8, 2012


In Part 1 of this series we introduced a number of basic Cloud Haskell communication patterns. All these patterns will work fine for modest numbers of work items; in this blog post we’re going to look at the performance and memory use for much larger numbers of work items, so we can see how each pattern scales up. We will see that scalability improves as we move from master-slave to work-pushing to work-stealing, and that many further improvements can still be made. More importantly, we hope to help you to predict runtime behaviour from your code, so that you can write more scalable and high-performance code.

Read more at well-typed.com

Communication Patterns in Cloud Haskell (Part 1)

Posted on October 5, 2012

Master-Slave, Work-Stealing and Work-Pushing

In this series (2, 3, 4) of blog posts we will describe a number of basic communication patterns in Cloud Haskell. We don’t assume much familiarity with Cloud Haskell, but it will probably be useful to be familiar with the basics; Towards Haskell in the Cloud (Epstein, Black and Peyton Jones, Haskell Symposium 2011) is a good starting point. We will start simple but we will finish with some more advanced techniques.

Read more at well-typed.com

Memory Layout for Multiple and Virtual Inheritance

Posted on January 1, 2006

In this article we explain the object layout implemented by gcc for multiple and virtual inheritance. Although in an ideal world C++ programmers should not need to know these details of the compiler internals, unfortunately the way multiple (and especially virtual) inheritance is implemented has various non-obvious consequences for writing C++ code (in particular, for downcasting pointers, using pointers to pointers, and the invocation order of constructors for virtual bases). If you understand how multiple inheritance is implemented, you will be able anticipate these consequences and deal with them in your code. Also, it is useful to understand the cost of using virtual inheritance if you care about efficiency. Finally, it is interesting :-)

Read more at phpcompiler.org

DLX/MIPS tutorial

Posted on May 19, 2005

This is a tutorial about the MIPS microprocessor, that I wrote for Prof Jeremy Jones at Trinity College, Dublin. The original tutorial can be found on his website, and if you are running Windows I recommend you go there instead because all the examples are in fact interactive. Unfortunately this does not work on Linux or OSX, however, so I’ve mirrored the tutorial here and created YouTube videos for all the examples.

Read more