Using Marlowe from the ghci command line¶
This tutorial shows you how to use Marlowe from within Haskell, and in particular shows how to exercise a contract using the semantics given earlier.
Marlowe in Haskell¶
This tutorial works in the version of Marlowe which can be found in the
main
branch of the marlowe-cardano repository.
We can run ghci by using the nix-shell available in marlowe-dependency-docs repository:
git clone "https://github.com/input-output-hk/marlowe-dependency-docs.git"
cd marlowe-dependency-docs
nix-shell
ghci
A standalone version and formalisation of the semantics can also be found in the marlowe repository, but some details may be slightly differently, like the use of slots instead of POSIX time.
Stepping through contracts¶
As we saw earlier the semantics of a single transaction are defined by the function
computeTransaction :: TransactionInput -> State -> Contract -> TransactionOutput
where the types are defined like this:
data TransactionInput = TransactionInput
{ txInterval :: TimeInterval
, txInputs :: [Input] }
data TransactionOutput =
TransactionOutput
{ txOutWarnings :: [TransactionWarning]
, txOutPayments :: [Payment]
, txOutState :: State
, txOutContract :: Contract }
| Error TransactionError
and States
are defined like this, with a helper function to define
an initially empty state:
data State = State { accounts :: Accounts
, choices :: Map ChoiceId ChosenNum
, boundValues :: Map ValueId Integer
, minTime :: POSIXTime }
emptyState :: POSIXTime -> State
emptyState sn = State { accounts = Map.empty
, choices = Map.empty
, boundValues = Map.empty
, minTime = sn }
We can use the facilities of ghci
to step through a contract one
transaction at a time, and, here, we will do that with the embedded
escrow contract contained in
Escrow.hs.
To load the contract into the interpreter we first import some libraries and create utility functions:
Prelude> :set -XOverloadedStrings
Prelude> import qualified Marlowe.Contracts.Escrow as Escrow
Prelude Escrow> import qualified Language.Marlowe.Extended.V1 as EM
Prelude Escrow EM> import Language.Marlowe as M
Prelude Escrow EM M> import qualified Data.Time.Clock.POSIX as P
Prelude Escrow EM M P> :set prompt "> "
> let toPOSIX = POSIXTime . floor . P.utcTimeToPOSIXSeconds . read
> let toEMPOSIX = EM.POSIXTime . floor . P.utcTimeToPOSIXSeconds . read
The example is written in Extended Marlowe, so we first need to convert it to core Marlowe in order to execute it:
> let Just contract = EM.toCore $ Escrow.escrow (EM.Constant 450) "bob" "alice" "carol" (toEMPOSIX "2023-02-01 00:00:00.000000 UTC") (toEMPOSIX "2023-03-01 00:00:00.000000 UTC") (toEMPOSIX "2023-04-01 00:00:00.000000 UTC") (toEMPOSIX "2023-05-01 00:00:00.000000 UTC") :: Maybe Contract
Now we can single step it using the facility to make local bindings:
> let (TransactionOutput txWarn1 txPay1 state1 con1) = computeTransaction (TransactionInput (toPOSIX "2023-01-01 00:00:00.000000 UTC", toPOSIX "2023-01-31 23:59:59.000000 UTC") [NormalInput (IDeposit "bob" "alice" ada 450)]) (emptyState 0) contract
In doing this we have pattern matched the output of an application of
computeTransaction
, which takes three inputs: the second is an
initial state (at slot number 0) and the third is the initial escrow
contract. The first is a TransactionInput
which contains a
TimeInterval
– here ((toPOSIX "2023-01-01 00:00:00.000000 UTC"), (toPOSIX "2023-01-31 23:59:59.000000 UTC"))
– and
a deposit of 450 Lovelace from "alice"
into bob
’s’ account namely
NormalInput (IDeposit "bob" "alice" ada 450)
.
Note
If you want to try this for yourself in ghci, you can copy and paste from the code examples: they are in horizontally scrolling windows.
The output is matched with
TransactionOutput txWarn1 txPay1 state1 con1
so that we can examine
the various components separately:
> txWarn1
[]
> txPay1
[]
> state1
State {accounts = Map {unMap = [(("bob",Token "" ""),450)]}, choices = Map {unMap = []}, boundValues = Map {unMap = []}, minTime = POSIXTime {getPOSIXTime = 1672531200}}
> con1
When [Case (Choice (ChoiceId "Everything is alright" "alice") [Bound 0 0]) Close,Case (Choice (ChoiceId "Report problem" "alice") [Bound 1 1]) (Pay "bob" (Account "alice") (Token "" "") (Constant 450) (When [Case (Choice (ChoiceId "Confirm problem" "bob") [Bound 1 1]) Close,Case (Choice (ChoiceId "Dispute problem" "bob") [Bound 0 0]) (When [Case (Choice (ChoiceId "Dismiss claim" "carol") [Bound 0 0]) (Pay "alice" (Account "bob") (Token "" "") (Constant 450) Close),Case (Choice (ChoiceId "Confirm claim" "carol") [Bound 1 1]) Close] (POSIXTime {getPOSIXTime = 1682899200}) Close)] (POSIXTime {getPOSIXTime = 1680307200}) Close))] (POSIXTime {getPOSIXTime = 1677628800}) Close
This shows that the transaction generates no warnings or payments, but
updates the state to show the balance in the account "bob"
, and
updates the contract, ready to receive a choice from Alice.
In the next state the contract is waiting for input, and if Alice agrees that “Everything is alright”, then a payment to Bob is generated. This is verified through this interaction in GHCI:
> let (TransactionOutput txWarn2 txPay2 state2 con2) = computeTransaction (TransactionInput (toPOSIX "2023-02-01 00:00:00.000000 UTC", toPOSIX "2023-02-28 23:59:59.000000 UTC") [NormalInput (IChoice (ChoiceId "Everything is alright" "alice") 0)]) state1 con1
> txPay2
[Payment "bob" (Party "bob") (Value (Map [(,Map [("",450)])]))]
> con2
Close
> state2
State {accounts = Map {unMap = []}, choices = Map {unMap = [(ChoiceId "Everything is alright" "alice",0)]}, boundValues = Map {unMap = []}, minTime = POSIXTime {getPOSIXTime = 1675209600}}
An alternative way of doing this is to add these definitions to a
working file, e.g. Build.hs
, where these definitions will be
preserved. Indeed, it would be very sensible to include some of the
definitions used above in such a file.
Alternative routes through the contract¶
An alternative execution of the contract is given by
First step: Alice deposits money as in the earlier example.
Second step: Alice reports a problem and Bob disagrees. This can be done like this:
> let (TransactionOutput txWarn2 txPay2 state2 con2) = computeTransaction (TransactionInput (toPOSIX "2023-02-01 00:00:00.000000 UTC", toPOSIX "2023-02-28 23:59:59.000000 UTC") [NormalInput (IChoice (ChoiceId "Report problem" "alice") 1), NormalInput (IChoice (ChoiceId "Dispute problem" "bob") 0)]) state1 con1
> con2
When [Case (Choice (ChoiceId "Dismiss claim" "carol") [Bound 0 0]) (Pay "alice" (Account "bob") (Token "" "") (Constant 450) Close),Case (Choice (ChoiceId "Confirm claim" "carol") [Bound 1 1]) Close] (POSIXTime {getPOSIXTime = 1682899200}) Close
> state2
State {accounts = Map {unMap = [(("alice",Token "" ""),450)]}, choices = Map {unMap = [(ChoiceId "Report problem" "alice",1),(ChoiceId "Dispute problem" "bob",0)]}, boundValues = Map {unMap = []}, minTime = POSIXTime {getPOSIXTime = 1675209600}}
This shows that we’re now in a contract where the choice is up to Carol,
and that there is still the 450 Lovelace in the "alice"
account.
Note that we have two inputs in the same transaction, Marlowe
supports this as long as the transaction is signed by all relevant
parties, and the time interval is before the timeout of the earliest
When
.
Third step: Carol makes a choice. If she chooses “Dismiss claim”, payment to Bob is made. If she chooses “Confirm claim”, Alice is refunded. Let’s do that now:
> let (TransactionOutput txWarn3 txPay3 state3 con3) = computeTransaction (TransactionInput (toPOSIX "2023-04-01 00:00:00.000000 UTC", toPOSIX "2023-04-30 23:59:59.000000 UTC") [NormalInput (IChoice (ChoiceId "Confirm claim" "carol") 1)]) state2 con2
> txPay3
[Payment "alice" (Party "alice") (Value (Map [(,Map [("",450)])]))]
> con3
Close
> state3
State {accounts = Map {unMap = []}, choices = Map {unMap = [(ChoiceId "Report problem" "alice",1),(ChoiceId "Dispute problem" "bob",0),(ChoiceId "Confirm claim" "carol",1)]}, boundValues = Map {unMap = []}, minTime = POSIXTime {getPOSIXTime = 1680307200}}
So now the contract is ready to Close
, and so to refund any
remaining money, but it is clear from state3
that there are no
accounts containing non-zero balances, and so the contract is
terminated.
Why is single stepping useful? It is the equivalent of debugging, and we are able to see the internal state of the contract at each stage, the contract continuation, i.e. what remains to be executed, and the actions produced at each step.
Exercise
Explore some other ways of engaging with the contract - What happens when Bob confirms there is a problem? - What happens if Bob and Alice disagree, but Carol sides with Bob?