3 ms·

I am fairly well read on substructural type theories, if you could explain what you mean by ‘strictly superior’ then maybe I could formulate some points of inte

• smabie 6y ago
  Okay maybe compare and contrast them? In what cases are affine types better and in what cases are they worse (than linear types)?
  • lpage 6y ago
    As GP alluded to, there’s not really a proper ordering. If you’re talking ease-of-reasoning from a formal methods standpoint, linear types (or ordered types for that matter) are “superior” to affine types. By extension, when compiling to machine code for real-world computing architectures, linear types have advantages. They lend themselves to aggressive compiler optimization, instruction and data cache-friendly access patterns, and automatic parallelization and vectorization opportunities. All of those things boil down to proving equivalence, so the ability to mathematically reason about code has both testing and performance implications. Affine types are less foreign to most developers. The safe fragment of Rust’s ownership model is an example of an affine type system...and that’s already a bit of a lift for folks new to the borrow checker. Affine types are harder to reason about than linear types, but still much easier to reason about than the Normal [1] (in the proper noun sense) types used in most PLs. [1] https://en.wikipedia.org/wiki/Substructural_type_system https://en.wikipedia.org/wiki/Substructural_type_system