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.
3
-
$\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, 2017 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 left SESep 19, 2017 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 ClarkeSep 20, 2017 at 12:37
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
- N. Kobayashi, B. C. Pierce, D. N. Turner, Linearity and the Pi-Calculus.
- K. Takeuchi, K. Honda, M. Kubo, An Interaction-based Language and its Typing System.
- K. Honda, V. T. Vasconcelos, M. Kubo, Language Primitives and Type Disciplines for Structured Communication-based Programming.
