First Protocol Specification - Session Types Article

[CMCDragonkai]

Write an article about session type development. Although this issue will also address some feedback about the most recent research and experiments.

[CMCDragonkai]

@olligobber Just a few questions.

In what case can a Map be not valid?

https://github.com/MatrixAI/Architect/blob/299e6820730ab0329b992996daa5257f6521ad91/ProtocolResearch/SessionTypesDemo/src/SessionType.hs#L41

More generally what's the purpose of checking the validity of the session type? What's an example incorrect construction?

With regards to subtyping:

https://github.com/MatrixAI/Architect/blob/299e6820730ab0329b992996daa5257f6521ad91/ProtocolResearch/SessionTypesDemo/src/SessionType.hs#L59-L67

What about the types that are being offered and chosen? If a service offers an object { key1: string, key2 : int }, but the consumer only requires an object {key1: string}, these 2 parties are compatible because the consumer only needs one of them. Check out row polymorphism for more about this. Did the article on contravariance and covariance help as well?

I think it would make it easier to understand if you also give example specification as well as the code implementation. Or even typing rules.

https://github.com/MatrixAI/Architect/blob/299e6820730ab0329b992996daa5257f6521ad91/ProtocolResearch/SessionTypesDemo/src/SessionType.hs#L69-L76

How does the dual interact with subtyping? What is the relationship between the subtyping in the demo and the more general subtyping theory?

https://github.com/MatrixAI/Architect/blob/299e6820730ab0329b992996daa5257f6521ad91/ProtocolResearch/SessionTypesDemo/src/SessionType.hs#L86-L95

This appears to work nicely for union composition, where it then allows one to create the gateway microservice pattern.

As a general feedback on the code, I would put the union' and other func' as where clauses since they should be encapsulated by the external API.

https://github.com/MatrixAI/Architect/blob/299e6820730ab0329b992996daa5257f6521ad91/ProtocolResearch/SessionTypesDemo/src/SessionType.hs#L97-L115

What does ambiguity here mean? Does it mean it chooses randomly, or just chooses the first one. That the first set that contains the key takes precedence. Also in that case, we should not call a union, but a merge operation that has deterministic behaviour. I'm not sure if that really makes sense in the context of Automatons though.

https://github.com/MatrixAI/Architect/blob/299e6820730ab0329b992996daa5257f6521ad91/ProtocolResearch/SessionTypesDemo/src/SessionType.hs#L117-L122

Please explain this limited ambiguity with some examples.

[CMCDragonkai]

Since Send and Recv are recursive, the base case is always Wait and Kill. Is Wait equivalent to a networked service just performing event-driven listen?

[CMCDragonkai]

I need to go over the tests with you @olligobber, there are parts which are hard to understand. Either restructuring, comments, or more deliberate names would help here.

[olligobber]

A Map can be invalid, see https://hackage.haskell.org/package/containers-0.5.11.0/docs/Data-Map-Strict.html,

valid (fromAscList [(3,"b"), (5,"a")]) == True
valid (fromAscList [(5,"a"), (3,"b")]) == False

Checking this does not affect the time complexity of the operation, so I left it in. Invalid session types are ones where the underlying data structures have been made invalid somehow, or that present invalid choices, such as an offer with no choices, or a choose that chooses nothing.

Duality inverts subtyping, as seen in the following property: https://github.com/MatrixAI/Architect/blob/165d409eae8a66fd3ef1c2dc91615b52bffcb7d9/ProtocolResearch/SessionTypesDemo/test/Spec.hs#L153

I've considered the various ways of unioning two session types, which we go with depends on how complicated our network combinators should be.

• With strictUnion, the combinator would be able to look at the first request and forward it to the appropriate automaton.
• With union, it may not be obvious until late in the communication which automaton the communication must be with, so the combinator will have to choose an arbitrary automaton, and when it reaches a point where that automaton cannot handle the incoming message, it would have to switch to another automaton, replay the entire conversation to the new automaton (hoping that the responses it receives are identical), and continue from there. There are cases where this is impossible to achieve
• With smartUnion, the combinator would be able to look at the first few requests and forward it to one of the appropriate automatons before any data is communicated. The union functions will need work, it depends on how we end up implementing the protocol specification and combinators.

Wait and Kill represent "wait for them to end communication" and "end communication now" respectively. Sometimes they are merged into a single Session Type called End, which might actually be more appropriate.

We do need more documentation including comments and examples.

[olligobber]

Draft of the article is ready to be proofread.

[CMCDragonkai]

The article is now published. https://matrix.ai/2018/07/14/session-types/

Note that use nohighlight as the markdown code annotation to prevent automatic (incorrect) syntax highlighting.

[CMCDragonkai]

Note that the idea of using rec for fixed points came from Nix. But Nix uses rec for attribute sets, and here we are using rec t as a domain specific way of delimiting a recursive point in the type declaration. See this http://r6.ca/blog/20140422T142911Z.html for more information.