On Mon, Oct 4, 2021 at 11:10 PM wrote:

[...] The V2 and V3 etc. types provided by the linear package (which you already found) model vectors in 2- and 3-dimensional real vector spaces, over the field given by their 'a' type parameter. Wanting to add a vector from a 2-dimensional vector space over 'a' and a vector from a 3-dimensional vector space over 'b' entails adding a 'V2 a' and 'V3 b'; those are distinct types. The vector space of 'V2 a' is morally 'a^2'.

It seems this satisfies what you want. Are there other guarantees you want enforced at compile time that this cannot give you?

Thanks Tom -- you're right this is enough for compile time guarantees. This need to encode dimensionality into a type seems to be a compelling use-case for type-level numbers or other type-level capabilities (which I've avoided learning about until now). Stu