The Marlowe data types

This tutorial formally introduces Marlowe as a Haskell data type, as well as presenting the different types used by the model, and discussing a number of assumptions about the infrastructure in which contracts will be run. The code that we describe here comes from the Haskell modules Semantics.hs and Util.hs.

Marlowe

The Marlowe domain-specific language (DSL) is modelled as a collection of algebraic types in Haskell, with contracts being given by the Contract type:

data Contract = Close
              | Pay Party Payee Token Value Contract
              | If Observation Contract Contract
              | When [Case] Timeout Contract
              | Let ValueId Value Contract
              | Assert Observation Contract

We saw in the previous tutorial what these contracts do. In the rest of this tutorial we will dig a bit deeper into the Haskell types that are used to represent the various components of the contracts, including accounts, values, observations, and actions. We will also look at types that relate to the execution of contracts, including inputs, states, the environment.

Basic components

In modelling basic parts of Marlowe we use a combination of Haskell data types, that define new types, and type synonyms that give a new name to an existing type. 1

A Marlowe Account holds amounts of multiple currencies and/or fungible and non-fungible tokens. A concrete amount is indexed by a Token, which is a pair of CurrencySymbol and TokenName. You can think of an Account as a Map Token Integer, where

data Token = Token CurrencySymbol TokenName

Cardano’s Ada token is Token adaSymbol adaToken. But you are free to create your own currencies and tokens.

Tokens of a currency can represent roles in a contract, e.g “buyer” and “seller”. Think of a legal contract in the sense of “hereafter referred to as the Performer/Vendor/Artist/Consultant”. This way we can decouple the notion of ownership of a contract role, and make it tradable. So you can sell your loan or buy a share of a role in some contract.

tradeRoles = CurrencySymbol "TradeRoles"
buyer = TokenName "buyer"
seller = TokenName "seller"
account = fromList[(Token tradeRoles buyer, 1), (ada 1000)]

Here account holds a buyer token of currency “TradeRoles”, and 1000 lovelace.

A Party is represented as either a public key hash or a role name.

data Party  = PK PubKeyHash | Role TokenName

In order to progress a Marlowe contract, a party must provide an evidence. For PK party that would be a valid signature of a transaction signed by a private key of a public key that hashes to party’s PubKeyHash, similarly to Bitcoin’s Pay to Public Key Hash mechanism. For a Role party the evidence is spending a role token within the same transaction, usually to the same owner.

So, Role parties will look like (Role "alice"), (Role "bob") and so on. However, Haskell allows us to present and read in these values more concisely (by declaring a custom instance of Show and using overloaded strings) so that these can be input and read as "alice", "bob" etc.

Slot numbers and amounts of money are treated in a similar way; with the same show/overload approach they will appear in contracts as numbers:

data Slot    = Slot Integer
type Timeout = Slot

Note that "alice" is the owner here in the sense that she will be refunded any money in the account when the contract terminates.

We can use overloaded strings to allow us to abbreviate this account by the name of its owner: in this case "alice".

A payment can be made to one of the parties to the contract, or to one of the accounts of the contract, and this is reflected in the definition

data Payee = Account Party
           | Party Party

Choices – of integers – are identified by ChoiceId which combines a name for the choice with the Party who had made the choice:

type ChoiceName = Text
data ChoiceId   = ChoiceId ChoiceName Party
type ChosenNum  = Integer

Values, as defined using Let are also identified by integers. 2

data ValueId    = ValueId Integer

Values, observations and actions

Building on the basic types, we can describe three higher-level components of contracts: a type of values, on top of that a type of observations, and also a type of actions, which trigger particular cases. First, looking at Value we have

data Value = AvailableMoney Party Token
           | Constant Integer
           | NegValue Value
           | AddValue Value Value
           | SubValue Value Value
           | MulValue Value Value
           | Scale Rational Value
           | ChoiceValue ChoiceId
           | SlotIntervalStart
           | SlotIntervalEnd
           | UseValue ValueId
           | Cond Observation Value Value

The different kinds of values – all of which are Integer – are pretty much self explanatory, but for completeness we have

  • Lookup of the value in an account AvailableMoney, made in a choice ChoiceValue and in an identifier that has already been defined UseValue.

  • Arithmetic constants and operators.

  • Scale multiplies a Value by a rational constant, say, 2/3, and rounds the result using ‘half even’ aka ‘banking’ rounding. So, 14/10 rounds to 1, both 15/10 and 25/10 rounds to 2.

  • The start and end of the current slot interval; see below for further discussion of this.

  • Cond represents if-expressions, that is - first argument to Cond is a condition (Observation) to check, second is a Value to take when condition is satisfied and the last one is a Value for unsatisfied condition; for example: (Cond FalseObs (Constant 1) (Constant 2)) is equivalent to (Constant 2)

Next we have observations

data Observation = AndObs Observation Observation
                 | OrObs Observation Observation
                 | NotObs Observation
                 | ChoseSomething ChoiceId
                 | ValueGE Value Value
                 | ValueGT Value Value
                 | ValueLT Value Value
                 | ValueLE Value Value
                 | ValueEQ Value Value
                 | TrueObs
                 | FalseObs

These are really self-explanatory: we can compare values for (in)equality and ordering, and combine observations using the Boolean connectives. The only other construct ChoseSomething indicates whether any choice has been made for a given ChoiceId.

Cases and actions are given by these types:

data Case = Case Action Contract

data Action = Deposit Party Party Token Value
            | Choice ChoiceId [Bound]
            | Notify Observation

data Bound = Bound Integer Integer

Three kinds of action are possible:

  • A Deposit n p t v makes a deposit of value v of token t from party p into account n.

  • A choice is made for a particular id with a list of bounds on the values that are acceptable. For example, [Bound 0 0, Bound 3 5] offers the choice of one of 0, 3, 4 and 5.

  • The contract is notified that a particular observation be made. Typically this would be done by one of the parties, or one of their wallets acting automatically.

This completes our discussion of the types that make up Marlowe contracts.

Transactions

As we noted earlier, the semantics of Marlowe consist in building transactions, like this:

transaction A transaction is built from a series of steps, some of which consume an input value, and others produce effects, or payments. In describing this we explained that a transaction modified a contract (to its continuation) and the state, but more precisely we have a function

computeTransaction :: TransactionInput -> State -> Contract -> TransactionOutput

where the types are defined like this:

data TransactionInput = TransactionInput
    { txInterval :: SlotInterval
    , txInputs   :: [Input] }

data TransactionOutput =
    TransactionOutput
        { txOutWarnings :: [ReduceWarning]
        , txOutPayments :: [Payment]
        , txOutState    :: State
        , txOutContract :: Contract }
    | Error TransactionError

The notation used here adds field names to the arguments of the constructors, giving selectors for the data as well as making in clearer the purpose of each field.

The TransactionInput type has two components: the SlotInterval in which it can validly be added to the blockchain, and an ordered sequence of Input values to be processed in that transaction.

A TransactionOutput value has four components: the last two are the updated State and Contract, while the second gives a ordered sequence of Payments produced by the transaction. The first component contains a list of any warnings produced by processing the transaction.

Slot ranges

This is part of the architecture of Cardano/Plutus, which acknowledges that it is not possible to predict precisely in which slot a particular transaction will be processed. Transactions are therefore given a slot interval in which they are expected to be processed, and this carries over to Marlowe: each step of a Marlowe contract is processed in the context of a range of slots.

data Slot         = Slot Integer
data SlotInterval = SlotInterval Slot Slot

ivFrom, ivTo :: SlotInterval -> Slot
ivFrom (SlotInterval from _) = from
ivTo   (SlotInterval _ to)   = to

How does this affect the processing of a Marlowe contract? Each step is processed relative to a slot interval, and the current slot value needs to lie within that interval.

The endpoints of the interval are accessible as the values SlotIntervalStart and SlotIntervalEnd, and these can be used in observations. Timeouts need to be processed unambiguously, so that all values in the slot interval have to either have exceeded the timeout for it to take effect, or fall before the timeout, for normal execution to take effect. In other words, the timeout value needs to either be less or equal than SlotIntervalStart (in order for the timeout to take effect) or be strictly greater than SlotIntervalEnd (for normal execution to take place).

Notes

The model makes a number of assumptions about the blockchain infrastructure in which it is run.

  • It is assumed that cryptographic functions and operations are provided by a layer external to Marlowe, and so they need not be modelled explicitly.

  • We assume that time is “coarse grained” and measured by block or slot number, so that, in particular, timeouts are delimited using block/slot numbers.

  • Making a deposit is not something that a contract can perform; rather, it can request that a deposit is made, but that then has to be established externally: hence the input of (a collection of) deposits for each transaction.

  • The model manages the refund of funds back to the owner of a particular account when a contract reaches the point of Close.

1

In fact we used newtype declarations rather than data types because they are more efficiently implemented.

2

This may be modified in the future to allow values to be named by strings.