Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Law and Order for Typestate with Borrowing

Hannes Saffrich, Yuki Nishida, Peter Thiemann

TL;DR

This work proposes a new, transition-oriented foundation for typestate in the setting of impure functional programming, and gives an algorithmic version of the type system and proves syntactic type soundness with respect to a resource-instrumented semantics.

Abstract

Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implications. Yet, we support a flexible notion of borrowing in the presence of typestate. Our core calculus comes with a notion of resource types indexed by an ordered partial monoid that models abstract state transitions. We prove syntactic type soundness with respect to a resource-instrumented semantics. We give an algorithmic version of our type system and prove its soundness. Algorithmic typing facilitates a simple surface language that does not expose tedious details of ordered types. We implemented a typechecker for the surface language along with an interpreter for the core language.

Law and Order for Typestate with Borrowing

TL;DR

This work proposes a new, transition-oriented foundation for typestate in the setting of impure functional programming, and gives an algorithmic version of the type system and proves syntactic type soundness with respect to a resource-instrumented semantics.

Abstract

Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implications. Yet, we support a flexible notion of borrowing in the presence of typestate. Our core calculus comes with a notion of resource types indexed by an ordered partial monoid that models abstract state transitions. We prove syntactic type soundness with respect to a resource-instrumented semantics. We give an algorithmic version of our type system and prove its soundness. Algorithmic typing facilitates a simple surface language that does not expose tedious details of ordered types. We implemented a typechecker for the surface language along with an interpreter for the core language.
Paper Structure (31 sections, 37 theorems, 222 equations, 13 figures)

This paper contains 31 sections, 37 theorems, 222 equations, 13 figures.

Table of Contents

  1. Introduction
  2. Motivation
  3. Ordered Partial Monoids
  4. Splitting and Order
  5. Borrowing vs. Resource-passing
  6. Aliasing and Permissions
  7. Language
  8. Syntax
  9. Operational Semantics
  10. Type System
  11. Typing Contexts
  12. Semantics of Typing Contexts
  13. Typing Rules
  14. Type Soundness
  15. Algorithmic Typing and Implementation
  16. ...and 16 more sections

Key Result

proposition 1

Contexts $\Gamma_{{\mathrm{1}}}$ and $\Gamma_{{\mathrm{2}}}$ are related by applying the monoid laws, commutativity of unordered composition, and demotion with unrestricted bindings, if and only if $\Gamma_{{\mathrm{1}}} \simeq \Gamma_{{\mathrm{2}}}$.

Figures (13)

  • Figure 1: Simple life cycle of file handles; OF=$(r|w)^*c$ (open file); CF=$\varepsilon$ (closed file)
  • Figure 2: OPM and API for ownership and mutable borrows
  • Figure 3: Syntax of expressions
  • Figure 4: Values and evaluation contexts
  • Figure 5: Operational semantics
  • ...and 8 more figures

Theorems & Definitions (69)

  • definition 1
  • Remark 1: Let expressions
  • definition 2: Heap
  • definition 3: Unrestricted and ordered types
  • definition 4: Notations for typing contexts
  • definition 5: Well-formed typing context
  • definition 6: Graph representation
  • definition 7: Join and union of graph representations
  • definition 8: Isomorphic graph representation
  • definition 9: Spanning graph representations
  • ...and 59 more