是否有一种编程语言,其中类型可以通过值进行参数化？

Question

参数化类型(如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"模板:

// 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,或者仅仅是将规则值分配给间隔的规则,并在编译时检查所有内容.

是否有任何语言采用这种参数化(或类似的方法),还是必须发明一种语言？有用的研究论文？

Answer 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具有相同的大小.

^<expanded>
所以让我们禁止在类型内部产生副作用,并限制递归和循环以证明终止案例.它是否使类型检查可判定？从理论的角度来看,是的,它可以.你所拥有的可能是 Coq证明术语.问题是如果你有足够的类型注释,类型检查很容易判断(类型注释是程序员提供的输入信息).这里足够意味着很多.太可怕了.在中,在每个单一语言结构中键入注释,不仅是变量声明,还包括函数调用,运算符和其他所有结构.类型将占程序大小的99.9999%.在C++中编写整个内容并对其进行调试通常会更快 比使用所有必需的类型注释编写整个程序.

因此,这里的困难是使类型系统仅需要合理数量的类型注释.从理论的角度来看,只要您允许省略某些类型注释,它就会成为类型推理问题而不是纯类型检查问题.即使是相对简单的类型系统,类型推断也是不可判定的.您不能轻易地使可判定(保证终止)静态(在编译时运行)合理(不需要疯狂数量的类型注释)依赖类型系统.
_</扩展>

依赖类型有时在主流语言中以有限的形式出现.例如,C99允许大小不是常量表达式的数组; 这种数组的类型是依赖类型.毫无疑问,对于C,编译器不需要检查这样的数组上的边界,即使需要检查常量大小的数组的边界.

更有用地,从属ML是方言ML与可由简单的整数表达式被索引的类型.这允许类型检查器静态地检查大多数数组边界.

依赖类型的另一个示例出现在ML的模块系统中.模块及其签名(也称为接口)类似于表达式和类型,但它们不是描述计算,而是描述程序的结构.

在大多数程序员认可的意义上,依赖类型经常出现在非编程语言的语言中,而是用于证明程序的数学属性(或仅仅是数学定理)的语言.维基百科页面中的大多数示例都具有这种性质.

¹ _{更一般地说,类型理论家根据类型系统是否具有高阶类型(按类型参数化的类型),多态(由类型参数化的表达式)和依赖类型(由表达式参数化的类型)对类型系统进行分类.这种分类称为Barendregt的立方体或lambda立方体.实际上它是一个超立方体,但通常第四个维度(由表达式参数化的表达式,即函数)不言而喻.}

Answer 2

我认为你基本上是在描述依赖类型.从文章中可以看出,有许多(主要是研究)语言实现了这些语言.在一般情况下,自动证明类型居住往往变得难以处理(即类型检查变得非常困难,或者在一般情况下不可判定),但是已经有一些使用它们的实际例子.