4
$\begingroup$

Are there any type systems similar to rust that don't depend on subtyping ? Can we express that one value must be consumed or dropped before another? For instance if I had an array of huge values on the heap and I would like to operate on a single item using a reference to it, the compiler would need to be sure I had finished with the reference before I could mutate or drop the parent array.

$\endgroup$
  • $\begingroup$ Maybe it's my lack of knowledge of Rust and/or type theory, but how do the features you mention relate to type systems? $\endgroup$ – Raphael Sep 19 '17 at 17:41
  • $\begingroup$ I wouldn't describe this aspect of Rust's type system as "depending" on subtyping. You can certainly find descriptions of type systems that mix linear and unrestricted (and affine and relevant) variables. If they incorporate subtyping between these, it's usually as a convenience. You can certainly explicitly witness the promotion and dereliction rules e.g. as done here. $\endgroup$ – Derek Elkins Sep 19 '17 at 23:55
  • $\begingroup$ The Rustbelt formalism of Rust's type system models the nested lifetime aspect using subtyping. To answer the question, look at region-based typing. $\endgroup$ – Dave Clarke Sep 20 '17 at 12:37
5
$\begingroup$

Linear and affine typing systems have been developed in the context of linear logic and process calculi. Most developments of such types do not use subtyping. The system in (1) is pioneering for its use of linearity, as are (2, 3) which introduced session types which are heavily based on linearity. See also the CSTheory Stackexchange thread Determinism and pi-calculus for some other (related) typing systems that make heavy use of linearity and affinity. While all this work is for process calculi, note that sequential behaviour is a well-behaved special case of concurrency and affinity in Rust is closely related (the same) as affinity in process theory.

  1. N. Kobayashi, B. C. Pierce, D. N. Turner, Linearity and the Pi-Calculus.
  2. K. Takeuchi, K. Honda, M. Kubo, An Interaction-based Language and its Typing System.
  3. K. Honda, V. T. Vasconcelos, M. Kubo, Language Primitives and Type Disciplines for Structured Communication-based Programming.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.