Есть ли язык программирования, где типы могут быть параметризованы значениями?

Параметризированные типы, такие как шаблоны С++, - это хорошая вещь, но большую часть времени они могут быть параметризированы другими типами.

Однако в С++ есть специальный случай, где можно параметризовать шаблон целым числом. Например, массивы с фиксированной длиной являются типичным прецедентом:

template<typename T, int SIZE> class FixedArray 
{ 
    T m_values[SIZE]; 

public: 
    int getElementCount() const { return SIZE; }

    T operator[] (int i) const { 
        if (i<0 || i>=SIZE) 
            throw;
        else 
            return m_values[i]; 
    }  
};

void f()
{
    FixedArray<float, 5> float_array; // Declares a fixed array of 5 floats. 
    //The size is known at compile time, and values are allocated on the stack.
}

В С++ допустимы только постоянные целые числа и указатели, но я думаю, что было бы интересно использовать любое значение для параметризации (float, экземпляры классов и т.д.). Это может позволить выразить предварительные условия во время компиляции (обычно неофициально указано в документации) и автоматически проверять их во время выполнения. Например, вот шаблон "Интервал" в гипотетическом диалекте С++:

// Interval of type T between TMin and TMax. 
template<typename T, T TMin, T TMax> class Interval
{
    T m_value;

public:
    Interval(int val) { *this = val; }

    Interval& operator = (T val) { 
        //check that 'val is in [TMin, TMax] and set the value if so, throw error if not
        if (val < TMin || val > TMax) 
            throw;
        else
            m_value = val; 

        return *this;
    };  

    operator T() const { return m_value; }
}   

// Now define a f function which is only allowing a float between O and 1
// Usually, that kind of function is taking a float parameter with the doc saying "the float is in 0-1 range". But with our Interval template we have
// that constraint expressed in the type directly.
float f(Interval<float, 0, 1> bounded_value)
{
    // No need to check for boundaries here, since the template asserts at compile-time that the interval is valid
    return ...;
}

// Example usage
void main();
{
    float val = 0.5;

    Interval<float, 0, 1> sample_interval = val;    // OK. The boundary check is done once at runtime.

    f(sample_interval);             // OK. No check, because it is asserted by the type constraint at compile-time.
                                // This can prevent endless precondition testing within an algorithm always using the same interval

    sample_interval = 3*val;            // Exception at runtime because the constraint is no longer satisfied

    f(sample_interval);             // If I am here, I am sure that the interval is valid. But it is not the case in that example.
}

Что может быть интересно тогда, чтобы выразить отношения между этими типами. Например, выражая правило, чтобы назначить интервал А другому интервалу В с другими границами или просто правило для присвоения значения интервалу, при этом все проверено во время компиляции.

Есть ли какой-либо язык с такой параметризацией (или подобный подход), или еще нужно придумать? Какие-нибудь полезные научные статьи?

Ответы

Ответ 1

Типы, параметризованные значениями, называются зависимыми типами.1 Было проведено много исследований по теме зависимых типов, но мало он достиг "основного языка".

Большая проблема с зависимыми типами заключается в том, что если ваши типы содержат выражения, т.е. биты кода, тогда средство проверки типов должно иметь возможность выполнять код. Это невозможно сделать в полной общности: что, если код имеет побочные эффекты? что, если код содержит бесконечный цикл? Например, рассмотрите следующую программу в синтаксисе типа C (ошибка проверки опущена):

int a, b;
scanf("%d %d", &a, &b);
int u[a], v[b];

Как компилятор мог узнать, имеют ли массивы u и v одинаковые размеры? Это зависит от номеров, которые вводит пользователь! Одним из решений является запрещение побочных эффектов в выражениях, которые появляются в типах. Но это не заботится обо всем:

int f(int x) { while (1); }
int u[f(a)], v[f(b)];

компилятор перейдет в бесконечный цикл, пытаясь решить, имеют ли теги u и v одинаковые размеры.

< расширен >
Таким образом, запрещайте побочные эффекты внутри типов и ограничивайте рекурсию и цикл для доказуемо завершающих случаев. Это делает проверку типов разрешимой? С теоретической точки зрения, да, это возможно. То, что у вас есть, может быть чем-то вроде Coq proof term. Проблема в том, что проверка типов тогда легко разрешима, если у вас достаточно аннотаций типа (аннотации типов - это информация для ввода, которую предоставляет программист). И здесь достаточно много значит. Очень много. Как и в, аннотации типов на каждой отдельной конструкции языка, а не только объявления переменных, а также вызовы функций, операторы и все остальное. И типы будут представлять 99,9999% от размера программы. Часто было бы быстрее написать все на С++ и отладить его, а не написать всю программу со всеми требуемыми аннотациями типа.

Следовательно, трудность здесь состоит в том, чтобы иметь систему типов, которая требует только разумного количества аннотаций типа. С теоретической точки зрения, как только вы позволяете отказаться от некоторых аннотаций типа, она становится проблемой типа вывода, а не чистым типом проверка проблемы. И вывод типа неразрешимый для даже относительно простых систем типа. Вы не можете легко получить разрешимую (гарантированную прекращение) статическую (работающую во время компиляции) разумную (не требующую безумного количества аннотаций типа) зависимую систему типов.
<Суб > </& расширенная GT;суб >

Зависимые типы иногда появляются в ограниченной форме на основных языках. Например, C99 позволяет массивы, размер которых не является постоянным выражением; тип такого массива является зависимым типом. Неудивительно, что для C компилятор не обязан проверять границы на таком массиве, даже если потребуется проверить границы для массива постоянного размера.

Более полезно, Dependent ML является диалектом ML с типами, которые могут быть проиндексированы с помощью простых целочисленных выражений. Это позволяет проверке типа статически проверять большинство границ массива.

В модульных системах для ML показан другой пример зависимого типа. Модули и их подписи (также называемые интерфейсами) похожи на выражения и типы, но вместо описания вычислений они описывают структуру программы.

Зависимые типы часто возникают на языках, которые не являются языками программирования, в смысле большинства программистов, но скорее языки для доказательства математических свойств программ (или просто математических теорем). Большинство примеров на странице wikipedia имеют такую ​​природу.

¹ В более общем плане теоретики типа классифицируют системы типов в зависимости от того, имеют ли они типы более высокого порядка (типы, параметризованные по типам) polymorphism (выражения, параметризованные типами), и зависимые типы (типы, параметризованные выражениями). Эта классификация называется куб Barendregt или лямбда-куб. На самом деле это гиперкуб, но обычно четвертое измерение (выражения, параметризованные выражениями, т.е. Функциями) само собой разумеется.

Ответ 2

Я думаю, вы в основном описываете Dependent Types. Существует ряд (в основном исследовательских) языков, которые их реализуют, связанные с этой статьей. Как правило, становится трудноразрешимым автоматически доказывать тип проживания в общем случае (т.е. Проверка типа становится очень трудной или в общем случае не разрешима), но были некоторые практические примеры их использования.

Ответ 3

Ada95 поддерживает общие формальные параметры, которые являются значениями. В примере на этой странице, Size - это общий формальный параметр, значение которого обязано быть положительным целым числом.