Есть ли язык программирования, где типы могут быть параметризованы значениями?
Параметризованные типы, такие как шаблоны C ++, - это хорошо, но в большинстве случаев они могут параметризоваться только другими типами.
Однако, в C ++ есть особый случай, когда можно параметризовать шаблон целым числом. Например, массивы фиксированной длины являются типичным случаем использования:
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.
}
В C ++ допускаются только постоянные целые и указатели, но я думаю, что было бы интересно использовать любое значение для параметризации (числа с плавающей запятой, экземпляры классов и т. Д.). Это может позволить выразить предварительные условия во время компиляции (обычно это неформально указано в документации) и автоматически проверять их во время выполнения. Например, вот шаблон «Interval» на гипотетическом диалекте C ++:
// 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.
}
Тогда может быть интересно выразить отношения между этими типами. Например, выражение правила назначения интервала A другому интервалу B с другими границами или просто правило назначения значения интервалу, когда все проверяется во время компиляции.
Существует ли какой-либо язык с таким параметризацией (или схожим подходом), или он все еще должен быть изобретен? Есть полезные исследовательские работы?
3 ответа
Типы, параметризованные значениями, называются зависимыми типами . На тему зависимых типов было проведено много исследований, но мало из них дошло до «основного языка».
Большая проблема с зависимыми типами заключается в том, что если ваши типы содержат выражения, то есть биты кода, тогда средство проверки типов должно иметь возможность выполнять код. Это невозможно сделать в общих чертах: что, если у кода есть побочные эффекты? что, если код содержит бесконечный цикл? Например, рассмотрим следующую программу в синтаксисе типа 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 . Проблема в том, что проверка типов тогда легко разрешима , если у вас достаточно аннотаций типов (аннотации типов - это типизированная информация, которую предоставляет программист). А здесь достаточно много значит. Ужасно много.Как и в случае с аннотациями типов в каждой языковой конструкции, не только с объявлениями переменных, но также с вызовами функций, операторами и всем остальным. И типы будут представлять 99,9999% размера программы. Часто бывает быстрее написать все это на C ++ и отладить , чем писать всю программу со всеми необходимыми аннотациями типов.
Следовательно, трудность состоит в том, чтобы иметь систему типов, которая требует только разумного количества аннотаций типов. С теоретической точки зрения, как только вы позволяете опустить некоторые аннотации типов, это становится проблемой вывода типа , а не чистой проблемой проверки типов. А вывод типов неразрешим даже для относительно простых систем типов. Вы не можете легко иметь разрешимую (гарантированно завершающуюся) статическую (работающую во время компиляции) разумную (не требующую безумного количества аннотаций типов) систему зависимых типов.
Зависимые типы иногда появляются в ограниченной форме в основных языках. Например, C99 позволяет использовать массивы, размер которых не является постоянным выражением; тип такого массива - зависимый тип. Неудивительно, что для C компилятор не обязан проверять границы такого массива, даже если потребуется проверять границы для массива постоянного размера.
Более полезно то, что Dependent ML является диалектом ML с типами, которые можно индексировать с помощью простых целочисленных выражений. Это позволяет средству проверки типов статически проверять большинство границ массива.
Другой пример зависимого типа появляется в модульных системах для ML.Модули и их сигнатуры (также называемые интерфейсами) похожи на выражения и типы, но вместо описания вычислений они описывают структуру программы.
Зависимые типы очень часто появляются в языках, которые не являются языками программирования в том смысле, который понимает большинство программистов, а скорее являются языками для доказательства математических свойств программ (или просто математических теорем). Большинство примеров на странице википедии имеют именно такой характер.
¹ В более общем плане теоретики типов классифицируют системы типов в зависимости от того, имеют ли они типы высшего порядка (типы, параметризованные типами), полиморфизм (выражения, параметризованные типами) и зависимые типы (типы, параметризованные выражениями). Эта классификация называется кубом Барендрегта или лямбда-кубом . На самом деле это гиперкуб, но обычно четвертое измерение (выражения, параметризованные выражениями, т. Е. Функции) само собой разумеется.
Я думаю, вы в основном описываете зависимые типы . Существует ряд (в основном исследовательских) языков, реализующих их, ссылки на которые приведены в статье. Автоматическое подтверждение наличия типа в общем случае становится трудноразрешимым (т.е. проверка типов становится очень сложной или в общем случае неразрешимой), но были некоторые практические примеры их использования.
Ada95 поддерживает общие формальные параметры, которые являются значениями. В примере на этой странице, Size является общим формальным параметром, значение которого должно быть целым положительным числом.