3 ms·
> And, if you think that a type system can be no help with some family of data structures, it can only because you are unfamiliar with powerful type systems. I
by the-lazy-guy 4y ago
> And, if you think that a type system can be no help with some family of data structures, it can only because you are unfamiliar with powerful type systems.
I am. Would you please point me at some things to study?
The best I can imagine is languages like F* (https://www.fstar-lang.org/ https://www.fstar-lang.org/, and more specifically the Low* subset for dealing with memory) which make you prove everything. And thus are such a PITA to program in that it make sense to code only the most security-demanding things.
Dependant types are also not able to protect you from memory bugs in self-referential datastructures AFAIK.
I am open to reading about research in PL. But if you point me at some mainstream (or just production-ready) languages/runtimes it would be even better.
Thanks.
- ncmncm 4y agoYou are in luck: ML, Haskell, and C++ all support powerful type systems. Rust's has been growing in power, coming from behind. Its recent addition of an analog to C++'s numeric template arguments was a big improvement. Meanwhile, C++20's long-gestating "concept" support moved it into new territory. So reading up on what can now be done with C++ concepts should give you some ideas. For a more abstract treatment, read about Haskell's type classes.
- the-lazy-guy 4y agoML and Haskell are languages with garbage collection. In case of Haskell it is also pure and lazy which makes it a huge PITA to use for any non-trivial non-hierarchical datastructures. You can look at Okasaki's book to see what level of mental gymnastics is needed to make it usable in some cases. Neither C++ now Rust can help you self-referential datastructures through types. In both you have either give up any help from compiler. Or pay some price for runtime checks (via shared_ptr/weak_ptr in C++ or their friends Rc/Weak in rust). Exactly like the ones described in the article. Concepts, Rust traits, Haskell Type classes provide close to 0 help with memory management. These are a typesafe way to write generic code. Things which do help with memory management at the language level (with 0 runtime costs) are Rust's borrow checker (and more generally(?) linear/affine types), F* proofs, and dependant types (you can prove index bounds with them to some extent). All of them are useful, but can't really model all interesting programs (i.e. you have to sidestep typesystem and just tell compiler "I know that I am right").
- ncmncm 4y agoRuntime assistance coupled via the type system is fully as legitimate as GC. Your example with "up" pointers in a pointer-linked tree (or DAG) structure is very easily handled that way. General graphs are, as I noted, better handled by decoupling ownership from connectivity, as is almost always quite easy.
- the-lazy-guy 4y ago> General graphs are, as I noted, better handled by decoupling ownership from connectivity, as is almost always quite easy. Let me reiterate once again. Decopling of ownership from connectivity does not solve any correctness problems. Instead of "use-after-free" you get "use-of-object-in-some-random-state" which might be even worse, since no tooling like address sanitizer or Valgrind will help you. > Runtime assistance coupled via the type system is fully as legitimate as GC. Your example with "up" pointers in a pointer-linked tree (or DAG) structure is very easily handled that way. > Runtime assistance coupled via the type system is fully as legitimate as GC. You do understand that this particular article is exactly about it? Runtime assistance comes at a cost, though. Actually very measurable if you for some reason want to get max performance. (atomic refcounting is expensive). More generally, any memory management approach is fully legitimate, including fully manual a-la C. But rigorous refcounting in C++ and Rust comes at a very high cost, and to make it as useable as tracing GC you have to actually implement cycle detection which makes it even more costly. So people generally cheat, and for some sorts of performance-sensitive code, that makes a lot of sense.
- ncmncm 4y agoThere is zero value in refcounting for tree node lifetimes. DAGs, only sometimes. Graphs are rarely as general as textbooks usually imply, although it is easy to find (e.g. geographical) examples that are. Fully manual memory management has been demonstrated not to be legitimate, for reasons well covered already. It is just the only choice in weak languages.
- the-lazy-guy 4y ago