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.
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.
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
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.