Relating Functional and Imperative Session Types
Imperative session types provide an imperative interface to session-typed communication. In such an interface, channel references are first-class objects with operations that change the typestate of the channel. Compared to functional session type APIs, the program structure is simpler at the surfac...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/8815/pdf |
| _version_ | 1797268492887523328 |
|---|---|
| author | Hannes Saffrich Peter Thiemann |
| author_facet | Hannes Saffrich Peter Thiemann |
| author_sort | Hannes Saffrich |
| collection | DOAJ |
| description | Imperative session types provide an imperative interface to session-typed
communication. In such an interface, channel references are first-class objects
with operations that change the typestate of the channel. Compared to
functional session type APIs, the program structure is simpler at the surface,
but typestate is required to model the current state of communication
throughout. Following an early work that explored the imperative approach, a
significant body of work on session types has neglected the imperative approach
and opts for a functional approach that uses linear types to manage channel
references soundly. We demonstrate that the functional approach subsumes the
early work on imperative session types by exhibiting a typing and semantics
preserving translation into a system of linear functional session types. We
further show that the untyped backwards translation from the functional to the
imperative calculus is semantics preserving. We restrict the type system of the
functional calculus such that the backwards translation becomes type
preserving. Thus, we precisely capture the difference in expressiveness of the
two calculi and conclude that the lack of expressiveness in the imperative
calculus is largely due to restrictions imposed by its type system. |
| first_indexed | 2024-04-25T01:33:21Z |
| format | Article |
| id | doaj.art-5922d027f1484764b265df41ee52634c |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:21Z |
| publishDate | 2022-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-5922d027f1484764b265df41ee52634c2024-03-08T10:39:30ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-09-01Volume 18, Issue 310.46298/lmcs-18(3:33)20228815Relating Functional and Imperative Session TypesHannes SaffrichPeter ThiemannImperative session types provide an imperative interface to session-typed communication. In such an interface, channel references are first-class objects with operations that change the typestate of the channel. Compared to functional session type APIs, the program structure is simpler at the surface, but typestate is required to model the current state of communication throughout. Following an early work that explored the imperative approach, a significant body of work on session types has neglected the imperative approach and opts for a functional approach that uses linear types to manage channel references soundly. We demonstrate that the functional approach subsumes the early work on imperative session types by exhibiting a typing and semantics preserving translation into a system of linear functional session types. We further show that the untyped backwards translation from the functional to the imperative calculus is semantics preserving. We restrict the type system of the functional calculus such that the backwards translation becomes type preserving. Thus, we precisely capture the difference in expressiveness of the two calculi and conclude that the lack of expressiveness in the imperative calculus is largely due to restrictions imposed by its type system.https://lmcs.episciences.org/8815/pdfcomputer science - programming languagesd.1.3d.3.1f.3.2 |
| spellingShingle | Hannes Saffrich Peter Thiemann Relating Functional and Imperative Session Types Logical Methods in Computer Science computer science - programming languages d.1.3 d.3.1 f.3.2 |
| title | Relating Functional and Imperative Session Types |
| title_full | Relating Functional and Imperative Session Types |
| title_fullStr | Relating Functional and Imperative Session Types |
| title_full_unstemmed | Relating Functional and Imperative Session Types |
| title_short | Relating Functional and Imperative Session Types |
| title_sort | relating functional and imperative session types |
| topic | computer science - programming languages d.1.3 d.3.1 f.3.2 |
| url | https://lmcs.episciences.org/8815/pdf |
| work_keys_str_mv | AT hannessaffrich relatingfunctionalandimperativesessiontypes AT peterthiemann relatingfunctionalandimperativesessiontypes |