microsoft / TypeScript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
https://www.typescriptlang.org
Apache License 2.0
100.19k stars 12.38k forks source link

Add Session types #41339

Open Trias opened 3 years ago

Trias commented 3 years ago

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:

RyanCavanaugh commented 3 years ago

This is actually pretty much supported already using assertion syntax.

interface RoundFinished {
    nextRound(): void;
}

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

interface GameFinished {
    getResults(): void;
} 

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

const g: PokerGame = new PokerGame();
g.bet();
// Not legal if moved above prior line
g.nextRound();
jcalz commented 2 years ago

Assertion methods only narrow, right? You can't use them to widen or otherwise modify types. So any "stateful type" that has obj.prop start off as a string but end up as a number after a call to obj.turnPropIntoANumber() is not something we can model in TS.

mharj commented 1 month ago

I think smallest change would be just allow combination of asserts this and return type for function/method like "(asserts this is AnotherType) & ReturnType".