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
}

template 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

template 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" -> 50
| "Saw" -> 40
| _ -> 20000 // Arbitrary large number

template 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
}

template Sale(buyer, seller, amount : Int, item, fine) =
  let val amountFromDate = \delivery -> \timestamp ->
    if (timestamp <= DateTime::addDays delivery 3) 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
}

template rec Loop (buyer, shownId) =
  <buyer> ProvideId then Loop (buyer, True)
  or
  <buyer> p : Purchase where
    not (p.ageRestriction) || shownId
    then Loop(buyer, shownId)

template 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)

template 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
    List::String::equals checkout.basket basket &&
    checkout.total = total

template 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 {}

template 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)

template 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)

template rec AgreeItem(seller, buyer1, buyer2) =
  <buyer1> i : ItemSuggesion
  then
  ((<buyer2> SuggestionAccept then CheckPrice(seller, buyer1, buyer2, i.item))
  or
  AgreeItem(seller, buyer2, buyer1))

template 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 }

template rec 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))

Solution: Reimbursement for business travel

See the exercise statement.

val reimburseForTravel =
  \(transport : Transportation) ->
  \(startDate: DateTime) ->
  \(endDate : DateTime) ->
    let val duration =
      Duration::components (Duration::between 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 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