6 ms·

Session types in programming languages (2016)

rurban 8y ago
Since then Pony came along: Primitive, Static No external Scribble-like protocol needed, builtin into the compiler. Actor-based.
hurricaneSlider 8y ago
Didn't write this but thought it was interesting as it seems to address pain points I've felt when building out a typed actor system (requirements for adapters, etc)
wcrichton 8y ago
For those who want to learn more, I wrote an extended, accessible introduction to session types (predicated on a little knowledge about PL metalanguage syntax, e.g. BNF grammar) here: http://cs242.stanford.edu/lectures/07-2-session-types.html http://cs242.stanford.edu/lectures/07-2-session-types.html It also includes a walkthrough of a session types implementation in Rust.
- vikiomega9 8y ago
  Noob question, I was not able to follow what the advantages of using session types were. What am I missing? Follow up, 1. How would session types differ from contract based testing? 2. Is there a notion of versioning on the types? 3. If there were better type support (ie. Well defined sum and product types) for wire protocols (protobufs etc) would that solve any of the problems session types might?
  - uryga 8y ago
    as an example, session types are useful if you want to give precise types to coroutines that yield nontrivially (i.e. aren't basically iterators). consider this (slightly contrived) Python example of a coroutine yields two intermediate values, a result, and finishes: from typing import Generator # Generator[YieldType, SendType, ReturnType] # https://docs.python.org/3/library/typing.html#typing.Generator def inc_mul(a, b) -> Generator[int, None, None]: "Computes (a+1) * (b+1), yields the intermediate results" a1 = a+1 yield a1 b1 = b+1 yield b1 yield a1*b1 proc = inc_mul(1, 3) # create the "process" a1 = proc.send(None) # 2 b1 = proc.send(None) # 4 ab = proc.send(None) # 8 proc.send(None) # end. raises StopIteration(None) Our signature inc_mul(a: int, b: int) -> Generator[int, None, int] doesn't really capture "yields two intermediate ints, a result int, and finishes" – it only says that it'll yield some unspecified number of ints. but using session types we can describe the interaction precisely! it'd look something like inc_mul(a:int, b:int) -> Process[ ?None => !int => ?None => !int => ?None => !int => ?None ] the notation is based on the article – `?T` means "accepts a T", `!T` means "yields a T`, `=>` means "and then". the type is a bit noisy because of all the dummy None's needed to push the coroutine along. we could also extend our coroutine to, after yielding the two intermediate values, accept a float (power) and yield `(a1 × b1) ^ power` as the result (this would let the user determine the exponent she wants based on the intermediate results, if she needed that for some reason). the type would then change to inc_mul(a:int, b:int) -> Process[ ?None => !int => ?None => !int => ?float => !float => ?None ] we can approximate this as `Generator[Union[int, float], Union[None, float], None]` but that doesn't capture the order/number of the yields/sends.
zozbot123 8y ago
Latest version of this post [2017] is found at http://groups.inf.ed.ac.uk/abcd/session-implementations.html http://groups.inf.ed.ac.uk/abcd/session-implementations.html
- hurricaneSlider 8y ago
  Thanks zozbot123
  - zozbot123 8y ago
    You're welcome! Besides, y'know, you could have read the post before submitting it, and it would have told you the exact same thing? It's not rocket surgery.
    - hurricaneSlider 8y ago
      Haha actually did read it. But eyes must've skipped over the header.

Since then Pony came along: Primitive, Static No external Scribble-like protocol needed, builtin into the compiler. Actor-based.

hurricaneSlider 8y ago

Didn't write this but thought it was interesting as it seems to address pain points I've felt when building out a typed actor system (requirements for adapters, etc)

wcrichton 8y ago

For those who want to learn more, I wrote an extended, accessible introduction to session types (predicated on a little knowledge about PL metalanguage syntax, e.g. BNF grammar) here: http://cs242.stanford.edu/lectures/07-2-session-types.html http://cs242.stanford.edu/lectures/07-2-session-types.html It also includes a walkthrough of a session types implementation in Rust.

vikiomega9 8y ago
Noob question, I was not able to follow what the advantages of using session types were. What am I missing? Follow up, 1. How would session types differ from contract based testing? 2. Is there a notion of versioning on the types? 3. If there were better type support (ie. Well defined sum and product types) for wire protocols (protobufs etc) would that solve any of the problems session types might?
- uryga 8y ago
  as an example, session types are useful if you want to give precise types to coroutines that yield nontrivially (i.e. aren't basically iterators). consider this (slightly contrived) Python example of a coroutine yields two intermediate values, a result, and finishes: from typing import Generator # Generator[YieldType, SendType, ReturnType] # https://docs.python.org/3/library/typing.html#typing.Generator def inc_mul(a, b) -> Generator[int, None, None]: "Computes (a+1) * (b+1), yields the intermediate results" a1 = a+1 yield a1 b1 = b+1 yield b1 yield a1*b1 proc = inc_mul(1, 3) # create the "process" a1 = proc.send(None) # 2 b1 = proc.send(None) # 4 ab = proc.send(None) # 8 proc.send(None) # end. raises StopIteration(None) Our signature inc_mul(a: int, b: int) -> Generator[int, None, int] doesn't really capture "yields two intermediate ints, a result int, and finishes" – it only says that it'll yield some unspecified number of ints. but using session types we can describe the interaction precisely! it'd look something like inc_mul(a:int, b:int) -> Process[ ?None => !int => ?None => !int => ?None => !int => ?None ] the notation is based on the article – `?T` means "accepts a T", `!T` means "yields a T`, `=>` means "and then". the type is a bit noisy because of all the dummy None's needed to push the coroutine along. we could also extend our coroutine to, after yielding the two intermediate values, accept a float (power) and yield `(a1 × b1) ^ power` as the result (this would let the user determine the exponent she wants based on the intermediate results, if she needed that for some reason). the type would then change to inc_mul(a:int, b:int) -> Process[ ?None => !int => ?None => !int => ?float => !float => ?None ] we can approximate this as `Generator[Union[int, float], Union[None, float], None]` but that doesn't capture the order/number of the yields/sends.

zozbot123 8y ago

Latest version of this post [2017] is found at http://groups.inf.ed.ac.uk/abcd/session-implementations.html http://groups.inf.ed.ac.uk/abcd/session-implementations.html

hurricaneSlider 8y ago
Thanks zozbot123
- zozbot123 8y ago
  You're welcome! Besides, y'know, you could have read the post before submitting it, and it would have told you the exact same thing? It's not rocket surgery.
  - hurricaneSlider 8y ago
    Haha actually did read it. But eyes must've skipped over the header.