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

Параметризованные типы, такие как шаблоны 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++ разрешены только константные целые числа и указатели, но я думаю, что было бы интересно использовать любое значение для параметризации (поплавки, экземпляры классов и т. д.). Это может позволить выражать предварительные условия во время компиляции (обычно неформально указанные в документации) и автоматически проверять их во время выполнения. Например, вот шаблон «Интервал» на гипотетическом диалекте 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 с другими границами или просто правило для присвоения значения интервалу с проверкой всего во время компиляции.

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


person Gabriel Cuvillier    schedule 22.08.2010    source источник
comment
Паскаль имеет поддиапазоны целочисленных типов, которые можно рассматривать как его частный случай.   -  person Joey    schedule 22.08.2010


Ответы (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 одинаковый размер.

‹expanded›
Итак, давайте запретим побочные эффекты внутри типов и ограничим рекурсию и циклы доказуемо завершающими случаями. Делает ли это проверку типов разрешимой? С теоретической точки зрения да, может. У вас может быть что-то вроде доказательства Coq. Проблема в том, что проверку типов легко решить, если у вас достаточно аннотаций типов (аннотации типов — это информация о типизации, которую предоставляет программист). И здесь достаточно много значит. Ужасно много. Например, вводите аннотации для каждой отдельной языковой конструкции, а не только для объявлений переменных, но также для вызовов функций, операторов и всего остального. И типы будут представлять 99,9999% размера программы. Часто было бы быстрее написать все на C++ и отладить, чем писать всю программу со всеми необходимыми аннотациями типов.

Следовательно, трудность здесь заключается в том, чтобы иметь систему типов, которая требует только разумного количества аннотаций типов. С теоретической точки зрения, как только вы разрешаете опускать некоторые аннотации типа, он становится выводом типа. проблема, а не проблема чистой проверки типов. И вывод типа неразрешим даже для относительно простых систем типов. У вас не может быть легко разрешимой (гарантированной остановки) статической (работающей во время компиляции) разумной (не требующей безумного количества аннотаций типов) зависимой системы типов.
‹/expanded›

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

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

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

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

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

person Gilles 'SO- stop being evil'    schedule 22.08.2010
comment
Интересный! Возможно, если бы средство проверки типов могло быть ограничено только константными выражениями и литералами, возможно, с полным подмножеством языка, не связанным с Тьюрингом, это могло бы быть интересным дополнением к языку (например, соблюдением основных предварительных условий и инвариантов). Я изучу эту вещь с зависимыми типами. - person Gabriel Cuvillier; 23.08.2010
comment
@Gabriel: Я вижу, я немного поторопился в середине. Даже с довольно ограниченным подмножеством выражений, доступных внутри типов, может быть трудно иметь пригодный для использования язык программирования с зависимыми типами (см. мое редактирование). Вы правы насчет принудительных утверждений, это большая мотивация зависимых типов. (Имейте в виду, это большая мотивация для типов любого вида.) - person Gilles 'SO- stop being evil'; 24.08.2010
comment
интересный ответ. Я немного смущен относительно того, где шаблоны С++ стоят в этой гамме систем типов. Как отметил OP, они предоставляют понятие типов, зависящих от (статических целочисленных) значений, поэтому их можно квалифицировать как зависимую типизацию. Шаблоны также принимают параметры менее известного типа, т. е. параметры шаблона шаблона. Это дает им еще одну степень гибкости, какая теоретическая концепция стоит за этим? - person user394460; 14.04.2011
comment
@ user394460: Я не знаю C++, но я думаю, что шаблоны, зависящие от шаблонов, сделали бы систему типов более высокого порядка. С точки зрения теории систем типов шаблоны C++ представляют собой своего рода модули. Модули в стиле ML можно параметризовать в других модулях (на самом деле они для этого и нужны). - person Gilles 'SO- stop being evil'; 15.04.2011
comment
Если правило заключалось в том, что неконстанты запрещались в объявлениях мест хранения, возникала ли какая-то особая проблема? В такой ситуации, как вы показали, скорее всего, либо переменные будут объявлены как абстрактный базовый тип FixedSizeArray, либо вызов общего метода с параметром типа, который можно использовать для создания нескольких переменных в методе для создания переменных. которые, как известно, были одного типа друг с другом. - person supercat; 06.02.2013
comment
@supercat Я не уверен, что полностью понимаю ваш комментарий (думаю, я не знаком с словарем C++ или C#, который вы используете). Если вы имеете в виду тип «массив с N элементами типа T», где N должно быть константой времени компиляции, это значительно упрощает систему типов. Система типов больше не является зависимой, поскольку типы больше не параметризуются значениями, а только целыми числами. К сожалению, эта система типов довольно ограничена (хотя все еще полезна): например, вы не можете выразить конкатенацию (которая имеет тип array[N](T) → array[M](T) → array[M+N]( T) для всех целых чисел M и N). - person Gilles 'SO- stop being evil'; 06.02.2013
comment
@Gilles: В .net типы могут создаваться во время выполнения, поэтому число не обязательно должно быть константой времени компиляции, но будет конкретизироваться при создании типа. Есть способы создать во время выполнения тип значения, который ведет себя как массив любого определенного размера, но код для доступа к элементам оказывается довольно громоздким. Во многих ситуациях классу требуется массив фиксированного размера плюс одна или две другие переменные; было бы полезно, если бы данные массива и переменные можно было объединить в один объект. - person supercat; 06.02.2013

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

person Gian    schedule 22.08.2010

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

person Stephen C    schedule 22.08.2010
comment
Являются ли они как-то статически проверяемыми или они заканчиваются утверждениями во время выполнения? - person Gian; 22.08.2010
comment
Я не знаю ada, но на первый взгляд это похоже на пример шаблона Габриэля, т.е. значение Size должно быть известно во время компиляции. - person sepp2k; 22.08.2010
comment
Любое преобразование типов, включающее ограниченные типы, может вызвать Constraint_Error, и я не вижу никаких причин, по которым преобразование значений для универсальных формальных параметров будет другим. В спецификации Ada95 (проект 4.0) нет упоминания о том, что выражения, предоставляющие значения формальных параметров, должны быть доступны для оценки во время компиляции. - person Stephen C; 22.08.2010