Juvix imports

module node_architecture.types.messages;

import prelude open public;
import node_architecture.types.basics open;
import node_architecture.types.identities open;
import node_architecture.types.anoma_message open;

Messages and mailboxes

Types

A message is a piece of data dispatched from one engine, termed the sender, to another engine, referred to as the target. When a message is sent, it is enveloped with additional metadata such as the target address and potentially the sender address, in case the sender wants to be identified. Upon arrival at the target engine, the message is stored in the target engine's mailboxes. These mailboxes are indexed by an identifier that are only unique to their engine. If the target engine has only one mailbox, the mailbox identifier is redundant.

The following types are used to represent these messages and mailboxes.

MailboxID

A mailbox identifier is a natural number used to index mailboxes.

Where do mailbox identifiers come from?

The concept of mailbox identifier is taken from the paper ¹ (see also Mailbox Cluster and ²).

syntax alias MailboxID := Nat;

EngineMessage

A message between engines. Consists of a sender, a target, an optional mailbox identifier, and the message itself.

type EngineMessage : Type :=
  mkEngineMessage {
    sender : EngineID;
    target : EngineID;
    mailbox : Option MailboxID;
    msg : Msg
  };

MessageID

Message identifier. Cryptographic hash of an EngineMessage.

syntax alias MessageID := Hash;

Mailbox S

A mailbox is a container for messages and optionally a mailbox state. The mailbox state could be used to store additional information about the mailbox, such as the priority of the messages in the mailbox.

Where does mailbox state come from?

The mailbox state is related to the capabilities of mailboxes of the paper ¹. In particular, at any given point in time, a mailbox will have a capability for receiving messages (in later versions of the specs). As mailbox state can be useful in general, we already have it now.

type Mailbox (MailboxStateType : Type) : Type :=
  mkMailbox {
    messages : List EngineMessage;
    mailboxState : Option MailboxStateType
  };

Timer H

type Timer (HandleType : Type) : Type :=
  mkTimer {
    time : Time;
    handle : HandleType
  };

Trigger H

type Trigger (HandleType : Type) :=
  | MessageArrived {msg : EngineMessage}
  | Elapsed {timers : List (Timer HandleType)};

• Extract the actual message from a trigger in case it has one:

  getMessageFromTrigger : {H : Type} -> Trigger H -> Option Msg
    | MessageArrived@{msg} := some (EngineMessage.msg msg)
    | Elapsed@{} := none;

• Get the message sender from a trigger:

  getSenderFromTrigger : {H : Type} -> Trigger H -> Option EngineID
    | MessageArrived@{msg} := some (EngineMessage.sender msg)
    | Elapsed@{} := none;

• Get the target destination from a trigger:

  getTargetFromTrigger : {H : Type} -> Trigger H -> Option EngineID
    | MessageArrived@{msg} := some (EngineMessage.target msg)
    | Elapsed@{} := none;

TimestampedTrigger H

type TimestampedTrigger (HandleType : Type) :=
  mkTimestampedTrigger {
    time : Time;
    trigger : Trigger HandleType
  };

• Get the actual message from a TimestampedTrigger:

  getMessageFromTimestampedTrigger {H} (tr : TimestampedTrigger H) : Option Msg :=
    getMessageFromTrigger (TimestampedTrigger.trigger tr);

• Get the sender from a TimestampedTrigger:

  getSenderFromTimestampedTrigger
    {H} (tr : TimestampedTrigger H) : Option EngineID :=
    getSenderFromTrigger (TimestampedTrigger.trigger tr);

• Get the target from a TImestampedTrigger:

  getTargetFromTimestampedTrigger
    {H} (tr : TimestampedTrigger H) : Option EngineID :=
    getTargetFromTrigger (TimestampedTrigger.trigger tr);

---

1. Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder. Special delivery: programming with mailbox types. Proceedings of the ACM on Programming Languages, 7(ICFP):78–107, August 2023. URL: http://dx.doi.org/10.1145/3607832, doi:10.1145/3607832. ↩↩

2. Shams M. Imam and Vivek Sarkar. Selectors: actors with multiple guarded mailboxes. AGERE! '14: Proceedings of the 4th International Workshop on Programming based on Actors Agents and Decentralized Control, October 2014. URL: http://dx.doi.org/10.1145/2687357.2687360, doi:10.1145/2687357.2687360. ↩