[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).