История изменений

Нет, не видней.

Кхм, ничего не имею возразить :)

На практике нужно.

На практике их нет. Не напишешь ты общий интерфейс на каждый чих.

Ты говоришь о сферическом в вакууме программировании.

Нет ты. Ещё раз — если интерфейсов нет, то никакой передачи одного типа на место аргумента который (в статике) ждёт другой быть не может, так что не понятно что ты собрался конвертировать во что. А если интерфейсы ООП, концепты обобщённого программирования или теории зависимых типов есть, и Вася с Петей написали зачем-то в рамках одного проекта два таких, решающих схожие задачи, то кому-то придётся их совмещать — так это не проблема зависимых типов, и непонятно почему ты думаешь, что в их случае конвертировать теории это накладно (я пробовал в агде — те же тривиальные враперы, а там много теорий в Algebra.* и Сategories.*, например).

Гора аннотаций осталась.

Откуда гора? «Ты говоришь о сферическом в вакууме программировании». Если я хочу гарантии для operator[](size_t i) для std::array<T, n>, то не гора, а добавление только <less<i, n>> после круглых скобок и вызовы вида if (i < n) { ... x[i]; ... } else { ... x[i]; <- static error ... } (operator<, less и bool должны быть связаны, dependent-if должен создавать контекст с пруфом, сами свидетели в угловых скобках после круглых в данном случае стираются во время компиляции). А если не хочу — будет как было.

Ну также один в один.

#include <array>

template <typename T, size_t a, size_t b>
std::array<T, a + b> concat(std::array<T, a> const& x, std::array<T, b> const& y) {
    std::array<T, a + b> z;
    std::copy(x.begin(), x.end(), z.begin());
    std::copy(y.begin(), y.end(), z.begin() + x.size());
    return z;
}

#include <cstdio>

int main() {
    for (auto const& x : concat(std::array<int, 3>{{1, 2, 3}},
                                std::array<int, 2>{{4, 5}}))
        printf("%d\n", x);
}

давай на хаскеле98 компилируемый и работающий с main (массивы-аргументы можно сделать переменными, результат concat — тоже, с auto или без), а потом ещё почитаем ассемблер :).

Так в плюсах тоже не по term. n - это не терм, а тип, просто сахарок Zero/Succ на уровне типов.

Мы этого не знаем. А знаем мы, что n можно передать в обычную (constexpr) функцию на место аргумента с обычным типом std::size_t, так что таки терм.

с++, где захуячена макросистема на простой типизированной лямбде

Ага, с quote и defmacro, «макросистема шаблонов», блин. Это ложная предпосылка про шаблоны-макросы, так что я не комментирую дальше. Я dependnet product показал (concat для std::array), ссылка на википедию про то что LambdaP в лямбда кубе это уже зависимые типы — была, NList : Set → ℕ → Set — тоже показал, про type -> type, term -> type, type -> term в type-level (которые делаются не какими-то там макросами, а обычной рекурсией с выборами — структуры играют роль таких type-level рекурсивных функций, причём если посмотреть, то g++ и clang++ умеет для них оптимизации, так что код получается хороший в итоге) сказал, про стандартные type traits (типа is_same) — тоже. Так что тут вопрос обратный — что такого умеют шаблоны, что не вкладывается один в один в зависимые типы (потому что макросы умеют кучу всего, поэтому они к зависимым типам не имеют прямого отношения).

Нет, не видней.

Кхм, ничего не имею возразить :)

На практике нужно.

На практике их нет. Не напишешь ты общий интерфейс на каждый чих.

Ты говоришь о сферическом в вакууме программировании.

Нет ты. Ещё раз — если интерфейсов нет, то никакой передачи одного типа на место аргумента который (в статике) ждёт другой быть не может, так что не понятно что ты собрался конвертировать во что. А если интерфейсы ООП, концепты обобщённого программирования или теории зависимых типов есть, и Вася с Петей написали зачем-то в рамках одного проекта два таких, решающих схожие задачи, то кому-то придётся их совмещать — так это не проблема зависимых типов, и непонятно почему ты думаешь, что в их случае конвертировать теории это накладно (я пробовал в агде — те же тривиальные враперы, а там много теорий в Algebra.* и Сategories.*, например).

Гора аннотаций осталась.

Откуда гора? «Ты говоришь о сферическом в вакууме программировании». Если я хочу гарантии для operator[](size_t i) для std::array<T, n>, то не гора, а добавление только <less<i, n>> после круглых скобок и вызовы вида if (i < n) { ... x; ... } else { ... x; <- static error ... } (operator<, less и bool должны быть связаны, dependent-if должен создавать контекст с пруфом, сами свидетели в угловых скобках после круглых в данном случае стираются во время компиляции). А если не хочу — будет как было.

Ну также один в один.

#include <array>

template <typename T, size_t a, size_t b>
std::array<T, a + b> concat(std::array<T, a> const& x, std::array<T, b> const& y) {
    std::array<T, a + b> z;
    std::copy(x.begin(), x.end(), z.begin());
    std::copy(y.begin(), y.end(), z.begin() + x.size());
    return z;
}

#include <cstdio>

int main() {
    for (auto const& x : concat(std::array<int, 3>{{1, 2, 3}},
                                std::array<int, 2>{{4, 5}}))
        printf("%d\n", x);
}

давай на хаскеле98 компилируемый и работающий с main (массивы-аргументы можно сделать переменными, результат concat — тоже, с auto или без), а потом ещё почитаем ассемблер :).

Так в плюсах тоже не по term. n - это не терм, а тип, просто сахарок Zero/Succ на уровне типов.

Мы этого не знаем. А знаем мы, что n можно передать в обычную (constexpr) функцию на место аргумента с обычным типом std::size_t, так что таки терм.

с++, где захуячена макросистема на простой типизированной лямбде

Ага, с quote и defmacro, «макросистема шаблонов», блин. Это ложная предпосылка про шаблоны-макросы, так что я не комментирую дальше. Я dependnet product показал (concat для std::array), ссылка на википедию про то что LambdaP в лямбда кубе это уже зависимые типы — была, NList : Set → ℕ → Set — тоже показал, про type -> type, term -> type, type -> term в type-level (которые делаются не какими-то там макросами, а обычной рекурсией с выборами — структуры играют роль таких type-level рекурсивных функций, причём если посмотреть, то g++ и clang++ умеет для них оптимизации, так что код получается хороший в итоге) сказал, про стандартные type traits (типа is_same) — тоже. Так что тут вопрос обратный — что такого умеют шаблоны, что не вкладывается один в один в зависимые типы (потому что макросы умеют кучу всего, поэтому они к зависимым типам не имеют прямого отношения).