Session types in programming languages (2016)

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.

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.