Uses of quantification over values ("const generics" in Rust)

My last post drew comments on reddit about the uses of const generics in Rust. As one comment said, the inability to do so hurts worst in matrix operations; see the example in aforesaid earlier post. But i more often wish for this feature; other cases include the following:

Finite sets

It can be convenient to have values of finite sets of statically known size (often called Fin, for example in the Agda standard library). In Rust, it would be particularly useful for array indexing: impl Index<Fin<n>> for [_; n], which would never panic.

I also find it useful dealing with certain coding schemes, for example: UTF-8, where the range of certain internal parametres (for example: number of codons/bytes) is statically known. (I can define an enum with the appropriate number of variants and convert to usize, in which case the compiler correctly infers the range of the value, but i must do so for each size of finite set i need, which is a horrid kludge.)

Complete tree arity

It is fairly widely known, a complete binary tree can be efficiently stored as an array. But the formula is more general; for a tree of arity a, for an element at index k-1, its parent is at index k/a-1, and its children are at indices k⨯a , k×a+1 , … , k×a+a-1. It would be convenient to specify the arity of a heap in its type, lest one pass the wrong arity and mangle the heap.

Other examples

I'm sure many uses will be found for const generics. The following others immediately come to mind:

  • Buffer/cache size
  • B-tree arity

I've not even gone into const generics of type other than usize/ℕ.

Rust in 2019

Rust made good progress in 2018:

  • const fn in particular was a welcome and sorely needed feature.
  • With #[panic_handler] now stable, we can finally write no_std binary crates on stable and not worry the next release will break it.
  • We got some other useful features, including the following: u128, NonNull, fixed-length slice patterns, LTO, #[repr(transparent)], #[repr(align(_))]

In 2019, i have one major wish for Rust:
Const Generics.

The worst pain point for me, by far, is the inability to quantify over numbers. Notions as basic as an array of a CloneEq type being CloneEq are inexpressible in Rust now; see the ridiculous (and necessarily incomplete) list of impls for [_; _]. (Edit(2018-12-23): I see Clone is now magical. The infelicity remains for other traits such as Eq and Ord.) We have kludges like "typenum" and "generic-array", but consider the impl header for matrix multiplication in my matrix library:
impl<B: Copy, A: Copy + Mul<B>,
K: ArrayLength<B> + ArrayLength<GenericArray<A, M>>,
M: ArrayLength<A> + ArrayLength<A::Output>,
N: ArrayLength<GenericArray<A::Output, M>> + ArrayLength<GenericArray<B, K>>> Mul<Matrix<B, K, N>> for Matrix<A, M, K>
where A::Output: Zero + AddAssign

Writing all the ArrayLength constraints is very tedious, and they are mere noise to a reader.

But the pain is deeper yet: these types are often part of the API, which makes me hesitate to stabilize such an API before we have const generics. (It also affects APIs which want to accept buffer sizes, for example.)

I hope at some point Rust will have a much richer kind system, letting users quantify over type constructors, arrays of types, and traits, at least. (See, for example, the broad utility of Monad :: (Type → Type) → Constraint in Haskell.) But the most urgently needed is natural numbers.

Note(2018-12-27): I posted a follow-up.

Hello, world!

So i finally started a blog.

I've been meaning to do so for some years, made a few abortive attempts writing my own engine (which usually involved far too many monad transformer layers) and serving from my own machine or VPS (while saying: i'm an engineer! i can do this!), and finally figured: what the hell, i'll just use managed WordPress like everyone else. (PHP is a train wreck but hey, someone else is writing it.)

I may post about mathematics (including logic and computation), engineering, music, photography, game design, physics, biology, spacefaring, or whatever else is on my mind.