Are there any languages which incorporate integer maths into their type system?

Question

I've been thinking a little bit about a hypothetical language feature, and I'm wondering if any languages have done anything similar that I could learn from, or that could provide relevant search terms.

It's pretty common for languages to allow types to be specialised with constrained type parameters, often referred to as generics. For example, Foo<Bar> as a type.

I'm curious whether any languages allow us to parameterise types with specific integer values, like Foo<10>. A simple example of a use case might be a fixed length array that could be statically checked by the type checker.

I'm particularly interested in languages that might allow basic mathematical operations within the type system. This C# style pseudocode would concatenate two fixed length arrays into a third fixed length array with a known length, which would be calculated and treated as a constant by the compiler.

FixedArray<Length1 + Length2> Concat<Length1, Length2>(FixedArray<Length1> a, FixedArray<Length2> b)
    where Length1: Integer, >= 0
    where Length2: Integer, >= 0
    {}

I'm aware of TypeScript, which comes close. It allows constants as types, so Foo<10> is valid. However, I believe the type system treats them more like enums or symbols, and doesn't understand them as mathematical values. There are ways to fake this a bit using overloading.

Research keywords and documents discussing features like this - even if not implemented in a language - are of interest. Resources that don't presume a deep familiarity with type theory are preferred, although I'll take anything.

Answer 1

In C++ you can parametrize templates with integers. In fact there is a template struct array<class T, size_t N> in the standard. You can define a function to concatenate it with compile time type check as follows:

template<class T, size_t N1, size_t N2> array<T, N1+N2> concat(
    const array<T, N1> &a, const array<T, N2> &b)
{
    array<T, N1+N2> ret;
    /* copy data into ret */
    return ret;
}

When used, the types will be checked during compilation:

array<T, 10> a;
array<T, 5> b;
array<T, 14> ab1 = concat(a, b); // error
array<T, 15> ab2 = concat(a, b); // works
auto ab3 = concat(a, b); // type of ab3 is auto-deduced to array<T, 15>

Here's a working example.