Solutions

Here we present solutions to the exercises that can be found throughout this language guide – both to the simpler ones from the introductory chapters, and to the more advanced ones presented in the previous section.

The solutions presented here are merely examples.

Solution: Pay on delivery

See the exercise statement.

type Delivery : Event {
  recipient : Agent,
  item : String
}

type Payment : Event {
  amount : Int,
  recipient : Agent,
  item : String
}

contract entrypoint sale = \(buyer, seller, amount, item) ->
  <seller> delivery: Delivery where
    delivery.item = item &&
    delivery.recipient = buyer
  then
  <buyer> payment: Payment where
    payment.amount = amount &&
    payment.recipient = seller &&
    payment.item = item

Solution: Pay or return

See the exercise statement.

type Delivery : Event {
  recipient : Agent,
  item : String,
  price : Int
}

type Payment : Event {
  amount : Int,
  recipient : Agent,
  item : String
}

type Return : Event {
  item : String,
  recipient : Agent
}

val inventoryPrice =
\ "Bike" -> 100
| "Hammer" -> 30
| "Saw" -> 40
| _ -> 20000 // Arbitrary large number

contract entrypoint sale = \(buyer, seller, item) ->
  <seller> delivery: Delivery where
    delivery.item = item &&
    delivery.recipient = buyer &&
    delivery.price = inventoryPrice item
  then
  (<buyer> payment: Payment where
    payment.amount = delivery.price &&
    payment.recipient = seller &&
    payment.item = item
  or
  <buyer> return: Return where
    return.item = delivery.item &&
    return.recipient = seller
  )

Solution: Bike and helmet

See the exercise statement.

type Order : Event {
  price : Int,
  recipient : Agent,
  item : String
}

val inventoryPrice =
\ "Bike" -> 100
| "Helmet" -> 30
| "Brakes" -> 20
| _ -> 20000 // Arbitrary large number

contract entrypoint doubleOrder = \(buyer, seller) ->
  <buyer> helmetOrder : Order where
    helmetOrder.item = "Helmet" &&
    helmetOrder.price = inventoryPrice "Helmet" &&
    helmetOrder.recipient = seller
  and
  <buyer> bikeOrder : Order where
    bikeOrder.item = "Bike" &&
    bikeOrder.price = inventoryPrice "Bike" &&
    bikeOrder.recipient = seller

Solution: Late payment

See the exercise statement.

type Delivery : Event {
  recipient : Agent,
  item : String
}

type Payment : Event {
  amount : Int,
  recipient : Agent,
  item : String
}

contract entrypoint sale = \(buyer, seller, amount : Int, item, fine) ->
  let val amountFromDate = \delivery -> \timestamp ->
    if (timestamp <= Instant::addDays 3 delivery) amount
    else amount + fine
  in
  <seller> delivery: Delivery where
    delivery.item = item &&
    delivery.recipient = buyer
  then
  <buyer> payment: Payment where
    payment.amount = amountFromDate delivery.timestamp payment.timestamp &&
    payment.recipient = seller &&
    payment.item = item

Solution: Age-restricted purchase

See the exercise statement.

type ProvideId : Event {}

type Purchase : Event {
  ageRestriction : Bool,
  item : String
}

contract rec loop = \(buyer, shownId) ->
  <buyer> ProvideId then loop (buyer, True)
  or
  <buyer> p : Purchase where
    not (p.ageRestriction) || shownId
    then loop (buyer, shownId)

contract entrypoint restrictedSale = \buyer -> loop (buyer, False)

Solution: Shopping basket

See the exercise statement.

type AddItem : Event{
  item : String
}

type RemoveItem : Event{
  item : String
}

type Checkout : Event {
  total : Int,
  basket : List String
}

val priceList =
 \ "Cabbage" -> 10
 | "Potato" -> 5
 | "Milk" -> 7
 | "Apple" -> 9
 | _ -> 0

val removeFirst = \rm -> \l ->
  let val inner = \el -> \(acc : Tuple (List String) Bool) ->
    if (snd acc) (Cons el (fst acc), True)
    else if (el=rm) (fst acc, True) else (Cons el (fst acc), False) in
  fst (foldr inner ([], False) l)

contract rec multiSale = \buyer -> \basket -> \total ->
  <buyer> order : AddItem where
    priceList order.item > 0
  then multiSale buyer (Cons order.item basket) (total + priceList order.item)
  or
  <buyer> order : RemoveItem where
    Maybe::isSome (List::first (\(item : String) -> item = order.item) basket)
  then multiSale buyer (removeFirst order.item basket) (total - priceList order.item)
  or
  <buyer> checkout : Checkout where
    checkout.basket = basket &&
    checkout.total = total

contract entrypoint sale = \buyer -> multiSale buyer [] 0

Solution: Two-buyer protocol

See the exercise statement.

type ItemSuggesion : Event {
  item : String
}

type SuggestionAccept : Event {}

type PriceEnquiry : Event {
  item : String,
  buyer1 : Agent,
  buyer2 : Agent,
  seller : Agent
}

type ItemPrice : Event {
  item : String,
  price : Int,
  recipient1 : Agent,
  recipient2 : Agent
}

type DeclareShare : Event {
  amount : Int
}

type Delivery : Event {
  item : String,
  recipient1 : Agent,
  recipient2 : Agent
}

type InsufficientFunds : Event {}

contract attemptPurchase = \seller -> \buyer1 -> \buyer2 -> \item -> \price ->
  <buyer1> d1 : DeclareShare then <buyer2> d2 : DeclareShare
  then
  (<seller> d : Delivery where
    d1.amount + d2.amount >= price &&
    d.recipient1 = buyer1 &&
    d.recipient2 = buyer2 &&
    d.item = item
  or
  <seller> InsufficientFunds where
    d1.amount + d2.amount < price)

contract checkPrice = \seller -> \buyer1 -> \buyer2 -> \item ->
  <buyer1> p : PriceEnquiry where
    p.item = item &&
    p.buyer1 = buyer1 &&
    p.buyer2 = buyer2 &&
    p.seller = seller
  then
  <seller> ip : ItemPrice  where
    ip.item = item &&
    ip.recipient1 = buyer1 &&
    ip.recipient2 = buyer2
  then
  attemptPurchase seller buyer1 buyer2 item ip.price

contract rec agreeItem = \seller -> \buyer1 -> \buyer2 ->
  <buyer1> i : ItemSuggesion
  then
  (
    (<buyer2> SuggestionAccept then checkPrice seller buyer1 buyer2 i.item)
    or
    agreeItem seller buyer2 buyer1
  )

contract entrypoint sale = \(seller, buyer1, buyer2) -> agreeItem seller buyer1 buyer2

Solution: Bank account balance

See the exercise statement.

type Deposit : Event { amount : Int }

type Withdraw : Event { amount : Int }

contract rec entrypoint accountOperations = \accountBalance ->
  (<*> d : Deposit where
      d.amount > 0 then accountOperations (accountBalance + d.amount))
  or
  (<*> w : Withdraw where
      w.amount <= accountBalance &&
      w.amount > 0
      then accountOperations (accountBalance - w.amount))

relation deposit(timestamp, amount, cid)
| Deposit{timestamp = timestamp, amount = amount} @ cid

relation withdraw(timestamp, amount, cid)
| Withdraw{timestamp = timestamp, amount = amount} @ cid

val when = \bexp -> \f -> if (bexp) f else id

val report getBalance = \cid ->
  let val deposited = (for (_, amount, c) in deposit do when (c=cid) (\x -> x + amount)) 0
      val withdrawn = (for (_, amount, c) in withdraw do when (c=cid) (\x -> x + amount)) 0
  in
    deposited - withdrawn

Solution: Reimbursement for business travel

See the exercise statement.

val reimburseForTravel =
  \(transport : Transportation) ->
  \(startDate: Instant) ->
  \(endDate : Instant) ->
    let val duration =
      Duration::components (Duration::betweenInstants startDate endDate) in
    let val perDiem = if (duration.day > 1) duration.day*50 else 0 in
    calculateTransportationPrice transport + perDiem

val travelReportForEmployee = \(travelNotices:List TravelNotice) -> \employee ->
  let val relevantNotices =
    List::filter (\(tn:TravelNotice) -> tn.employee = employee) travelNotices in
  (employee,
   foldl
     (\acc -> \(e:TravelNotice) ->
       acc + reimburseForTravel e.transport e.startDate e.endDate)
     0
     relevantNotices)

val isAcceptedNotice = \(notice : TravelNotice) ->
  List::any
    (\(ack:TravelAcknowledgement) ->
      ack.employee = notice.employee &&
      ack.startDate = notice.startDate &&
      ack.endDate = notice.endDate)

val report generateTravelReport =
  \(eventsFromCids : List (List Event)) ->
  \(employees: List Agent) ->
    let val travelAcknowledgements =
      List::mapMaybe
        (\(e:Event) ->
          type ta = e of {TravelAcknowledgement -> Some ta; _ -> None})
        eventsFromCids in
    let val acceptedTravelNotices =
      List::mapMaybe
        (\(e:Event) ->
          type ta = e of {
            TravelNotice ->
              if (isAcceptedNotice ta travelAcknowledgements) Some ta else None;
            _ -> None})
        eventsFromCids in
    List::map (travelReportForEmployee acceptedTravelNotices) employees