[_0w8t]

Zig approach essentially parametrizes instances of containers on the instance of the allocator. To properly support that in the type system one needs dependent types.

In theory that can be done, but the consequences for the compilation time will be extreme as the compiler becomes essentially a generic theorem prover.

Plus the noise from the proofs in the sources will be much bigger than that of type parameters.

[throwaway17_17]

I’m pretty sure the ‘logic’ require for paramterizing container types over allocators can be restricted in a wide majority of cases to a linear set which would allow for refinement types to be used. This would eliminate the requirement for full theorem proving.

In fact, it would probably be acceptable to insist on keeping the scope of parameterization limited to the linearly determinable set of values and operations on those values.

[_0w8t]

A Zig-style allocator that is passed as arguments requires to introduce a dependency of the type of the container on the instance of the allocator.

Perhaps it is possible to specialize for that case a generic prover, but I am sceptical that the effect on compilation timing will be minimal.

[iudqnolq]

Are you sure? I have no type theory experience but that sounds trivially expressible in Rust. The issues around making the stdlib allocactor-parametric have been about optimal api design, not theoretical possibility.

Just write

   struct MyVec<T, A> { ... }

   impl<T, A: Allocator> MyVec { ... }

[_0w8t]

That just restricts A to implement Allocator trait and will allow to pass any instance of Allocator when calling methods of MyVect. This is unsafe. What is required for safety is to state that all methods of MyVec that receives the allocator reference can only work with one particular instance of Allocator.

To make this compile-time safe in Rust a typical approach is to embed the Allocator reference in MyVect and use regions to ensure that allocated data do not outlive the allocator. This bloats MyVect with a reference to the allocator. To workaround this one specializes for static allocators to eliminate the need to embed the reference to those in MyVect.

An alternative that is not covered in the article is to require that a reference to the allocator can always be deduced from the allocated data. This solves the bloating problem as the overhead can be reduced to a word per allocation page which is typically at least CPU page in size.

Still even with this the result is not optimal especially with arena-style allocators when one wants to ensure the max performance of tiny allocations.

[iudqnolq]

> That just restricts A to implement Allocator trait and will allow to pass any instance of Allocator when calling methods of MyVect.

No, that kind of rust generic requires monomorphization rather than dynamic dispatch. Any given Vec must have a specific A, just like it must have a specific T.

> To make this compile-time safe in Rust a typical approach is to embed the Allocator reference in MyVect

Yeah, that was implied by the "...". It won't compile otherwise, generics have to be used (including by PhantomData).

But I understand the problem better now. You're right, there's no good way in the type system to specify "you must always provide the same instance of this allocator when calling any method on this vec". (I'm ignoring branding because I think it's not practically convenient).

[throwawaymaths]

I think realistically if you want to prove safety of memory provenance in zig, you assume that allocators are sound, and you just track the lifetime of the memory from alloc/create to free/destroy and call it a day. This is probably "good enough", and in rust you're assuming the allocation is sound as well, it's just implicit.

[anonymoushn]

What you get for free with the global allocator is a guarantee that you will use the same allocator for each operation on an allocation. That is the property that is claimed to be difficult to keep if you literally do the Zig thing and have e.g. ArrayListUnmanaged which requires you to pass in the allocator again to free the backing slice.

[throwawaymaths]

Ok so those are 'unsafe'. Plenty of safe (when statically checked) data structures in zig, like the managed array list, where the associated allocator is attached to the object.