Hacker News
points by jordan_bonecut 4 days ago | 0 comments
Dependent types are part of it, yeah! There are definitely some things I dislike about Rust which I am not planning on including, mainly lifetimes and some ways they handle pointer mutability. One thing I particularly dislike about Rust is:

let x = vec![1,2,3]; let a = &mut x[0]; let b = &mut x[1]; swap(a, b);

This is not allowed. And actually in the compiler’s mind it’s for the same reason as this:

let x = vec![1,2]; let a = &mut x[0]; x.push(3); a = a + 1;

Which is definitely not safe and should be rejected. But the compiler cannot reason that the above case is actually safe, because they both fail to compile for lifetime reasons.

Another thing I’m working on are “patterns” which are like enums on steroids. In Rust you cannot define how an enum is laid out, thus requiring optimizations for types like Option<&T> to be in the compiler. In evergreen this will be in the language via a similar process to trait implementation.

[–] nicce 4 days ago
> not planning on including, mainly lifetimes and some ways they handle pointer mutability

How are you going to solve the problem with other means? Lifetimes basically guarantee, that there are no use-after-free bugs.

[–] jordan_bonecut 4 days ago
The compiler statically tracks “where” everything lives. It also knows “when” the “where” is valid.

Each “where” is called a plane, which is a tree. The stack plane contains all your function calls memory, a structure allocated on the stack has a child plane for each field. The compiler tags which plane something is from at compile time and tracks when it dies.

Things do get complicated in scenarios like:

fn max(a: &usize, b: &usize) -> &usize {

  if *a > *b { a } else { b }
}

In such a scenario the compiler tags the result with both of the input planes. However, you cannot define add a postcondition ensures clause to make it more precise

[–] tancop 3 days ago
Sounds a lot like group borrowing from Valen, but that one still has annotations like `entity in world.entities[] mut`. Are you tracking the same things implicitly with post conditions?
[–] 0c3ca83 3 days ago
And what about allocations and threads?
[–] jordan_bonecut 3 days ago
Allocations live in their own plane, the root allocated typed being the root node of that plane. For threads, I’m still working on that, don’t have a super cool answer yet
[–] 0c3ca83 3 days ago
how does that prevent use after free? pretty sure your algorithm is either very poorly explained or doesnt' actually work.
[–] jordan_bonecut 3 days ago
Another thing - when a value is moved or dropped the plane’s type changes from T to shape(T). shape(T) contains unspecified data but has the size and alignment of a T. So you couldn’t safely prove that a moved out/dropped shape(T) is a T
[–] 0c3ca83 3 days ago
This only works if you make every allocation its own plane, and scope all borrows to the lifetime of the plane, with a move terminating all borrows, at which point this is equivalent to rust, just with confusing jargon.
[–] jordan_bonecut 3 days ago
The compiler tracks all of the currently living planes. The compiler tracks from which plane each borrow is borrowed. Once the plane it is borrowed from dies that borrow is no longer valid
[–] 0c3ca83 3 days ago
If you can replace elements in a vector you can make elements unreachable.
[–] throwaway17_17 4 days ago
Since you are replying, I’ll go ahead and you answer…

In a sibling comment I said the types seem more likely to be refinement (or Liquid) types instead of being full-spectrum dependent types. Is this correct? I certainly haven’t been through enough of the docs to be confident, but I took a swing when I posted my comment.

[–] jordan_bonecut 3 days ago
What I’ve showcased is definitely not full fledged dependent types. Support is planned via ideal generics but it’s lower on the priority list to nail down