A directed acyclic graph, where a node can have several incoming edges, but you somehow can guarantee absence of cycles. […] I honestly have no idea if there are any languages exhibiting this mode.
This is Rust with refcounting, Rc and Arc etc.
So far this looks like an interesting variant of Rust’s borrow checker. It makes sense to integrate borrowing into the type system more explicitly.
I’m unsure from the descriptions which (if any) of the special types are implemented in the library and which are builtin language features. And I wonder if “dependencies” are exactly like Rust’s borrows, or if not, how they differ.
Pretty sure Rc/Arc don't guarantee absence of cycles? The fact you could make cycles with them was (part of?) the impetus for the Leakpocalypse, after all.
The "widening" approach in this article seems interesting, and not something I've seen before (I guess this is a thing in typescript? I've never written any typescript). I can't tell just from reading the article whether this is "magic" or a "footgun" or maybe both.
The "widening" approach in this article seems interesting, and not something I've seen before (I guess this is a thing in typescript? I've never written any typescript). I can't tell just from reading the article whether this is "magic" or a "footgun" or maybe both.
It's standard abstract interpretation per Cousot & Cousot '77, though I took some liberties with terminology (what I call "widening" is strictly the lattice join).
As someone also interested in this space, I would've found it helpful for the pt 2 post if you spelled out the type signatures for the functions and how exactly the the tracking for "what has been pushed to this array" works across function boundaries.
You also gave an example of a record where a field may be potentially reference another field, how does that work across function boundaries, where code may want to reason about aliasing? E.g. in Rust, std::mem::swap takes two mutable references so the implementation can rely on them not aliasing.
This is the subject of the next post, and I'd like to avoid spoiling it too much. Rust's approach is beautiful in its simplicity, but I wanted something less restrictive, so in my model two arguments can have arbitrary aliasing, which in turn necessitates polyvariant analysis.
Thanks! Let me know what you think when you finish. Also, it's abstract interpretation (overapproximating) and not really true dependent types - just a vaguely similar kind of thing.
fanf | 8 hours ago
This is Rust with refcounting, Rc and Arc etc.
So far this looks like an interesting variant of Rust’s borrow checker. It makes sense to integrate borrowing into the type system more explicitly.
I’m unsure from the descriptions which (if any) of the special types are implemented in the library and which are builtin language features. And I wonder if “dependencies” are exactly like Rust’s borrows, or if not, how they differ.
aw1621107 | 2 hours ago
Pretty sure Rc/Arc don't guarantee absence of cycles? The fact you could make cycles with them was (part of?) the impetus for the Leakpocalypse, after all.
drmorr | 16 hours ago
The "widening" approach in this article seems interesting, and not something I've seen before (I guess this is a thing in typescript? I've never written any typescript). I can't tell just from reading the article whether this is "magic" or a "footgun" or maybe both.
[OP] ergeysay | 10 hours ago
It's standard abstract interpretation per Cousot & Cousot '77, though I took some liberties with terminology (what I call "widening" is strictly the lattice join).
typesanitizer | 16 hours ago
As someone also interested in this space, I would've found it helpful for the pt 2 post if you spelled out the type signatures for the functions and how exactly the the tracking for "what has been pushed to this array" works across function boundaries.
You also gave an example of a record where a field may be potentially reference another field, how does that work across function boundaries, where code may want to reason about aliasing? E.g. in Rust, std::mem::swap takes two mutable references so the implementation can rely on them not aliasing.
[OP] ergeysay | 10 hours ago
This is the subject of the next post, and I'd like to avoid spoiling it too much. Rust's approach is beautiful in its simplicity, but I wanted something less restrictive, so in my model two arguments can have arbitrary aliasing, which in turn necessitates polyvariant analysis.
ocramz | 12 hours ago
Symbolic execution, linear types, dependent types, lots to chew on! Saving this for a closer read.
[OP] ergeysay | 10 hours ago
Thanks! Let me know what you think when you finish. Also, it's abstract interpretation (overapproximating) and not really true dependent types - just a vaguely similar kind of thing.