On Monday, 25 August 2014 at 01:09:59 UTC, Ola Fosheim Grøstad
wrote:
Cool initiative!
It is probably a good idea to look at what other languages with
linear type systems are doing:
http://en.m.wikipedia.org/wiki/Substructural_type_system
The idea is mostly inspired by Rust, but it came out very
different. Rust's borrowing rules are way more complicated. It
also has to deal with move semantics, for example. And it
annotates lifetimes, not owners, and thereby gets
non-hierarchical dependencies, as far as I understand it. I
believe this proposal is close to the best we can achieve without
resorting to data flow analysis.
My gut feeling is that borrowing in D will suffer the same
problems as @safe without a high level IR that is proven
correct. Meaning, if the IR is correct you can add new language
features without breaking the type system.
I'm unfortunately not familiar with the theoretical foundations
of type systems, and formal logic. So I'm not sure what exactly
you mean here. It seems to me the problems with @safe are with
the way it was implemented (allow everything _except_ certain
things that are known to be bad, instead of the opposite way:
allow nothing at first, but lift restrictions where it's safe to
do so), they are not conceptual.
But if you see potential problems, or know a way to avoid them,
this is exactly the kind of thing I'd like to see discussed.
