Is this just "Rust with dependent types"? Not saying that as a criticism, I think this is genuinely useful.

▲ jordan_bonecut an hour ago | parent | next [-]

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 an hour ago | parent | next [-]

> 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 an hour ago | parent [-]

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 16 minutes ago | parent | next [-]

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 19 minutes ago | parent | prev [-]

And what about allocations and threads?

	▲	jordan_bonecut 13 minutes ago \| parent [-]
		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

▲ throwaway17_17 an hour ago | parent | prev [-]

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.

▲ throwaway17_17 an hour ago | parent | prev [-]

The introductory examples look more like refinement type (or Liquid types) which are limited to those operations and restrictions one’s that are provable by the compiler utilizing a restricted subset of operations and computational constructs subject to deterministic proving via SAT solving. I’m going to look closer at the docs so I could be mistaken on that point. It certainly seems to have taken the ownership and ‘borrowing’ concepts for memory semantics from Rust at a quick glance at the first few pages.

▲

jordan_bonecut an hour ago | parent | next [-]

Dependent types can be achieved via “ideal Generics”. Very undocumented and not ready to commit to how they work yet, but the basic idea is that a type can be generic on a value.

▲

ch4s3 an hour ago | parent [-]

How long have you been working on this?

▲

jordan_bonecut an hour ago | parent [-]

I have been building little prototype languages for years. This iteration which is heavily AI powered is a couple weeks old

	▲	ch4s3 38 minutes ago \| parent [-]
		Oh cool, it's amazing how quickly you can stand up a language now, I love it. I'd love to exchange ideas, I really like what you're doing. How are you doing resolution of your dependent(refined?) types? I've been using Z3, but you're clearly doing something else here.

▲

ch4s3 an hour ago | parent | prev [-]

Yeah it definitely looks like refinement vs actual dependent types. I do the same thing here[1] in my language (pardon the mess). Adding liquid types to basically rust is IMHO a good idea.

[1] https://march-lang.org/docs/refinement-types/