Lectures onType Theory
Swiftlet mutable values
appendix sectionsignatures

Swiftlet mutable values

Signature.

Values are finite trees represented by a pointer store; frames map names to roots. Paths select fields or array elements. Ordinary arguments are copied, while inout arguments temporarily reuse mutable path locations.

Invariant.

Distinct innermost-frame roots have disjoint accessible representations (definition 49.8). The book-owned conflict check implies physical disjointness for simultaneous inout arguments (lemma 49.6).

Source gap and repair.

The published access-relatedness relation lacks left congruence for descendants below unknown indices. The chapter therefore does not import source Lemma A.1 or Theorem 4.1 at their unrestricted signatures. Theorem 49.9, Corollary 49.10 are for the strengthened book variant. Source Theorem 4.2 remains a proof sketch.

Boundary.

No result proves LLVM lowering, copy-on-write, reference counting, current Swift or Hylo safety, first-class borrowing, or cleanup after arbitrary failure. Appendix E’s finite Kappa path auditor decides only the book conflict relation.

Search the book

Type to search the local edition.