Есть ли название для батут-класса?

Question

Я разрабатываю язык программирования, и одна функция, которую я хотел бы добавить, - это перекресток между trampoline function и class. То есть, класс, который принимает буквальный, похожий на generic class, принимающий в . Я застрял на имени для них, потому что раньше я не встречался с ними на языке, есть ли что-то, что уже означает эту концепцию или что-то близкое? Использование trampoline class является опцией, но если есть что-то, что более точно описывает это или уже используется на другом языке, я бы предпочел пойти с ним, чтобы сократить количество жаргона, требуемого в документации.

Псевдо-код следует проиллюстрировать этот принцип в случае, если это не ясно из сказанного выше:

class Point<const int n> { 
    private float[n] _value; 
    Point() { 
     for (int i = 0; i < n; i++) { 
      this._value[i] = 0f; 
     } 
    } 
    Point(Point<o> other) { 
     for (int i = 0; i < min(n, o); i++) { 
      this._value[i] = 0f; 
     } 
    } 
    public static float operator [index] (optional float value = null) { 
     if (value != null) { this._value[index] = value; } 
     return (this._value[index]); 
    } 
    public static Point<max(o, p)> operator + (Point<const int o> p1, Point<const int p> p2) { 
     Point<min(o, p)> small = (p1.n < p2.n ? p1 : p2); 
     Point<min(o, p)> large = (p1.n < p2.n ? p2 : p1); 
     Point<max(o, p)> ret = new Point<max(o, p)>(large); 
     for (int i = 0; i < min(o, p); i++) { ret[i] += small[i] } 
     return (ret); 
    } 
} 

Answer 1

Термин вы ищете dependent types. Это означает, что тип может не только иметь параметры типа (например, дженерики), но и тип можно также параметризовать произвольными значениями (параметры зависимого типа). Например, вы можете определить подпись функции, которая принимает число n и возвращает массив длиной n.

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

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

---

В комментариях ниже, мы выяснили, что та часть, которая, как представляется, параметр зависимого типа не должна фактически использоваться для проверки типа. Вместо этого его можно рассматривать как неявный параметр. Он похож на неявный параметр, проходящий на языке программирования Scala.