有没有语言把整数数学融入到他们的类型系统中？

Question

我一直在思考一个假设的语言特性，我想知道是否有任何语言做了类似的事情，我可以学习，或者可以提供相关的搜索词。

对于语言来说，允许使用受约束的类型参数来专门化类型是很常见的。例如，Foo<Bar>作为一种类型。

我很好奇是否有任何语言允许我们使用特定的整数值来参数化类型，比如Foo<10>。一个简单的用例示例可能是可以由类型检查器静态检查的固定长度数组。

我对允许在类型系统中进行基本数学运算的语言特别感兴趣。这种C#风格的伪代码将两个固定长度的数组连接成第三个具有已知长度的固定长度数组，编译器将计算该数组并将其视为常量。

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

我知道TypeScript，它很接近。它允许常量作为类型，所以Foo<10>是有效的。但是，我认为类型系统更多地将它们视为枚举或符号，而不是将它们理解为数学值。有一些方法可以使用重载来伪造这一点。

讨论这样的特性的研究关键字和文档-即使不是在语言中实现的-也是有意义的。假设不熟悉类型理论的资源是首选的，尽管我会选择任何东西。

Answer 1

在C++中，你可以用整数来参数化模板。事实上，在标准中有一个template struct array<class T, size_t N>。您可以定义一个函数来将其与编译时类型检查连接在一起，如下所示：

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;
}

使用时，将在编译过程中检查类型：

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>

这是一个working example。

Answer 2

我想你可能要找的词是dependently typed。这不是一个非常具体的术语，但它意味着类型可以依赖于值，值通常包括数字。

下面是Idris的一个示例，它是一种依赖类型的编程语言：

total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil       ys = ys
append (x :: xs) ys = x :: append xs ys

n和m是Vect的类型参数，表示向量的长度，因此将两个Vect加在一起的结果长度为n + m。