Здравствуйте, Кодт, Вы писали:

К>Эта штука называется "зависимые типы". К позиции 0 можно прибавлять смещение 7, а к позиции 1 — уже нельзя.

В том же русте не так. Ты можешь сложить числа 100 и 200, но если оба аргумента имеют тип u8, то компилятор тебе ничего не скажет. Типа всё ок. Но ты получишь падающую программу, из-за чего матерясь полезешь явно кастить оба аргумента к i32. Ну и нахрена оно надо, изначально-то чего в i32 не хранится? Нахрен мне нужно ограничение, при котором предполагается, что промежуточный результат будет иметь те же ограничения, что и сами данные, если это вообще даже близко не так? И тогда зачем вообще ограничивать тип, когда проще все эти проверки делать в сеттере поля?

К>Те же chrono.
К>По большому счёту, там только time_point<???> и duration<???>, и очевидно, нужно сделать всю арифметику между всеми типами time и всеми типами duration, плюс какие-то удобные приведения, — чтобы у пользователя вообще не возникало желание что-то там хакнуть, выковырять внутреннее представление и надругаться напрямую.

И получаем либу, с которой невозможно работать без часового курения документации. А по факту было бы достаточно одной-единственной функции, возвращающей число наносекунд с начала эпохи в виде примитивного типа i128 (знаковый, чтоб можно было вычитать два момента и не париться). Если нужны даты и дни недели — то отдельными функциями, которые берут это самое i128 дальше сами там всё считают.
А ещё с этими ограничениями я не могу написать так:

class C {
  C(int128& time): time(time) { time -= std::chrono::now(); }
  ~C() { time += std::chrono::now(); }
  int128& time;
};

(после работы этого кода значение time увеличится ровно на то время, когда жил класс C)
Конечно это всё можно обойти, и для случая когда надо просто сложить-вычесть, легко это написать по-другому. Но операции над теми же векторами бывают посложнее.

К>Долбаный хипстер ввёл Point, Vector и Rotation, а людям расхлёбывать, да? А может, людям за чистотой своих рук последить, прежде чем Point+Point или Point+Rotation делать, не?

Point+Point это нормальная операция, не надо её запрещать. Point+Rotation конечно может привести к неприятностям, но я слабо представляю себе, как можно даже случайно так написать. В случае же разделения вектора и точки на два типа получаем код, которым очень трудно пользоваться, причём геморрой от борьбы с тараканами хипстера намного превышает вероятность потенциального бага, который к тому же легко обнаружить и исправить.

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

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