Using Marlowe from the ghci command line
This tutorial shows you how to use Marlowe from within Haskell, and in particular shows you 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 the following:
- 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?