3 ms·

One of the fascinating ambitions of Rust is to bring linear type systems to the mainstream. The programming world is so un-acquainted with linear types, yet the

One of the fascinating ambitions of Rust is to bring linear type systems to the mainstream. The programming world is so un-acquainted with linear types, yet the possibilities are staggering. To me, functional programming languages were always based around referential transparency: the property that a name and its value are interchangeable. But Rust takes another approach: a name is an owner of value, and owners are linear resources. This is very exciting, and makes me want to learn linear logic. It also makes me wonder if there is a smaller language dying to break out of this larger one.

pcwalton 13y ago
> It also makes me wonder if there is a smaller language dying to break out of this larger one. I don't think so, at least without sacrificing one of (a) memory safety; (b) no mandatory garbage collection; (c) race-free concurrency. Virtually every feature in Rust* is necessary to achieve one of those three goals. * OK, not methods, typeclasses, or macros. But methods and interfaces/typeclasses in some form are more or less an expected part of every programming language that is to go mainstream nowadays, and macros are necessary for really important conveniences like println and deriving to work.
- aaronblohowiak 13y ago
  You could if you had only linear-typed mutable and refcounted immutable. Refcounted immutable obviously could not contain pointers to linear typed mutable things. That would be much simpler, just as safe and require no GC.
  - pcwalton 13y ago
    Well, you'd have no multiply-owned mutable state then, which would prohibit a bunch of useful things (such as implementing the DOM in a browser). In any case, you just described basically how Rust the language works: the ref-counted mutable types are all just part of the standard library, implemented with unsafe code but exposing a safe interface. The only mutability in the language itself is through linear types.
Kutta 13y ago
I'm excited about practical linear typing implemented on the top of full-dependent systems. It would bode pretty well for experimentation and research, more so than baked-in linear type systems, because of the possibility of writing new stuff without having to touch the compiler internals. In Idris there is some experimental support from writing effectively linear/substructural typing rules for some program state, all within the language, and using it to enforce resource usage or state transitions. http://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf http://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf In its current form it's not all that usable, because Idris itself is not usable, the error messages are positively Lovecraftian, and there is a hefty performance overhead. But it could be really good when fleshed out. It would be also great to be able to interface higher-level linear typing constructs with low-level primitives, so that we could reproduce some of the main benefits of the Rust type system, and maybe write some kind of custom "ST monad on steroids" with more control over memory.
- deleted 13y ago
  [deleted]

pcwalton 13y ago

> It also makes me wonder if there is a smaller language dying to break out of this larger one. I don't think so, at least without sacrificing one of (a) memory safety; (b) no mandatory garbage collection; (c) race-free concurrency. Virtually every feature in Rust* is necessary to achieve one of those three goals. * OK, not methods, typeclasses, or macros. But methods and interfaces/typeclasses in some form are more or less an expected part of every programming language that is to go mainstream nowadays, and macros are necessary for really important conveniences like println and deriving to work.

aaronblohowiak 13y ago
You could if you had only linear-typed mutable and refcounted immutable. Refcounted immutable obviously could not contain pointers to linear typed mutable things. That would be much simpler, just as safe and require no GC.
- pcwalton 13y ago
  Well, you'd have no multiply-owned mutable state then, which would prohibit a bunch of useful things (such as implementing the DOM in a browser). In any case, you just described basically how Rust the language works: the ref-counted mutable types are all just part of the standard library, implemented with unsafe code but exposing a safe interface. The only mutability in the language itself is through linear types.

Kutta 13y ago

I'm excited about practical linear typing implemented on the top of full-dependent systems. It would bode pretty well for experimentation and research, more so than baked-in linear type systems, because of the possibility of writing new stuff without having to touch the compiler internals. In Idris there is some experimental support from writing effectively linear/substructural typing rules for some program state, all within the language, and using it to enforce resource usage or state transitions. http://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf http://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf In its current form it's not all that usable, because Idris itself is not usable, the error messages are positively Lovecraftian, and there is a hefty performance overhead. But it could be really good when fleshed out. It would be also great to be able to interface higher-level linear typing constructs with low-level primitives, so that we could reproduce some of the main benefits of the Rust type system, and maybe write some kind of custom "ST monad on steroids" with more control over memory.

deleted 13y ago
[deleted]