In our Developer Deep Dive series of occasional technical blogs, we invite IOHK’s researchers and engineers to discuss their latest work and insights.

Marlowe is a domain-specific language for secure financial smart contracts that is being developed by IOHK for the Goguen capabilities of the Cardano blockchain. Following my introductory post on Marlowe, in this Deep Dive post, we'll look at the details of the language, and the various ways of writing Marlowe smart contracts as we move into the era of decentralized finance (DeFi). After explaining our approach to oracles, which import ‘real world’ information into a running contract, we look at the Algorithmic Contract Types Unified Standard (Actus) for financial contracts, and explain how we have implemented this innovation in Marlowe.

Marlowe in a nutshell

Marlowe is a small language, with a handful of constructs that, for each contract, describe behavior involving a fixed, finite set of roles.

• A running contract can make a payment to a role or to a public key.
• In a complementary way, a contract can wait for an action by one of the roles, such as a deposit of currency, or a choice from a set of options. Crucially, a contract cannot wait indefinitely: if no action has been initiated by a given time (the timeout), then the contract will continue with another behavior, such as refunding any funds in the contract.
• Depending on the current state of a contract, it may make a choice between two future courses of action, which are themselves contracts.
• When no more actions are required, the contract will close, and any remaining currency in the contract will be refunded.

When a contract is run, the roles it involves are fulfilled by participants, which are identities on the blockchain. This model allows a role to be transferred during contract execution, so that roles in a running contract can be traded. Each role is represented by a token on the chain, and transferring this transfers the ability to perform the role’s actions. Taking this further, we can represent a single role with multiple tokens, thus allowing the role to be shared: this could be termed being ‘securitized’.

The Marlowe system

We deliberately chose to make the language as simple as we can, so that it is straightforward to implement on Cardano and in the Marlowe Playground. Marlowe describes the flow of cryptocurrencies between participants, and for this to be implemented in practice on the Cardano blockchain, code has to be executed both on-chain and off-chain: remember, though, that just one Marlowe contract describes both parts. The on-chain part accepts and validates transactions that conform to the requirements of the smart contract: this part is implemented as a single Plutus script for all Marlowe contracts, with the particular Marlowe contract comprising a datum passed through the transactions. Off-chain, the Marlowe contract will be presented via the user interface and wallet, offering or, indeed, automating deposits and choices and receiving cryptocurrency payments.

Figure 1. Marlowe Playground simulates the ways that contracts behave

In the Playground we’re able to simulate contract behavior, so that potential users can walk through different ways that contracts will evolve, according to different actions taken by the participants. In the main simulation, Figure 1, users have an omniscient point of view and are able to perform actions by any participant, with the option at each point to undo the actions taken, and then to take a different path. The wallet simulation allows users to see behavior from one particular participant’s perspective, thus simulating how that user will interact with the running contract once it is deployed on the blockchain.

This simplicity also makes it possible for us to model Marlowe contracts in an SMT solver, a logic system for automatically checking the properties of systems. Using this model, which we call static analysis, for each contract we are able to check whether or not it might fail to fulfil a payment, and if the contract can fail we get evidence of how it fails, helping the author to rewrite the contract if they wish.

We can build a formal model of our implementation in a proof assistant, in which we are able to produce machine-checked proofs of how the language behaves. While the SMT solver works for individual contracts, the proof assistant can prove properties of contract templates, as well as the system itself: for instance, we can show that in any running contract, the accounts it references can never be in debit. Simulation, static analysis, and proof provide complementary levels of assurance for a contract to which users will be committing assets to ensure that the contract behaves as it should.

Writing Marlowe contracts

We have seen how Marlowe contracts can be analysed in various ways, but how do authors actually write smart contracts in Marlowe? The Playground provides several ways of producing Marlowe contracts. Users can write Marlowe directly, but beginners often choose to build contracts visually, using an interactive Blockly editor. Figure 2 shows a section of an escrow contract.

Figure 2. An escrow contract in Playground’s interactive Blockly editor

Working in this visual editor has the advantage of showing all the options as you select how to fill in a part of the contract that is being developed. Alternatively, you can develop contracts in Haskell, because the Marlowe DSL is in fact embedded in Haskell. Figure 3 shows the same contract in Haskell: the blue and purple parts are Marlowe, and the black components are defined in Haskell, as abbreviations that make the overall contract more readable. This approach allows users to build up a smart contract step by step from components. In the code shown in Figure 3, the roles, Alice and Bob, are each asked to make a choice: if their choices match, they agree, and the contract proceeds one way; if not, then a third participant, Carol, is asked to arbitrate between them. The contracts agreement and arbitrate are defined later in the Haskell file.

Figure 3. The escrow contract in Haskell

Users will also be able to write their financial smart contracts using JavaScript, while still enjoying all the advantages of analysis, simulation, and proof, as provided by the Marlowe implementation.

Oracles

One of the first questions we get asked when we describe Marlowe is about financial oracles, or how we can get a contract to take account of external data values, such as the exchange rate between ada and bitcoin. Abstractly, an oracle is just like a participant that makes a choice, and so the semantics of Marlowe can already deal with external values. However, we plan to support oracle values as part of the implementation, allowing contracts to access values directly from a stock market ticker or a data feed such as Coinbase. At the same time, the Plutus team is researching the best way to deal with oracles in general, and we can expect support for that in due course, though maybe not in the first full release of Marlowe and the Plutus Application Framework.

Actus for financial contracts

Marlowe has the potential to give people the chance to make financial commitments and trades without a third party facilitating it: the blockchain ensures that the contract is followed.

We are building a Marlowe implementation of disintermediated contracts to offer to end users who want to make peer-to-peer financial deals directly without the intervention of any third parties.

The Actus Financial Research Foundation categorizes financial contracts by means of a taxonomy that is described in a detailed technical specification.

Actus builds on the understanding that financial contracts are legal agreements between two (or more) counterparties on the exchange of future cash flows. Historically, such legal agreements are described in natural language, leading to ambiguity and artificial diversity. As a response, Actus defines contracts by means of a set of contractual terms and deterministic functions mapping these terms to future payment obligations. Thereby, it is possible to describe most financial instruments through 31 contract types or modular templates.

Next, we look at a simple example, and then we explain our full approach to implementing Actus, with complementary approaches providing different pros and cons.

A first Actus example

A zero-coupon bond is a debt security that does not pay interest (a coupon) but is issued at a discount, rendering profit at maturity when the bond is redeemed for its full face value.

For example, Figure 4 describes a contract whereby an investor can buy a bond that costs 1,000 lovelaces with 15% discount. She pays 850 lovelaces to the bond issuer before the start time, here slot 10.

Later, after maturity date, slot 20 here, the investor can exchange the bond for its full notional value, ie, 1,000 lovelaces.

Figure 4. Contract for a zero-coupon bond with a 15% discount

This contract has a significant drawback. Once the investor has deposited the 850 lovelaces, it will be immediately paid to the issuer; if the investor does not invest quickly enough, ie before the timeout, the contract ends. After that, two outcomes are possible:

• the issuer deposits 1,000 lovelaces in the investor's account, and that sum is immediately paid to the investor in full;
• if the investor doesn’t make the deposit, then the contract is closed and all the money in the contract is refunded, but there is no money in the contract at this point, so the investor loses her money.

How can we avoid this problem of the bond issuer defaulting? There are at least two ways to solve this: we could ask the issuer to deposit the full amount before the contract begins, but that would defeat the object of issuing the bond in the first place. More realistically, we could ask a third party to be a guarantor of the deal, as expressed here.

Figure 5. Improved contract with a guarantor

Actus in Marlowe

Products in the Actus taxonomy, such as the principal at maturity contract, can be presented in different ways in Marlowe, according to the degree to which they can accept changes to their terms during the contract lifetime (Figure 6).

Figure 6. Actus taxonomy and Marlowe

In the simplest case, all cash flows are set, or frozen, at contract initiation, so that it is entirely predictable how the contract will operate, assuming that all participants continue to engage with the contract during its lifetime. Contracts of this kind we call Actus-F (for fixed or frozen).

Dynamism – that is change during contract evolution – can happen in two ways. Participants can make unscheduled payments that require re-calculation of the remaining cash flows, and also the cash flows can be modified by taking into account external risk factors. The full generality of contracts that do both are modelled in Actus-M (for Marlowe).

There are intermediate levels too: Actus-FS models fixed schedules: allowing risk factors to be taken into account, but with no unexpected payments; conversely, Actus-FR contracts allow payments to be made at unexpected points, but do not take into account any risk factors.

Finally, moving outside Marlowe, Actus-H (H for Haskell) models the contracts directly as programs in Plutus or Haskell, using Marlowe for validation of each transaction in the contract lifetime by generating Plutus code from the Marlowe description of the contract logic.

Why do we offer these different models of Actus contracts? The reason is that there is a trade-off between the dynamic nature of contracts and the assurance we can give to users about how the contracts will perform in advance of contract execution.

• Actus-F contracts present an entirely fixed schedule of payments, which can be scrutinized directly by the participants so that it is straightforward to see, for example, that all payments from such a contract will succeed.
• Actus-FS and -FR contracts present more dynamism, but the contracts are readable and easy to scrutinize. Moreover, they are subject to (slower) static analysis to establish, for example, that all payments will succeed.
• Actus-M contracts are expressed in Marlowe, and so can be analysed. Analysis is, however, substantially slower because of the unpredictability of the actions that the contract will undergo at any particular point in time. Note that assurance can be offered for scaled-down versions of contracts, which have the same computational content, but which evolve over a shorter time, thus involving fewer interactions.
• Actus-H contracts are written in a combination of Plutus and Marlowe, and so are not amenable to static checking in the same way as the others. However, this platform offers corporate clients full extensibility and tailoring of the implementation of the Actus standard.

In our implementation of Actus, available as a pre-release version in the Labs tab of the Playground, users are able to generate Actus-F and -FS contracts from the terms of the contract, using a visual presentation of the data required.

Figure 7. The three items with asterisks are required for a principal at maturity contract

For a principal at maturity contract, three items are required: the start and end date, and the notional amount of the contract (hence the items being starred in the template). Such a contract will comprise a simple load, in which the notional amount is transferred from the counterparty to the party at the start of the contract, and in the reverse direction at the maturity date.

Adding additional items will change the generated contract accordingly. In Figure 7, the party will have to transfer the notional plus the premium to the counterparty at maturity date, hence giving the counterparty an incentive to make the loan in the first place.

Moving into a DeFi world with smart contracts

As we have seen, finance professionals and developers now have a way to start creating financial smart contracts directly in Haskell or pure Marlowe, or visually, using the Marlowe Playground, depending on their programming expertise. In the Playground, you can simulate and analyse the contracts you create to test that they work properly and are ready to be issued into the world of decentralized finance when the Goguen stage of Cardano is implemented. IOHK’s Marlowe team will continue implementing examples from the Actus standard, as we prepare to finalize the implementation of Marlowe on Cardano, and bring financial smart contracts to the blockchain itself.

In this post, we introduce Marlowe, a new language for financial contracts, and describe the benefits of it being a domain-specific language (DSL). As a DSL it describes only financial contracts, rather than smart contracts in general. Because of this, it differs from general-purpose blockchain languages like Solidity and Bitcoin Script.

Marlowe is industry-scale. We have built Marlowe contracts based on examples from one of the leading projects for financial smart contracts, the Algorithmic Contract Types Unified Standards (Actus) system. Currently, these and other examples can be seen in the Marlowe Playground, a browser-based environment in which users can create, edit, simulate, and analyse Marlowe contracts, without having to install or pay for anything.

Who can use Marlowe? Marlowe is a platform for decentralized finance (DeFi) that supports direct, peer-to-peer lending, contracts for difference (CFD), and other similar instruments. Financial institutions can use it to develop and deploy custom instruments for their customers and clients, for example.

As a part of the Goguen rollout, we will be completing the implementation of Marlowe on Cardano, giving users and organisations the opportunity to execute DeFi contracts they have written themselves or downloaded from a contract repository, transferring cryptoassets according to the contract terms. Marlowe will run first of all on the Cardano blockchain, but it is not tied to Cardano, and could run on other blockchains in the future.

Smart contracts running on Cardano will be able to access external data values, such as the exchange rate between ada and bitcoin, through oracles. In some ways, an oracle is just like a participant that makes a choice, and we plan to support oracle values as part of the implementation, allowing contracts to access values directly from a stock market ‘ticker’ or a popular data feed such as Coinbase.

Marlowe contracts can be used in many ways: for instance, a Marlowe program can automate the operation of a financial contract that transacts cryptocurrencies on a blockchain. Alternatively, for audit purposes, it could be used to record compliance of users’ actions to a contract being executed in the real world.

Marlowe is just one example of a DSL running on a blockchain, but it is also an exemplar of how other DSLs might be created to cover supply-chain management, insurance, accounting, and so on, leveraging the experience of designing and building Marlowe on the Cardano platform.

We have stressed that Marlowe is a special-purpose financial DSL, but what if you want to write other kinds of contract? To write those, Cardano has Plutus, a general purpose language running on the blockchain. Plutus contracts can handle all kinds of cryptoassets, and don’t have the constraints of Marlowe contracts: for example, they are unconstrained in how long they will remain active, and in how many participants they can involve. Indeed, every Marlowe contract is run by a single Plutus program, the Marlowe interpreter.

Marlowe as a domain-specific language for DeFi

Being domain-specific, rather than general purpose, has a number of advantages.

Contracts are written in the language of finance, rather than the language of the blockchain. This means that some sorts of errors are impossible to write: so certain kinds of incorrect contracts are ruled out completely. For example, every Marlowe contract will have a finite lifetime after which it will perform no further actions, and at that point any funds tied up in the contract will be returned to the participants, meaning that funds in a contract can never be locked up indefinitely.

It is possible to analyse, completely automatically, how a contract will behave in all circumstances, without having to run it. For example, it is possible to determine whether a particular contract can fail to make a payment in some cases, or whether it is guaranteed to make full payments in every eventuality.

Contract behaviour can be simulated in a browser, so that users can try out the different ways that a contract might behave, before committing funds and running it for real.

Users can create their DeFi contracts in different ways: they can write them as text, but also use visual programming to create smart contracts by fitting together blocks that represent the different components. Users can also choose from a range of templates and customise them as needed.

Next steps – and some prize challenges

Currently, Marlowe contracts can be written in Haskell or JavaScript or directly in Marlowe, and visually, using the Marlowe Playground, where it is also possible to simulate and analyse those contracts. Over the next few months we will continue revising and improving the user experience provided by the Playground, and continue implementing examples from the Actus project. At the same time, we will finalise the implementation of Marlowe on Cardano, so that Marlowe contracts will run on the blockchain itself. We look forward to sharing that work with you as soon as it is ready.

In the meantime, take a look at Marlowe Playground or join in one of the two Marlowe-based challenges running this month – there’s a $10,000 cryptocurrency fund to tackle the United Nations’ global development goals, and a $5,000-prize Actus event at the Wyoming Hackathon.

Creating a decentralized financial and social operating system for the world is the core mission of Cardano. But it’s not one that we can accomplish alone. That’s why we are always on the lookout for relationships which help us build a global foundation for growth. So, we’re thrilled to announce our hackathon challenge to support the UN’s sustainable development goals (SDGs) designed to accelerate progress on fighting hunger, injustice, and climate change.

Sustainability and blockchain

In this hackathon challenge we aim to give the blockchain community an opportunity to make an impact on international development. The challenge will draw on IOHK’s expertise in community-focused funding developed with Project Catalyst. This initiative brings innovation, voting, and decentralized funding to Cardano by crowdsourcing development proposals, and financing their implementation.

IOHK and United Nations personnel will use the Project Catalyst platform to find and fund initiatives that align with the UN’s Sustainable Development Goals. These goals were adopted by 193 world leaders in 2015. Each of the 17 targets focus on ending extreme poverty and hunger, fighting inequality and injustice, and tackling climate change by 2030.

This IOHK-sponsored challenge hopes to promote projects based in the digitization of finance which increase the efficacy and transparency of funding for the UN’s Decade of Action. In the run-up to the 2030 deadline for achieving the global sustainability goals, the UN is marking 75 years since its establishment. Given that the transnational organization works on global collective action problems it has engaged with blockchain technology as a solution.

Crowdsourcing the future

Participants in the program can put forward ideas focused on any of the 17 goals. To encourage participation, IOHK is sponsoring a prize fund of ada worth $10,000 as well as ongoing support to bring the projects to fruition. Proposals will be judged by a panel of IOHK and UN employees. They will determine the winners based on an idea’s technical prowess, scalability and social impact, as well as its financial and volunteer support. The winning ideas will be able to seek the advice of experts from both the UN and IOHK to ensure that they are implemented in the most impactful way.

To qualify for the scheme, entries must be open source and be created for use on the Cardano blockchain. Example code should be written in Marlowe, a domain specific language developed for financial contracts on Cardano. These do not need to be fully coded submissions. Instead they can be ideas which inspire anyone to get involved with blockchain technology and sustainable development. The proposal submission period opens on Saturday October 10th. Participants must be registered by then in order to submit. Entries must be finalized by October 18 at 11:59 MDT. Make sure to check the official rules to learn more.

Winners will be announced on October 24, United Nations Day, which marks the anniversary of the charter of the organization. We encourage everyone with an interest in using Cardano to achieve sustainability goals to get involved. Make your voice heard to help the UN’s Decade of Action now. If you are interested more generally in developing Cardano, join Project Catalyst on Ideascale.

In our Developer Deep Dive series of occasional technical blogs, we invite IOHK’s engineers to discuss their latest work and insights.

Haskell is a lazy language. The importance of laziness has been widely discussed elsewhere: Why Functional Programming Matters is one of the classic papers on the topic, and A History of Haskell: Being Lazy with Class discusses it at length as well. For the purposes of this blog we will take it for granted that laziness is something we want. But laziness comes at a cost, and one of the disadvantages is that laziness can lead to memory leaks that are sometimes difficult to find. In this post we introduce a new library called nothunks aimed at discovering a large class of such leaks early, and helping to debug them. This library was developed for our work on the Cardano blockchain, but we believe it will be widely applicable in other projects too.

A motivating example

Consider the tiny application below, which processes incoming characters and reports how many characters there are in total, in addition to some per-character statistics:

import qualified Data.Map.Strict as Map

data AppState = AppState {
      total :: !Int
    , indiv :: !(Map Char Stats)
    }
  deriving (Show)

type Stats = Int

update :: AppState -> Char -> AppState
update st c = st {
      total = total st + 1
    , indiv = Map.alter (Just . aux) c (indiv st)
    }
  where
    aux :: Maybe Stats -> Stats
    aux Nothing  = 1
    aux (Just n) = n + 1

initAppState :: AppState
initAppState = AppState {
      total = 0
    , indiv = Map.empty
    }

main :: IO ()
main = interact $ show . foldl' update initAppState

In this version of the code, the per-character statistics are simply how often we have seen each character. If we feed this code ‘aabbb’, it will tell us that it saw 5 characters, 2 of which were the letter ‘a’ and 3 of which were ‘b’:

# echo -n aabbb | cabal run example1
AppState {
    total = 5
  , indiv = fromList [('a',2),('b',3)]
  }

Moreover, if we feed the application a ton of data and construct a memory profile,

dd if=/dev/zero bs=1M count=10 | cabal run --enable-profiling example1 -- +RTS -hy

we see from Figure 1 that the application runs in constant space.

Figure 1. Memory profile for the first example

So far so good. But now suppose we make an innocuous-looking change. Suppose, in addition to reporting how often every character occurs, we also want to know the offset of the last time that the character occurs in the file:

type Stats = (Int, Int)

update :: AppState -> Char -> AppState
update st c = -- .. as before
  where
    aux :: Maybe Stats -> Stats
    aux Nothing       = (1     , total st)
    aux (Just (n, _)) = (n + 1 , total st)

The application works as expected:

# echo -n aabbb | cabal run example2
AppState {
    total = 5
  , indiv = fromList [('a',(2,1)),('b',(3,4))]
  }

and so the change is accepted in GitHub's PR code review and gets merged. However, although the code still works, it is now a lot slower.

# time (dd if=/dev/zero bs=1M count=100 | cabal run example1)
(..)
real    0m2,312s

# time (dd if=/dev/zero bs=1M count=100 | cabal run example2)
(..)
real    0m15,692s

We have a slowdown of almost an order of magnitude, although we are barely doing more work. Clearly, something has gone wrong, and indeed, we have introduced a memory leak (Figure 2).

Figure 2. Memory profile for example 2

Unfortunately, tracing a profile like this to the actual problem in the code can be very difficult indeed. What’s worse, although our change introduced a regression, the application still worked fine and so the test suite probably wouldn’t have failed. Such memory leaks tend to be discovered only when they get so bad in production that things start to break (for example, servers running out of memory), at which point you have an emergency on your hands.

In the remainder of this post we will describe how nothunks can help both with spotting such problems much earlier, and debugging them.

Instrumenting the code

Let’s first see what usage of nothunks looks like in our example. We modify our code and derive a new class instance for our AppState:

data AppState = AppState {
      total :: !Int
    , indiv :: !(Map Char Stats)
    }
  deriving (Show, Generic, NoThunks)

The NoThunks class is defined in the nothunks library, as we will see in detail later. Additionally, we will replace foldl' with a new function:

repeatedly :: forall a b. (NoThunks b, HasCallStack)
           => (b -> a -> b) -> (b -> [a] -> b)
repeatedly f = ..

We will see how to define repeatedly later, but, for now, think of it as 'foldl' with some magic sprinkled on top’. If we run the code again, the application will throw an exception almost immediately:

# dd if=/dev/zero bs=1M count=100 | cabal run example3
(..)
example3: Unexpected thunk with context
  ["Int","(,)","Map","AppState"]
CallStack (from HasCallStack):
  error, called at shared/Util.hs:22:38 in Util
  repeatedly, called at app3/Main.hs:38:26 in main:Main

The essence of the nothunks library is that we can check if a particular value contains any thunks we weren’t expecting, and this is what repeatedly is using to make sure we’re not inadvertently introducing any thunks in the AppState; it’s this check that is failing and causing the exception. We get a HasCallStack backtrace telling us where we introduced that thunk, and – even more importantly – the exception gives us a helpful clue about where the thunk was:

["Int","(,)","Map","AppState"]

This context tells us that we have an AppState containing a Map containing tuples, all of which were in weak head normal form (not thunks), but the tuple contained an Int which was not in weak head normal form: a thunk.

From a context like this it is obvious what went wrong: although we are using a strict map, we have instantiated the map at a lazy pair type, and so although the map is forcing the pairs, it’s not forcing the elements of those pairs. Moreover, we get an exception the moment we introduce the thunk, which means that we can catch such regressions in our test suite. We can even construct minimal counter-examples that result in thunks, as we will see later.

Using nothunks

Before we look at how the library works, let’s first see how it’s used. In the previous section we were using a magical function repeatedly, but didn’t see how we could define it. Let’s now look at this function:

repeatedly :: forall a b. (NoThunks b, HasCallStack)
           => (b -> a -> b) -> (b -> [a] -> b)
repeatedly f = go
  where
    go :: b -> [a] -> b
    go !b []     = b
    go !b (a:as) =
        let !b' = f b a
        in case unsafeNoThunks b' of
              Nothing    -> go b' as
              Just thunk -> error . concat $ [
                  "Unexpected thunk with context "
                , show (thunkContext thunk)
                ]

The only difference between repeatedly and foldl' is the call to unsafeNoThunks, which is the function that checks if a given value contains any unexpected thunks. The function is marked as ‘unsafe’ because whether or not a value is a thunk is not normally observable in Haskell; making it observable breaks equational reasoning, and so this should only be used for debugging or in assertions. Each time repeatedly applies the provided function f to update the accumulator, it verifies that the resulting value doesn’t contain any unexpected thunks; if it does, it errors out (in real code such a check would only be enabled in test suites and not in production).

One point worth emphasizing is that repeatedly reduces the value to weak head normal form (WHNF) before calling unsafeNoThunks. This is, of course, what makes a strict fold-left strict, and so repeatedly must do this to be a good substitute for foldl'. However, it is important to realize that if repeatedly did not do that, the call to unsafeNoThunks would trivially and immediately report a thunk; after all, we have just created the f b a thunk! Generally speaking, it is not useful to call unsafeNoThunks (or its IO cousin noThunks) on values that aren’t already in WHNF.

In general, long-lived application state should never contain any unexpected thunks, and so we can apply the same kind of pattern in other scenarios. For example, suppose we have a server that is a thin IO layer on top of a mostly pure code base, storing the application state in an IORef. Here, too, we might want to make sure that that IORef never points to a value containing unexpected thunks:

newtype StrictIORef a = StrictIORef (IORef a)

readIORef :: StrictIORef a -> IO a
readIORef (StrictIORef v) = Lazy.readIORef v

writeIORef :: (NoThunks a, HasCallStack)
           => StrictIORef a -> a -> IO ()
writeIORef (StrictIORef v) !x = do
    check x
    Lazy.writeIORef v x

check :: (NoThunks a, HasCallStack) => a -> IO ()
check x = do
    mThunk <- noThunks [] x
    case mThunk of
      Nothing -> return ()
      Just thunk ->
        throw $ ThunkException
                  (thunkContext thunk)
                  callStack

Since check already lives in IO, it can use noThunks directly, instead of using the unsafe pure wrapper; but otherwise this code follows a very similar pattern: the moment we might introduce a thunk, we instead throw an exception. One could imagine doing a very similar thing for, say, StateT, checking for thunks in put:

newtype StrictStateT s m a = StrictStateT (StateT s m a)
  deriving (Functor, Applicative, Monad)

instance (Monad m, NoThunks s)
      => MonadState s (StrictStateT s m) where
  get    = StrictStateT $ get
  put !s = StrictStateT $
      case unsafeNoThunks s of
        Nothing -> put s
        Just thunk -> error . concat $ [
            "Unexpected thunk with context "
          , show (thunkContext thunk)
          ]

Minimal counter-examples

In some applications, there can be complicated interactions between the input to the program and the thunks it may or may not create. We will study this through a somewhat convoluted but, hopefully, easy-to-understand example. Suppose we have a server that is processing two types of events, A and B:

data Event = A | B
  deriving (Show)

type State = (Int, Int)

initState :: State
initState = (0, 0)

update :: Event -> State -> State
update A (a, b)    = let !a' = a + 1 in (a', b)
update B (a, b)
  | a < 1 || b < 1 = let !b' = b + 1 in (a, b')
  | otherwise      = let  b' = b + 2 in (a, b')

The server’s internal state consists of two counters, a and b. Each time we see an A event, we just increment the first counter. When we see a B event, however, we increment b by 1 only if a and b haven’t reached 1 yet, and by 2 otherwise. Unfortunately, the code contains a bug: in one of these cases, part of the server’s state is not forced and we introduce a thunk. (Disclaimer: the code snippets in this blog post are not intended to be good examples of coding, but to make it obvious where memory leaks are introduced. Typically, memory leaks should be avoided by using appropriate data types, not by modifying code.)

A minimal counter-example that will demonstrate the bug would therefore involve two events A and B, in any order, followed by another B event. Since we get an exception the moment we introduce an exception, we can then use a framework such as quickcheck-state-machine to find bugs like this and construct such minimal counter-examples.

Here’s how we might set up our test. Explaining how quickcheck-state-machine (QSM) works is well outside the scope of this blog post; if you’re interested, a good starting point might be An in-depth look at quickcheck-state-machine. For this post, it is enough to know that in QSM we are comparing a real implementation against some kind of model, firing off ‘commands’ against both, and then checking that the responses match. Here, both the server and the model will use the update function, but the ‘real’ implementation will use the StrictIORef type we introduced above, and the mock implementation will just use the pure code, with no thunks check. Thus, when we compare the real implementation against the model, the responses will diverge whenever the real implementation throws an exception (caused by a thunk):

data T

type instance MockState   T = State
type instance RealMonad   T = IO
type instance RealHandles T = '[]

data instance Cmd T f hs where
  Cmd :: Event -> Cmd T f '[]

data instance Resp T f hs where
  -- We record any exceptions that occurred
  Resp :: Maybe String -> Resp T f '[]

deriving instance Eq   (Resp T f hs)
deriving instance Show (Resp T f hs)
deriving instance Show (Cmd  T f hs)

instance NTraversable (Resp T) where
  nctraverse _ _ (Resp ok) = pure (Resp ok)

instance NTraversable (Cmd T) where
  nctraverse _ _ (Cmd e) = pure (Cmd e)

sm :: StrictIORef State -> StateMachineTest T
sm state = StateMachineTest {
      runMock    = \(Cmd e) mock ->
        (Resp Nothing, update e mock)
    , runReal    = \(Cmd e) -> do
        real <- readIORef state
        ex   <- try $ writeIORef state (update e real)
        return $ Resp (checkOK ex)
    , initMock   = initState
    , newHandles = \_ -> Nil
    , generator  = \_ -> Just $
        elements [At (Cmd A), At (Cmd B)]
    , shrinker   = \_ _ -> []
    , cleanup    = \_ -> writeIORef state initState
    }
  where
    checkOK :: Either SomeException () -> Maybe String
    checkOK (Left err) = Just (show err)
    checkOK (Right ()) = Nothing

(This uses the new Lockstep machinery in QSM that we introduced in the Munihac 2019 hackathon.)

If we run this test, we get the minimal counter-example we expect, along with the HasCallStack backtrace and the context telling us precisely that we have a thunk inside a lazy pair:

*** Failed! Falsified (after 6 tests and 2 shrinks):
Commands
  { unCommands =
      [ Command At { unAt = Cmd B } At { unAt = Resp Nothing } []
      , Command At { unAt = Cmd A } At { unAt = Resp Nothing } []
      , Command At { unAt = Cmd B } At { unAt = Resp Nothing } []
      ]
  }

(..)

Resp (Just "Thunk exception in context [Int,(,)]
    called at shared/StrictIORef.hs:26:5 in StrictIORef
    writeIORef, called at app5/Main.hs:71:37 in Main")
:/= Resp Nothing

The combination of a minimal counter-example, a clear context, and the backtrace, makes finding most such memory leaks almost trivial.

Under the hood

The core of the nothunks library is the NoThunks class:

-- | Check a value for unexpected thunks
class NoThunks a where
  noThunks   :: [String] -> a -> IO (Maybe ThunkInfo)
  wNoThunks  :: [String] -> a -> IO (Maybe ThunkInfo)
  showTypeOf :: Proxy a -> String

data ThunkInfo = ThunkInfo {
      thunkContext :: Context
    }
deriving (Show)

type Context = [String]

All of the NoThunks class methods have defaults, so instances can be, and very often are, entirely empty, or – equivalently – derived using DeriveAnyClass.

The noThunks function is the main entry point for application code, and we have already seen it in use. Instances of NoThunks, however, almost never need to redefine noThunks and can use the default implementation, which we will take a look at shortly. Conversely, wNoThunks is almost never useful for application code but it’s where most of the datatype-specific logic lives, and is used by the default implementation of noThunks; we will see a number of examples of it below. Finally, showTypeOf is used to construct a string representation of a type when constructing the thunk contexts; it has a default in terms of Generic.

noThunks

Suppose we are checking if a pair contains any thunks. We should first check if the pair itself is a thunk, before we pattern match on it. After all, pattern matching on the pair would force it, and so if it had been a thunk, we wouldn’t be able to see this any more. Therefore, noThunks first checks if a value itself is a thunk, and if it isn’t, it calls wNoThunks; the w stands for WHNF: wNoThunks is allowed to assume (has as precondition) that its argument is not itself a thunk and so can be pattern-matched on.

noThunks :: [String] -> a -> IO (Maybe ThunkInfo)
noThunks ctxt x = do
    isThunk <- checkIsThunk x
    if isThunk
      then return $ Just ThunkInfo { thunkContext = ctxt' }
      else wNoThunks ctxt' x
  where
    ctxt' :: [String]
    ctxt' = showTypeOf (Proxy @a) : ctxt

Note that when wNoThunks is called, the (string representation of) type a has already been added to the context.

wNoThunks

Most of the datatype-specific work happens in wNoThunks; after all, we can now pattern match. Let’s start with a simple example, a manual instance for a type of strict pairs:

data StrictPair a b = StrictPair !a !b

instance (NoThunks a, NoThunks b)
      => NoThunks (StrictPair a b) where
  showTypeOf _ = "StrictPair"
  wNoThunks ctxt (StrictPair x y) = allNoThunks [
        noThunks ctxt x
      , noThunks ctxt y
      ]

Because we have verified that the pair itself is in WHNF, we can just extract both components, and recursively call noThunks on both of them. Function allNoThunks is a helper defined in the library that runs a bunch of thunk checks, stopping at the first one that reports a thunk.

Occasionally we do want to allow for selected thunks. For example, suppose we have a set of integers with a cached total field, but we only want to compute that total if it’s actually used:

data IntSet = IntSet {
      toSet :: !(Set Int)

      -- | Total
      --
      -- Intentionally /not/ strict:
      -- Computed when needed (and then cached)
    , total :: Int
    }
  deriving (Generic)

Since total must be allowed to be a thunk, we skip it in wNoThunks:

instance NoThunks IntSet where
  wNoThunks ctxt (IntSet xs _total) = noThunks ctxt xs

Such constructions should probably only be used sparingly; if the various operations on the set are not carefully defined, the set might hold on to all kinds of data through that total thunk. Code like that needs careful thought and careful review.

Generic instance

If no implementation is given for wNoThunks, it uses a default based on GHC generics. This means that for types that implement Generic, deriving a NoThunks instance is often as easy as in the AppState example above, simply saying:

data AppState = AppState {
      total :: !Int
    , indiv :: !(Map Char Stats)
    }
  deriving (Show, Generic, NoThunks)

Many instances in the library itself are also defined using the generic instance; for example, the instance for (default, lazy) pairs is just:

instance (NoThunks a, NoThunks b) => NoThunks (a, b)

Deriving-via wrappers

Sometimes, we don’t want the default behavior implemented by the generic instance, but defining an instance by hand can be cumbersome. The library therefore provides a few newtype wrappers that can be used to conveniently derive custom instances. We will discuss three such wrappers here; the library comes with a few more.

Only check for WHNF

If all you want to do is check if a value is in weak head normal form (ie, check that it is not a thunk itself, although it could contain thunks), you can use OnlyCheckIsWhnf. For example, the library defines the instance for Bool as:

deriving via OnlyCheckWhnf Bool
         instance NoThunks Bool

For Bool, this is sufficient: when a boolean is in weak head normal form, it won’t contain any thunks. The library also uses this for functions:

deriving via OnlyCheckWhnfNamed "->" (a -> b)
         instance NoThunks (a -> b)

(Here, the Named version allows you to explicitly define the string representation of the type to be included in the thunk contexts.) Using OnlyCheckWhnf for functions means that any values in the function closure will not be checked for thunks. This is intentional and a subtle design decision; we will come back to this in the section on permissible thunks below.

Skipping some fields

For types such as IntSet where most fields should be checked for thunks, but some fields should be skipped, we can use AllowThunksIn:

deriving via AllowThunksIn '["total"] IntSet
         instance NoThunks IntSet

This can be handy for large record types, where giving the instance by hand is cumbersome and, moreover, can easily get out of sync when changes to the type (for example, a new field) are not reflected in the definition of wNoThunks.

Inspecting the heap directly

Instead of going through the class system and the NoThunks instances, we can also inspect the GHC heap directly. The library makes this available through the InspectHeap newtype, which has an instance:

instance Typeable a => NoThunks (InspectHeap a) where
  -- ..

Note that this does not depend on a NoThunks instance for a. We can use this like any other deriving-via wrappers, for example:

deriving via InspectHeap TimeOfDay
         instance NoThunks TimeOfDay

The advantage of such an instance is that we do not require instances for any nested types; for example, although TimeOfDay has a field of type Pico, we don’t need a NoThunks instance for it.

The disadvantage is that we lose all compositionality. If there are any types nested inside for which we want to allow for thunks, we have no way of overriding the behaviour of the no-thunks check for those types. Since we are inspecting the heap directly, and the runtime system does not record any type information, any NoThunks instances for those types are irrelevant and we will report any thunks that it finds. Moreover, when we do find such a thunk, we cannot report a useful context, because – again – we have no type information. If noThunks finds a thunk deeply nested inside some T (whose NoThunks instance was derived using InspectHeap), it will merely report "..." : "T" as the context (plus perhaps any context leading to T itself).

Permissible thunks

Some data types inherently depend on the presence of thunks. For example, the Seq type defined in Data.Sequence internally uses a finger tree. Finger trees are a specialized data type introduced by Ralf Hinze and Ross Paterson; for our purposes, all you need to know is that finger trees make essential use of thunks in their spines to achieve their asymptotic complexity bounds. This means that the NoThunks instance for Seq must allow for thunks in the spine of the data type, although it should still verify that there are no thunks in any of the elements in the sequence. This is easy enough to do; the instance in the library is:

instance NoThunks a => NoThunks (Seq a) where
  showTypeOf _   = "Seq"
  wNoThunks ctxt = noThunksInValues ctxt . toList

Here, noThunksInValues is a helper function that checks a list of values for thunks, without checking the list itself.

However, the existence of types such as Seq means that the non-compositionality of InspectHeap can be a big problem. It is also the reason that for functions we merely check if the function is in weak head normal form. Although the function could have thunks in its closure, we don’t know what their types are. We could check the function closure for thunks (using InspectHeap), but if we did, and that closure contained, say, a Seq among its values, we might incorrectly report an unexpected thunk. Because it is more problematic if the test reports a bug when there is none than when an actual bug is not reported, the library opts to check only functions for WHNF. If in your application you store functions, and it is important that these functions are checked for thunks, then you can define a custom newtype around a -> b with a NoThunks instance defined using InspectHeap (but only if you are sure that your functions don’t refer to types that must be allowed to have thunks).

Comparison with the heap/stack limit size method

In 2016, Neil Mitchell gave a very nice talk at HaskellX, where he presented a method for finding memory leaks (he has also written a blog post on the topic). The essence of the method is to run your test suite with much reduced stack and heap limits, so that if there is a memory leak in your code, you will notice it before it hits production. He then advocates the use of the -xc runtime flag to get a stack trace when such a ‘stack limit exhausted’ exception is thrown.

The technique advocated in this post has a number of advantages. We get an exception the moment a thunk is created, so the stack trace we get is often much more useful. Together with the context reported by noThunks, finding the problem is usually trivial. Interpreting the stack reported by -xc can be more difficult, because this exception is thrown when the limit is exhausted, which may or may not be related to the code that introduced the leak in the first place. Moreover, since the problem only becomes known when the limit is exhausted, minimal counter-examples are out of the question. It can also be difficult to pick a suitable value for the limit; how much memory does the test site actually need, and what would constitute a leak? Finally, -xc requires your program to be compiled with profiling enabled, which means you’re debugging something different to what you’d run in production, which is occasionally problematic.

Having said all that, the nothunks method does not replace the heap/stack limit method, but complements it. The nothunks approach is primarily useful for finding space leaks in pieces of data where it’s clear that we don’t want any thunk build-up, typically long-lived application state. It is less useful for finding more ‘local’ space leaks, such as a function accumulator not being updated strictly. For finding such leaks, setting stack/heap limits is still a useful technique.

Conclusions

Long-lived application data should, typically, not have any thunk build-up. The nothunks library can verify this through the noThunks and unsafeNoThunks function calls, which check if the supplied argument contains any unexpected thunks. These checks can then be used in assertions to check that no thunks are created. This means that if we do introduce a thunk by mistake, we get an immediate test failure, along with a callstack to the place where the thunk was created as well as a context providing a helpful hint on where the thunk is. Together with a testing framework, this makes memory leaks much easier to debug and avoid. Indeed, they have mostly been a thing of the past in our work on Cardano since we started using this approach.

Today, we are announcing the launch of Project Catalyst’s first public fund, an important first step into the world of on-chain governance, treasury, and community innovation for Cardano.

The public fund launch follows five months of intense activity, across two previous trial ‘funds’. ‘Fund 0’ was the very first experiment, using a focus group made up from IOG team members. ‘Fund 1’ was the first time we introduced the idea to the Cardano community, recruiting a group of some 50 volunteers to help us develop the platform and processes. While this voting cycle did not offer ‘real’ funding, it served as a hugely valuable way to give our team and the Cardano community members a chance to test drive and refine the emerging process.

We still have a way to go. But with the community's support, we want to maintain the pace of progress we have already set. If Fund 0 was the technical runthrough, Fund 1 was the dress rehearsal. Announced today, Fund 2 is the opening night where the star acts of the community get the chance to compete for the funding to bring their project center stage.

Funding the future

We have learned a lot since we kicked off the private phase of the program in August. Support from our pioneer group of 50 community participants helped us to identify areas for improvement so we could develop and refine the process before opening things up more widely. We learned that providing clear documentation and guidelines helps the community engage more deeply and focus on the ideas. We also learned we can provide alternative avenues for the community to discuss “meta” proposals. This enhances the Catalyst and Voltaire processes while focusing attention on writing impactful proposals. Furthermore, we realized that it was important for IOHK to support individuals writing proposals to ensure their ideas were fairly represented.

Cardano will thrive by unlocking the creative potential of our global community. Our voting protocol will only be as good as the ideas which feed into it. To that end, we are developing a guide to help anyone develop the best possible proposal for Fund 2 and beyond.

The first public fund we’re announcing today contains up to $250k-worth of ada, which the community can access. Anyone can bring their idea and create a proposal. Through a public vote, ‘winning’ proposals will begin a development process.

Initially, we’re keeping the focus tight, asking the community to address a challenge statement: “How can we encourage developers and entrepreneurs to build Dapps and businesses on top of Cardano in the next 6 months?” Funding proposals (or ‘FPs’) can address this with a wide variety of ideas – from marketing initiatives and infrastructure development, to business planning and content creation.

The first stage will be to ‘explore the challenge’, asking members of the community to provide their perspectives. Next, we’ll encourage everyone to put their best ideas forward on the innovation platform to collaborate and discuss via a dedicated Telegram chat channel.

A public vote

After the initial ideation, collaboration and proposal stages, we’ll be putting things to a vote. Proposals can be reviewed either on the innovation platform or on the new mobile voting application, currently in development. When it comes time to vote, all participants will need to register to vote through the voting app. The ‘right’ to vote will be linked to each participant’s ada holdings and will earn them additional rewards for voting. Participating in this first funding round will not prevent ada holders from delegating their ada and earning rewards as normal. Voting effectively functions like a ‘transaction’, allowing all participants to cast their vote to indicate ‘yes,’ or ‘no.’ We’ll share further information on the app and the voting process in a future blog post.

Collaboration and innovation

Voltaire will be a crucial building block in the Cardano ecosystem, because it allows every ada holder to be involved in making decisions on the future development of the platform and contribute to the growth of the ecosystem. Project Catalyst is the important first component in delivering that capability. The early stages of this experiment have already demonstrated the passion and commitment of the Cardano community to develop this further. With the introduction of an on-chain voting and treasury system, network participants will be able to use their stake and voting rights to steer Cardano towards tackling shared goals, in a democratic and self-sustaining way.

To find out more, you can watch our announcement Crowdcast with Charles Hoskinson and Project Catalyst’s product manager, Dor Garbash.