时间戳

首页 > 解决方案 > 有没有将整数数学纳入其类型系统的语言？

generics - 有没有将整数数学纳入其类型系统的语言？

问题描述

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

语言允许使用受约束的类型参数专门化类型是很常见的，通常称为泛型。例如，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>是有效的。但是，我相信类型系统将它们更多地视为枚举或符号，并且不将它们理解为数学值。有一些方法可以使用重载来伪造这一点。

研究讨论此类功能的关键字和文档——即使没有用一种语言实现——也很有趣。不认为对类型理论非常熟悉的资源是首选，尽管我会接受任何东西。

标签： genericstypeslanguage-design

解决方案

在 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>

这是一个工作示例。

推荐阅读