[Haskell-cafe] Haskell-Cafe Digest, Vol 218, Issue 5

[Stuart Hungerford]

On Mon, Oct 4, 2021 at 11:10 PM <haskell-cafe-request at haskell.org> 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