Rusky

Is what really dependently typed? I'm saying C++ is not dependently typed, because it doesn't do any symbolic verification of N and M.

This is the wrong side of the API to make C++20 dependently typed. Concepts let the compiler report errors at the instantiation site of a template, but they don't do anything to let the compiler report errors with the template definition itself (again before instantiation time).

To be clear this distinction is not unique to dependent types, either. Most languages with some form of generics or polymorphism check the definition of the generic function/type/etc against the constraints, so the compiler can report errors before it ever sees any instantiations. This just also happens to be a prerequisite to consider something "dependently typed."

The question of whether a language is dependently typed only has to do with how type checking is done. The optimizer doesn't come into play until later, so whether it uses the information is unrelated to whether the language is dependently typed.

C++ is not a dependently typed language, for the same reason that templates do not emit errors until after they are instantiated. All non-type template parameters get fully evaluated at instantiation time so they can be checked concretely.

A truly dependently typed language performs these checks before instantiation time, by evaluating those expressions abstractly. Code that is polymorphic over values is checked for all possible instantiations, and thus its types can actually depend on values that will not be known until runtime.

The classic example is a dynamic array whose type includes its size- you can write something like `concat(vector<int, N>, vector<int, M>) -> vector<int, N + M>` and call this on e.g. arrays you have read from a file or over the network. The compiler doesn't care what N and M are, exactly- it only cares that `concat` always produces a result with the length `N + M`.

> those “killer features” are usually absolute nonsense, very niche, or they rarely have any big benefit

This is a fantastic way to turn everyone off of your language: dismiss everything they like about the ones they're already using!

It's not the same unwritten social contract: in Rust even the unsafe code has the same stricter type signatures as the safe code, so there is a formal way to judge which part of the program is at fault when the contract is broken. You might say the contract is now written. :-)

In C, the type system does not express things like pointer validity, so you have to consider the system as a whole every time something goes wrong. In Rust, because the type system is sound, you can consider each part of the program in isolation, and know that the type system will prevent their composition from introducing any memory safety problems.

This has major implications in the other direction as well: soundness means that unsafe code can be given a type signature that prevents its clients from using it incorrectly. This means the set of things the compiler can verify can be extended by libraries.

The actual practice of writing memory-safe C vs memory-safe Rust is qualitatively different.

A worked example: https://github.com/pizlonator/llvm-project-deluge/blob/delug...

They could not "just" have used SPIR-V bytecode. WebGL already had to do a bunch of work to restrict GLSL's semantics to work in the web sandbox; whatever WebGPU chose would have had the same problem.

The point of the post is that conservative GC can be useful for reasons other than that simple lack of control.

And the same can of course be done under conservative GC...

Any tracing GC, conservative or precise, generational or not, already does this. Hinkley is wrong about what "conservative" and "precise" mean.

Paterson-Wegman and Martelli-Montanari are worst-case linear, but Algorithm J just uses the earlier almost-linear union-find approach: unification variables are represented as mutable pointers to either a) nothing, or b) another type (which may itself be the "parent" unification variable in the union-find structure). Unification is then just a recursive function over a pair of types that updates these pointers as appropriate- and often doesn't even bother with e.g. path compression.

The Polonius rules were formulated using Datalog, but the implementation that will ship in rustc does not use Datalog: https://blog.rust-lang.org/inside-rust/2023/10/06/polonius-u...

In fact, those union-find trickeries come from the same paper that presented algorithm W, where they were named algorithm J. W was known from the start to be more useful for proofs than implementation:

> As it stands, W is hardly an efficient algorithm; substitutions are applied too often. It was formulated to aid the proof of soundness. We now present a simpler algorithm J which simulates W in a precise sense.

https://doi.org/10.1016/0022-0000(78)90014-4

I am not talking about UB at all. I am talking about the same constant-time stuff that djb's post is talking about.

Disabling all optimizations isn't even enough- fundamentally what you need is a much narrower specification for how the source language maps to its output. Even -O0 doesn't give you that, and in fact will often be counterproductive (e.g. you'll get branches in places that the optimizer would have removed them).

The problem with this is that no general purpose compiler wants to tie its own hands behind its back in this way, for the benefit of one narrow use case. It's not just that it would cost performance for everyone else, but also that it requires a totally different approach to specification and backwards compatibility, not to mention deep changes to compiler architecture.

You almost may as well just design a new language, at that point.

A compiler that emitted enough checks to make TypeScript sound would not perform competitively with a JIT, is my point.

Because the context here is the idea of using the type system to justify removing those sorts of dynamic checks to generate better code.

The dynamic checks in the Java case are are a well-defined and narrowly-targeted part of the language semantics- you get an exception on mismatched array writes, out-of-bounds access, etc., but when an expression produces a value it always matches its type.

TypeScript defers these kinds of type system violations to the underlying JavaScript engine, which makes things work out (sometimes with an exception, but sometimes just proceeding with a value that doesn't match the expression's type) using precisely the dynamism we wanted to get rid of. And this can leak out and cause arbitrarily-far-away parts of the program not to match their types, either.

Technically it is possible to swap the HashMap out of the Cell, mutate it, and put it back, but that is maybe even worse than the RefCell.

What I would expect a production language implementation to do is build its own table that integrates its solution for interior mutability into its design. There are several other things (e.g. iterators, concurrent GC) that will also contribute to the need for a custom table, so (again for a production language) this is not too crazy.

I guess a better way to put it is, if you got Lox working with RefCells, then you didn't need RefCells (or their overhead) to begin with - you must not have been holding those dynamic borrows any longer than a single VM instruction, or something close to that.

You don't want to use `RefCell` for something like this- it is still too strict for Lox's semantics.

Doing this properly means putting `GcData`'s fields (and/or `ObjFun`/`ObjClosure`/etc's fields) in plain `Cell`s, and using that for all mutation without ever forming any `&mut` references.

> Especially I find it confusing that the term mutable reference is sometimes used to mean a reference to a mutable place.

It always means this- unlike C, the mutability of a place is not part of its type, so if you're talking about the reference itself being mutable that will be tracked somewhere else.

Yes, it's safe to cast a reference to a raw pointer and a raw pointer to an address.

It might have been nicer in some ways if the language had restricted that a bit more up front, but it would probably have taken some design work to do that while still supporting a lot of the low-level stuff people need to do.

Yes, they are necessarily global pointers. If a self reference is an offset, what happens when you take its address (and pass that somewhere else that doesn't know where it came from)?

Now every "reference to a reference" (and similar things) can dynamically be a global pointer or a relative one, with no way to tell how to use it.

They're not quite that independent, because the choice of memory management strategy relies on the aliasing rules. But (as the post argues) the aliasing rules don't rely on the memory management strategy.

The guarantee that &mut is unique enables mutations to change the "shape" of an object in memory- e.g. reallocating a Vec to grow it, or overwriting a Box with a new one and freeing the original, or overwriting an enum/union in-place with a different variant.

If &mut were not restricted in this way, then this "eager" memory re-use could cause other references, into the interior of the shape, to dangle. But this is how Rust manages memory- if there may be other references to the old memory, when is it safe to free it, and reuse it with a potentially different type? Lifetimes don't help you here, unless you make them powerful enough to re-encode the same old aliasing rules!

It's important to note that this is not only about heap allocations. The enum/union case, for example, is entirely in-place in Rust. So even if you switch to an arena or type-segregating allocator, and accept that the old references might point to stale or now-unrelated values, you still haven't recovered memory safety. You need to keep the old value, with its old type, in place in memory simultaneously.

GC provides memory safety by making it practical to forbid these kinds of memory layouts to begin with- the program cannot eagerly free an old backing array or heap object, nor can it overwrite an enum in-place. Instead it can only mutate the references themselves, leaving the old value alone for any other references that may still exist.

There is a middle ground, where a language could allow shared mutability with more compact memory layouts, but it requires a different set of restrictions: like GC, no references to array elements or Box/enum/union fields; without a GC, working with these values requires deep copying them. Languages like Java already do this, but only for primitive types where the copy can be atomic. (Or you could use something GC-like, such as reference counting and/or copy-on-write.)

The point of the post is that the Rust approach to memory management is not the only thing that the aliasing rules gives you, because they also aid in local reasoning about your programs, regardless of your approach to memory layout and allocation.

It wouldn't. For some reason in Rust people tend to apply the term "arena" to "vector + indices" as well as the proper definition, which does have that restriction.

Neither Windows Aero nor Zed renders every single frame, 120 times per second. The parent comment is correct is correct that the important thing is to be able to render any given frame in 1/120th of a second, but to leave things alone when nothing is changing.

Roslyn specifically does not include parent pointers in its immutable AST nodes. It must do this in order to share those nodes between different versions of the tree.

It only introduces parent pointers in a convenience wrapper layer, built on-demand as you traverse the tree - you could equivalently just pass the parent down as an argument to your tree walking functions.

(The ownership problem of parent pointers also goes away when you use the arena allocation approach that the post arrives at.)

Unfortunately, C++ containers generally cannot use realloc, because they are required to invoke their elements' move/copy constructors when their addresses change.

&T is noalias - while there may be aliases none can write, which is the important thing - without UnsafeCell, and &UnsafeCell<T> loses noalias for that reason.