Anomian

Preface¶

As in the Little Typer book, we explore some aspects of the Anoma model through a dialogue that presents the notions considered in the specification. There are two participants in this dialogue: the student, Jordan, and Anomian, the modeller. When Anomian speaks, it is in the form of a quote. Otherwise, Jordan speaks.

Hi, I am Anomian.

The goal of this dialogue is to illustrate what the Anoma system is about and how to model it. For the sake of concreteness, we present a few Juvix code snippets that are intended to clarify the model and help resolve potential ambiguities. Most of the data types are enumerations and inductive types. The quotes alone should convey the main idea. The Jordan interjections are to confirm, ask questions, and reiterate the concepts.

Last, but not least, we have not only code snippets, but we fully embrace literate programming. This comes at the inconvenience of some lines of boilerplate here, but it can safely be skipped on a first reading.

module anomian;

import arch.node.types.basics open public;
import arch.node.types.identities open;
import arch.node.types.messages open hiding {EngineMsg; mkEngineMsg; Mailbox};

Chapter 1: The core players of the game¶

At the core of the Anoma model, we find engines. They do most of the heavy lifting.

So, what do you mean by an engine?

type EngineStatus :=
  | Running
  | Dead
  | Suspended;

Dynamic entity? What is dynamic about it?

You and I are not the same person we were yesterday because some events happened to us. For engines, a typical event is the reception of an engine-message and as a reaction to message reception, their state may change. This ability to change their state is what makes them dynamic. However, notice that this change of internal state is optional. We call those engines that never change their state stateless engines.

Huh, so, an engine has its own state, and that state can change by reacting to messages that are sent to it. Easy.

It's like when we receive a letter from the tax office. Once we read the letter and understand it, we know that we have to pay taxes and eventually do so. That letter may "change" us, some money may be gone.

But wait, who really sends those messages actually?

Any engine, including the same engine which receives the message. For example, an engine could remind itself to do something by sending a message to itself.

I see, and the messages can be in different languages, right? I read English but not French. How are engines able to communicate with each other? Do they all speak the same language?

Each engine has its own message interface, indicating the language(s) they speak. This message interface defines the format and content of the messages it can comprehend and process.

syntax alias EnglishPayload := String;

syntax alias FrenchPayload := String;

syntax alias SpanishPayload := String;

type AnomianMsgInterface :=
  | AnomianMsgEnglish@{
      msg : EnglishPayload;
    }
  | AnomianMsgFrench@{
      msg : FrenchPayload;
    };

type JordanMsgInterface :=
  | JordanMsgEnglish@{
      msg : EnglishPayload;
    }
  | JordanMsgSpanish@{
      msg : SpanishPayload;
    };

helloAnomian : AnomianMsgInterface :=
  AnomianMsgEnglish@{
    msg := "Hello!";
  };

The model defines all the message interfaces defined by engines.

type MsgInterface :=
  | MsgAnomian AnomianMsgInterface
  | MsgJordan JordanMsgInterface;

To see the full list of message interfaces in the current model, check out the sum type Msg in Anoma Message.

Chapter 2: Communication patterns¶

Now that we understand engines and their message interfaces, let's talk about how they communicate with each other or better said, what patterns of communication are there.

I can send a message to you, Anomian, either to expect a response or simply to inform you that I'm alive. What else can I do?

syntax alias Timeout := Nat;

type CommunicationPattern :=
  | FireAndForget
  | RequestReply@{
      timeout : Option Timeout;
    }
  | PubSub;

We can consider three patterns of communication. The pattern FireAndForget allows us to communicate asynchronously. One can send a message and not expect any response like notifications on your phone. However, if you need a response or result and can wait for it, we can use the RequestReply pattern. That is the pattern that every synchronous communication uses implicitly. And finally, the PubSub pattern (pub/sub for short) that allows us to communicate asynchronously and without a response, broadcasting messages to multiple engines.

type EngineMsgKind :=
  | Request
  | Reply
  | Notify;

Chapter 3: Engine configurations¶

Anomian, you mentioned that engines have an internal state, a message interface, and specific communication patterns. Are there any other characteristics that define an engine? And what about us, are we also engines? For instance, humans have attributes such as name, age, and parents. Do engines have similar attributes?

type EngineCfg C :=
  mkEngineCfg@{
    parent : Option EngineID;
    name : EngineName;
    node : NodeID;
    cfg : C;
  };

As we say the engine configuration is immutable by design. This means that once an engine is created, attributes such as the name of the engine cannot be changed. If you want to change the name of an engine, you have to create a new engine with the new name.

Tell me one thing about the parents of engines. Do they always know who their parent is? I don't know who is my father, actually.

axiom localhost : NodeID;

simpleConfig : EngineCfg Unit :=
  mkEngineCfg@{
    parent := none;
    name := "Anomian";
    node := localhost;
    cfg := unit;
  };

So, we have one way to identify engines: by their name and their node if we know where it runs.

EngineID : Type := Pair (Option NodeID) EngineName;

Okay, I guess that we can nevertheless start thinking about identifiers already.

JordanID : EngineID := mkPair (some localhost) "Jordan9121";

AnomianID : EngineID := mkPair (some localhost) "Anomian184";

With engine identifiers (of type EngineID), we can define engine messages. These messages serve as events for engines, sent to them by some other engine.

type EngineMsg M :=
  mkEngineMsg@{
    sender : EngineID;
    target : EngineID;
    mailbox : Option MailboxID;
    pattern : CommunicationPattern;
    kind : EngineMsgKind;
    msg : M;
  };

jordanToAnomian : EngineMsg MsgInterface :=
  mkEngineMsg@{
    sender := JordanID;
    target := AnomianID;
    mailbox := some 1;
    pattern :=
      RequestReply@{
        timeout := none;
      };
    kind := Request;
    msg :=
      MsgAnomian
        AnomianMsgEnglish@{
          msg := "What is the meaning of life?";
        };
  };

anomianToJordan : EngineMsg MsgInterface :=
  mkEngineMsg@{
    sender := AnomianID;
    target := JordanID;
    mailbox := some 1;
    pattern := FireAndForget;
    kind := Reply;
    msg :=
      MsgJordan
        JordanMsgEnglish@{
          msg := "The meaning of life is 42.";
        };
  };

But how can I send it? Do I have to go to the post office?

Chapter 4: Mailboxes for anyone¶

Messages are sent to the engine's mailbox.

type Mailbox S M :=
  mkMailbox@{
    messages : List (EngineMsg M);
    mailboxState : Option S;
  };

MailboxCluster (S M : Type) : Type := Map MailboxID (Mailbox S M);

Why bother with the mailbox cluster? One mailbox is enough, right?

While a single mailbox would suffice for basic functionality, multiple mailboxes provide valuable message organisation capabilities.

That sounds like how my email works. It is a cluster of mailboxes, and in principle, I have one big mailbox, but truly I can see it as having multiple mailboxes, one for each folder, such as promotions, important, family, etc.

graph LR
    MailboxCluster["Jordan's Mailbox Cluster"] --> Mailbox1
    MailboxCluster --> Mailbox2
    MailboxCluster --> Mailbox3

    subgraph Mailbox1["Mailbox#1 : 'Urgent'"]
        Queue1("Queue of Messages")
        Data1("Mailbox state")
    end

    subgraph Mailbox2["Mailbox #2 : 'Promotions'"]
        Queue2("Queue of Messages")
        Data2("Mailbox state")
    end

    subgraph Mailbox3["Mailbox #3 : 'Family'"]
        Queue3("Queue of Messages")
        Data3("Mailbox state")
    end

You have not answered yet how mail is actually sent.

Well, imagine for a second that the communication process is magically handled by one mailelf that delivers messages to the engines. When a message is sent to an engine, the mailelf takes the message from the sender and puts it in the engine's mailbox. In other words, for the moment, it suffices to assume that all messages are delivered eventually.

Chapter 5: Context of execution¶

This is quite a fancy setup for sending messages, but how do engines "actually" get things done?!

I mean, we've discussed that engines have certain attributes: an identifier, a message interface, and a configuration that includes details like a parent, a name, and a virtual location where the engine runs. So, maybe a better question: how do engines actually run?

AddressBook : Type := Set EngineName;

type EngineEnv S Msg :=
  mkEngineEnv@{
    state : S;
    mailbox : MailboxCluster S Msg;
    acq : AddressBook;
  };

Note that engine environments do not encompass the engine's configuration, although they could. Instead, engine configurations are accessible separately from the engine environments. This separation promotes modularity.

Chapter 6: What engines can do¶

axiom ReturnSomething : Type;

Handler (M S : Type) : Type := M -> EngineEnv S M -> ReturnSomething;

The computational aspect of an engine is what we refer to as its behaviour, and it is correct to think of it as a function that takes in a message and the engine's environment. However, the return type of this function cannot be anything: the type what an engine can produce is part of the model of engines, and it is fixed for each engine.

What exactly can an engine do if it's not just the same message passing we already know?

syntax alias TimeTrigger := Nat;

type Effect S E M :=
  | SendMsg@{
      msg : EngineMsg M;
    }
  | UpdateState@{
      state : S;
    }
  | SpawnEngine@{
      engine : E;
    }
  | Chain@{
      effects : List (Effect S E M);
    }
  | Schedule@{
      trigger : TimeTrigger;
      action : Effect S E M;
    };

Based on the type for possible effects,⁴ the only new aspect for me about engines is that they record the need for actions to happen at a later time. We already have covered that engines have a parent; the SpawnEngine effect is the other side of the same coin. The rest remains the same as before.

Our actions are restricted by certain pre-conditions, some inherent from the environment. We only take action if the conditions are met. For engines, these conditions are expressed as guards.⁵

I got it. This mirrors our situation perfectly. Taking the tax office example: when I receive a notice to pay taxes, I first assess whether I have the funds available. If I do, I take action to pay; otherwise, I might postpone the payment.

Guard (S M C R : Type) : Type :=
  EngineMsg M -> EngineEnv S M -> EngineCfg C -> Option R;

isSatisfied
  {S M C R}
  (guard : Guard S M C R)
  (msg : EngineMsg M)
  (env : EngineEnv S M)
  (cfg : EngineCfg C)
  : Bool :=
  case guard msg env cfg of
    | none := false
    | some _ := true;

Wait! I see an issue. What if the engine has several guards, and they are all satisfied?

type GuardStrategy :=
  | FirstGuard
  | LastGuard
  | OneGuard
  | UniqueGuard
  | AllGuards;

type GuardEval S M C R :=
  mkGuardEval@{
    guards : List (Guard S M C R);
    strategy : GuardStrategy;
  };

Ah, I see! So the guards act as the rules the engine follows, and the actions are the procedures executed when those rules are satisfied, and with the possible outcomes of the guards.

EngineBehaviour (S E M C R : Type) : Type := GuardEval S M C R -> Effect S E M;

type Engine (S E M C R : Type) :=
  mkEngine@{
    status : EngineStatus;
    cfg : EngineCfg C;
    state : EngineEnv S M;
    behavior : EngineBehaviour S E M C R;
  };

Chapter 7: We have engines, and now, what?¶

I think I am getting the hang of it. But what's next?

Yes, I think we have made a good start. However, we have to fill in the blanks and put everything together in a single system. In the upcoming chapters, how the system looks like in more detail and how ensure the following properties for engine-to-engine communication:

• Message delivery: All messages are eventually delivered
• Engine isolation: Each engine maintains independent state
• Type safety: All communication follows defined message interfaces
• Configuration immutability: Engine configurations cannot be modified after creation

A quick glossary of the terms we have seen so far.

• EngineStatus: Represents the possible states an engine can be in—Running, Dead, or Suspended.

• CommunicationPattern: Enumerates the types of communication patterns available, such as FireAndForget, RequestReply with an optional timeout, and PubSub.

• EngineMsgKind: Categorizes messages into Request, Reply, or Notify.

• EngineID: A composite identifier for engines, consisting of a nodeId and a name.

• MessageInterface: Defines the interface for messages specific to different engines (AnomianMsgInterface, JordanMsgInterface) and aggregates them into a general MsgInterface.

• EngineCfg: An immutable configuration for an engine, including optional parent information, engine name, node ID, and a generic configuration type c.

• Mailbox and MailboxCluster: Structure for message queues (Mailbox) and a collection of mailboxes (MailboxCluster) indexed by MailboxID.

• EngineEnv: The execution context of an engine, comprising its state, mailbox cluster, and an address book of known engines.

• Guard and GuardStrategy: Mechanisms to evaluate whether certain conditions are met (Guard) and strategies to handle multiple satisfied guards (GuardStrategy).

• Effect: The possible outcomes or actions an engine can perform, such as sending messages, updating state, spawning new engines, chaining effects, or scheduling future actions.

• EngineBehaviour: A function defining how an engine responds to evaluated guards and decides on an effect.

• Engine: The core representation of an engine, combining its status, configuration, state, and behaviour.

• EngineMsg: Structure of messages exchanged between engines, including sender and target identifiers, mailbox, communication pattern, message kind, and the message content itself.