Add Session types

Search Terms

session types, mutable types, stateful types

Suggestion

Session Types are used to describe stateful protocol (aka Sessions). Static typing can prevent mistakes made by calling methods out of order. This can be espacially helpful for providing public API's to guide users.

A simple example would be an API which requires authentification: At first, you would need to call a login-Method, after that you are allowed to call any other method, for example getPrivateData.

Session Types are still a somewhat obscure feature in type systems. To my knowledge no major programming language has support for it by default. Therefore Typescript could be among the innovators ;). There is a lot of academic material out there, but no material for the general public i'm afraid. This seems to be a fairly readable introduction: http://www.simonjf.com/2016/05/28/session-type-implementations.html

Use Cases

The most common use case for session types are stateful connection protocols (aka Sessions). For example a class handling file access, which would ensure that files are open()-ed before you write to it

Currently these use cases are covered either by runtime checks or by the design of a "fluent api". However both solutions are not sufficient:

Runtime checks are equivalent to dynamic typing and may be missed when refactoring. They cannot be statically analyzed to provide IDE-suppport.

With fluent Api, you loose a lot of general language abilities like return values, control flow and so on. If the flunt api is implemented "uni-typed", there is no type checking at all and type checking has to be done by RuntimeExceptions.

When implementing a "typed fluent API" (i.E return different objects than this), it may get wasteful as many objects are created for no good reason and also the code gets rather complicated.

Examples

modelling the game of poker (texas hold 'em):

const pokerGame = new PokerGame();
await pokerGame.receiveCards();
const cards = pokerGame.getMyCards();

if(ai.iWantToBet()){
    await pokerGame.bet() // may only be called once and is exclusive with .pass(), .fold()
}else if(ai.iWantToPass()){
    await pokerGame.pass() // may only be called once and is exclusive with .bet(), .fold()
}else if(ai.iWantToFold()){
   await pokerGame.fold() // may only be called once and is exclusive with .bet(), .pass()
}

await pokerGame.nextRound() // only method which is allowed to be called by now.

const publicCards = pokerGame.getPublicCards(); // can only be called after nextRound() has been called

// and so on...

As syntax, we could use the type assertion syntax (x as Type), as this would essentially the same as setting the type of this inside the function call.

Possibly one may extend the syntax to set types of the arguments as well, but I'll leave that open for discussion..

interface RoundFinished {
    nextRound();
}

interface RoundStart {
    bet(): this as RoundFinished;
    pass(): this as RoundFinished;
    fold(): this as GameFinished;
}

interface GameFinished {
    getResults();
} 

class PokerGame {
    bet(): this as RoundFinished  {
        // code
       // after the function exits, "this" is now typechecked as "RoundFinished" (without having to use "fluent API") 
    }
    nextRound(): this as RoundStart {
        // and so on..
    }
}

Checklist

My suggestion meets these guidelines:

• This wouldn't be a breaking change in existing TypeScript/JavaScript code
• This wouldn't change the runtime behavior of existing JavaScript code
• This could be implemented without emitting different JS based on the types of the expressions
• This isn't a runtime feature (e.g. library functionality, non-ECMAScript syntax with JavaScript output, etc.)
• This feature would agree with the rest of TypeScript's Design Goals.

Es werden keine Quelldateien, Einstiegspunkte oder Tests genannt. Beginne mit der Durchsicht der vorgeschlagenen Beispiele für Session-Typen und der verlinkten Einführung und vergleiche die Idee anschließend mit den Designzielen von TypeScript; für den Abschluss wären eine festgelegte Syntax und ein festgelegtes Design für die Typprüfung vor der Implementierung erforderlich.