Messaging

[stefjoosten]

Intro

Messaging is required in the design of distributed information systems. In the past, we have had an idea of distributed systems. We called that the "Multi Context Problem". Nevertheless, distributed systems are a very practical target for Ampersand, since most information systems in practice are distributed. As a consequence, software engineers have to spend lots of effort synchronizing their messaging. In the light of cloud architecture, we see the number of services (microservices) growing in practical applications. We should target nothing short of generating multiple services including the messaging that goes with it. This issue is the first step.

Assumptions, desires, requirements.

1. I assume that a Service is capable of acting on its own, has interfaces, and is attached to a data space. (This has a relation with issues Specify a (set of) INTERFACE(s) for resolving violations by users #514, feature: Name spaces #850, What to do with INTERFACEs defined in SystemContext or FormalAmpersand #979, and maybe even Should we support MODULEs? #261.)
2. I assume that a Service can consume and produce streams of messages. (Yet to be elaborated)
3. I perceive a message as an aggregate of pairs in a hierarchical structure.
4. A service that consumes a message must allocate every pair from the message in a unique relation of its own.
5. I don't care about the messaging format. I am using JSON as an example, but I'd be happy with XML, AVRO, or whatever.
6. I want streams to have one type. The type of a stream corresponds to a JSON scheme.
7. I want type checking to be static (i.e. at compile-time). The idea is that a service can consume a stream if it can allocate each pair contained in any message of that stream to precisely one of the relations in the data space attached to the service. If the message has pairs that cannot be allocated, or if it is ambiguous, the entire message is considered ill-typed and should never have occurred in the stream.

This issue attempts to define the semantics of messages.

JSON as an example

Further down this issue, I define a conceptual model for JSON messages, trusting that it is easily implemented in other protocols too.
Here is an example message with a wee bit of code to give the flavour of digging into the message in JavaScript.

var myJSON = '{ "command" : "INSERT", "concept" : "Person", "rel" : [ { "name" : "lastName", "target" : "Text", "atoms" : ["John"] }, { "name" : "age", "target" : "Age", "atoms" : [34] }, { "name" : "address", "target" : "Address", "frames" : [{ "name" : "street", "atoms" : ["Albert Cuyplaan"] }, { "name" : "zipCode", "atoms" : ["1012AB"] }, { "name" : "city", "atoms" : ["Amsterdam"] }] }], "relFlp" : [ { "name" : "member", "source" : "Company", "atoms" : ["ACME"] } }';
var myObj = JSON.parse(myJSON);
console.log(JSON.stringify(myObj.rel[2].frames[2]));

This yields the text {"name":"city","atoms":["Amsterdam"]}

The JSON-message

{ "command" : "INSERT"
, "concept" : "Person"
, "rel" : [ { "name" : "lastName", "target" : "Text", "values" : ["John"] }
          , { "name" : "age", "target" : "Age", "values" : [34] }
          , { "name" : "address"
            , "target" : "Address"
            , "frames" : [ { "name" : "street", "values" : ["Albert Cuyplaan"] }
                         , { "name" : "zipCode", "values" : ["1012AB"] }
                         , { "name" : "city", "values" : ["Amsterdam"] }
                         ]
            }
          ]
, "relFlp" : [ { "name" : "member", "source" : "Company", "values" : ["ACME"] } ]
}

can be consumed by a service that has matching relations, e.g.:

SERVICE "receiver"
   RELATION member[Company*Person]
   RELATION lastName[Person*Text]
   RELATION age[Person*Age]
   REPRESENT Age TYPE INTEGER
   RELATION address[Person*Address]
   RELATION street[Address*StreetName]
   RELATION zipCode[Address*Zip]
   RELATION city[Address*City]
ENDSERVICE

Note that the sources and targets are not complete in the JSON message, but the allocation of pairs to the relations is unambiguous and complete, so this is type-correct.
If a service cannot match one of the relations in the message, Ampersand will block with a type error. The matching process resembles type checking in the current Ampersand: source and target fields in the JSON message may be omitted if the type checker can resolve the type in the relation set of the consuming service.

Haskell

At a certain point, we'll have to tell Haskell how to compile things. This is the data structure I have in mind. (code has NOT been checked):

data Message =
  Message { command : Command
          , concept : Concept
          , rel, relFlp : [Frame]
          }

Each frame represents a single relation.
Frames have a tree structure. Value frames are leaves and Comp frames are nodes.

data Frame =
  Value { name : Identifier
        , source, target : Maybe Concept
        , value : Set Atom
        }
 | Comp { name : Identifier
        , source, target : Maybe Concept
        , rel, relFlp : [Frame]
        }

Proposal

@hanjoosten once urged me to provide FormalAmpersand code with any proposal. That is a terrific idea. I have specified the type checking and (part of) the allocation of frames to relations in the following script. It has been type-checked by Ampersand. I have not run any prototyping experiments with this script yet, so things may change.

CONTEXT "MESSAGING"

PATTERN Atoms -- This pattern is copied from FormalAmpersand
    RELATION name[Concept*Identifier] [UNI,TOT]
    RELATION name[Relation*Identifier] [UNI,TOT]
    RELATION source[Relation*Concept] [UNI,TOT]
    RELATION target[Relation*Concept] [UNI,TOT]

    REPRESENT Identifier TYPE ALPHANUMERIC

    RULE "Identifiability of concepts": name;name~ |- I[Concept]
    VIOLATION (TXT "The name \"", SRC I, TXT "\" is already in use")

    RELATION in[Pair*Relation] [UNI,TOT]
    RELATION pop[Atom*Concept] [UNI,TOT]
    RELATION lAtom[Pair*Atom] [UNI,TOT]
    RELATION rAtom[Pair*Atom] [UNI,TOT]
ENDPATTERN

-- The following stuff is not (yet) in FormalAmpersand
RELATION context[Relation*Service] [UNI,TOT]
RELATION command[Message*Command] [UNI,TOT]
RELATION concept[Message*Concept] [UNI,TOT]
RELATION rel[Message*Frame]
RELATION relFlp[Message*Frame]
RELATION name[Frame*Identifier] [UNI,TOT]
RELATION source[Frame*Concept] [UNI]
RELATION target[Frame*Concept] [UNI]
RELATION value[Frame*Atom]
RELATION sub[Frame*Frame]

PATTERN "Message Type System"
    RELATION matchExists[Relation*Frame]
    MEANING "Registers a match between relation and frame"
    PURPOSE RULE "Definition of matchExists"
    {+ To allow shorter JSON messages, a frame does not have to specify its source and target concepts.
    In case this leads to ambiguity, the compiler must signal a mistake and refrain from generating code.
    +}
    RULE "Definition of matchExists" :
         matchExists = name;name~     /\     -- names must match in all cases
                       source/source  /\     -- if the frame has a source, it must match
                       target/target         -- if the frame has a target, it must match
    MEANING "There is a match between a frame and a relation if their name, source, and target match, insofar the frame has a source or target."
    
    RELATION uniqueMatch[Relation*Frame]
    MEANING "A relation matches to a frame if the type checker says so."
    PURPOSE RULE "Definition of uniqueMatch"
    {+ This relation allows the type checker to determine that there is precisely one match for every frame.
    If not, the compiler must signal a mistake and refrain from generating code.
    +}
    RULE "Definition of uniqueMatch" :
         uniqueMatch = matchExists - -I;matchExists
    MEANING "f is a unique match to r if there exists only one r for every f."
    
    RELATION acceptable[Service*Message]
    MEANING "A service can only consume a message if it is acceptable to that service."
    PURPOSE RULE "Definition of acceptable"
    {+ If a message contains pairs that do not fit into one of the relations of a service or if it fits in multiple relations, that service cannot interpret this message.
    This definition lets the type checker verify that all pairs will find "a home" inside the service.
    +}
    RULE "Definition of acceptable" :
         acceptable = context~;uniqueMatch;(rel\/relFlp)~
    MEANING "A message is acceptable iff every frame in that message can be matched to one relation."
ENDPATTERN

PATTERN "Allocation of atoms"
    PURPOSE RULE rhsAtoms
    {+ This rule describes which pairs are generated from a message.
    The left-hand side atom is to be generated by the exec-engine (TBD)+}
    RULE rhsAtoms : uniqueMatch;(rel~;rel/\I);value |- in~;rAtom
    MEANING "The value of a frame (unflipped) is the right-hand side atom of a pair."
    
    PURPOSE RULE lhsAtoms
    {+ This rule describes which pairs are generated from a message.
    The right-hand side atom is to be generated by the exec-engine (TBD)+}
    RULE lhsAtoms : uniqueMatch;(relFlp~;relFlp/\I);value |- in~;lAtom
    MEANING "The value of a frame (flipped) is the left-hand side atom of a pair."
ENDPATTERN

ENDCONTEXT

Here is the data model:

[RieksJ]

This issue seems to attempt to do 2+ things. First, it postulates the existence of a generic problem (messaging in the context of distributed systems). Then, it tries to make it concrete for Ampersand. The '+' in '2+' refers to the reference to this issue from #1167, of which I fail to see the direct relation.

I suggest we distinguish between a formal, generic approach from any kind of implementation. Artifacts resulting from our generic (conceptual) thinking might result in texts that are like this, and a file in FormalAmpersand may well be added to that (with sufficient comments/references to let readers that didn't write the text understand what's going on).

Then there is the implementation. TNO's SSI-Lab already has quite some practical experiences with prototypes that use APIs for data objects that could well be classified as messages, and with writing code to handle them (both for sending and receiving).

There is a banking application in TNO's SSI-Lab that allows users to to transfer money from one account to another account, provided the accounts are with the same bank. We may want to consider an experiment that would result in a demo that would allow the transfer of money between accounts of different (existing) banks. We could use the experience there to complement the conceptual thinking.

[stefjoosten]

This sounds like a very practical idea: rebuilding the banking application in terms of streams services events and messages in &4 (Ampersand4). This allows us to experiment with the way we see things. @RieksJ do you already have a streams-and-services graph in mind for this particular application?