Существуют ли языки, которые включают целочисленную математику в свою систему типов?

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

Я думаю, что вы можете искать термин зависимо набранный . Это не очень специфический термин, но это означает, что типы могут зависеть от значений, которые обычно включают числа.

Вот пример для 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.

Answer 2

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

Вот рабочий пример .