WG211/M18 Kiselyov - Revision history

Ups at 13:27, 21 May 2018

2018-05-21T13:27:47Z

← Older revision		Revision as of 15:27, 21 May 2018
Line 13:		Line 13:
	languages. We need not just monads but parameterized monads as well as		languages. We need not just monads but parameterized monads as well as
	type functions and linear types. Realizing session types in OCaml		type functions and linear types. Realizing session types in OCaml
	requires inordinary cleverness~-- meaning the implementation and the		requires inordinary cleverness - meaning the implementation and the
	error messages are very hard to understand. One is constantly reminded		error messages are very hard to understand. One is constantly reminded
	of template metaprogramming in C++.		of template metaprogramming in C++.

Ups at 13:27, 21 May 2018

2018-05-21T13:27:30Z

← Older revision		Revision as of 15:27, 21 May 2018
Line 4:		Line 4:
	approximate communication among computations. Session types are		approximate communication among computations. Session types are
	appealing because they can be inferred/checked statically, and because		appealing because they can be inferred/checked statically, and because
	well--session-typed programs ``do not go wrong'': the computations do		well--session-typed programs "do not go wrong": the computations do
	not deadlock, do not send data or commands their party is not prepared		not deadlock, do not send data or commands their party is not prepared
	to handle, do not try to use closed or delegated away channels.		to handle, do not try to use closed or delegated away channels.

Ups: Created page with "Session types without sophistry by Oleg Kiselyov, joint work with Keigo Imai of Gifu University Whereas ordinary types approximate the results, session types approximate comm..."

2018-05-21T13:27:11Z

Created page with "Session types without sophistry by Oleg Kiselyov, joint work with Keigo Imai of Gifu University Whereas ordinary types approximate the results, session types approximate comm..."

New page

Session types without sophistry by Oleg Kiselyov, joint work with Keigo Imai of Gifu University

Whereas ordinary types approximate the results, session types
approximate communication among computations. Session types are
appealing because they can be inferred/checked statically, and because
well--session-typed programs ``do not go wrong'': the computations do
not deadlock, do not send data or commands their party is not prepared
to handle, do not try to use closed or delegated away channels.

Session types are a form of typestate: they describe not only what is
communicated now but also what should or could be communicated
next. Therefore, they are non-trivial to realize in conventional
languages. We need not just monads but parameterized monads as well as
type functions and linear types. Realizing session types in OCaml
requires inordinary cleverness~-- meaning the implementation and the
error messages are very hard to understand. One is constantly reminded
of template metaprogramming in C++.

We present the ongoing work exploring a very different approach to
session typing: programming the inference and checking in the
appropriate language (OCaml) and still obtaining the static assurances
about communicating programs. We can emit detailed error messages
customized at will, and use the ordinary debugger. The key idea is
staging: ordinary run-time checks in the generator are `type-checks'
from the point of view of the generated program. Fancy types are
replaced with boring generator terms. (In type-checking, like in
investing, exciting is ruinous.) Our library of binary session types
supports multiple communication channels, internal and external
choices, and channel delegation.