4 ms·

I'm not super well versed on this stuff, but aren't affine types strictly superior? Though I suppose linear types might be better for tracking system resources?

• throwaway17_17 6y ago
  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 interest, but as the question stands, I don’t think there is any justification for claiming that affine types are better than linear types.
  • 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
• deleted 6y ago
  [deleted]
• deleted 6y ago
  [deleted]
• logicchains 6y ago
  Linear types let you ensure resource cleanup; files flushed/closed, memory freed, radiation-emitter disabled. That's why even in safe Rust code, it's possible to leak memory, and for the program to e.g. shut down without calling the "switch off the radiation emitter" destructor on a medical device.
  • akiselev 6y ago
    > files flushed/closed, memory freed, radiation-emitter disabled All of this is performed by destructors/GC cleanup/Drop in most languages. > That's why even in safe Rust code, it's possible to leak memory It's possible to leak memory through circular references and lazy evaluation in all languages AFAIK. > e.g. shut down without calling the "switch off the radiation emitter" destructor on a medical device. Unsafe unwinding is possible in any language, including one with linear types. If the runtime crashes, there's nothing to guarantee their one-time use.
    • logicchains 6y ago
      >All of this is performed by destructors/GC cleanup/Drop in most languages. Most GC languages don't guarantee that finalisers will run on shutdown, and no languages I'm aware of guarantee that destructors will run. For really safety critical applications it's not enough that it works fine most of the time; it needs to provide an iron-clad guarantee (as e.g. Ada with Spark can provide for many things). When writing a library it's not possible to guarantee the user will use it correctly when the compiler isn't able to enforce this. >It's possible to leak memory through circular references and lazy evaluation in all languages AFAIK. In a garbage-collected language, circular references alone aren't enough to cause memory leaks, as if the circle is not referenced transitively from the root object then it will still be collected. >Unsafe unwinding is possible in any language, including one with linear types. If the runtime crashes, there's nothing to guarantee their one-time use. That's true and unfortunate. But linear types at least guarantee that with orderly shutdown, every destructor will be called correctly.
      • pjmlp 6y ago