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

Другое дело, что у них может быть какой-то особый синтаксис

Ну (0: int) и x из (val x: int = 0) оба передаются на место int в аргумент функции в круглых скобочках, а в аргумент конструктора типа list (тоже в круглых скобочках) передаётся только (0: int), но не x, причём компилятор жалуется, что оно не static (так же как плюсы жалуются на вещь в <> которая не constant expression).

То, что плюсы не чекают шаблон - проблема плюсов.

Всё верно. Концептов нет, шаблоны не чекаются — не есть хорошо. Можно, например, переписать какое-то простенькое доказательство из зависимых типов на шаблоны, но это бессмысленно — вся конструкция не чекается, никаких гарантий нет, они будут только для конкретных инстансов (никакой универсальности). Точно так же IsAbelianSemiGroup только подразумевается (по факту — есть operator+, считаем, что ты крякнул и утка).

template<T> void f();

<typename T>?

Ты, наверно, этот f начнёшь специализировать, ну хорошо, в агде это будет:

record f-Theory (_ : Set) : Set where
  field axiom-of : IO Void

f : ∀ {T} ⦃ _ : f-Theory T ⦄ → IO Void
f ⦃ model ⦄ = f-Theory.axiom-of model

-- ^ template <typename T> f();

SomeModel : f-Theory SomeType
SomeModel = record { axiom-of = ... proof ... }

-- ^ template <> f<SomeType>() { ... }

t = f ⦃ SomeModel ⦄

-- ^ f<SomeType>();

то есть сахар instance arguments (SomeModel будет выбираться автоматически, как в плюсах, если T ~ SomeType известно из контекста) над теми же базовыми вещами (тут индексации нет, просто полиморфизм по типу).

Давай я ещё раз расскажу как я вижу (и как я твою картинку понял).

Объясняем так, мол, ребята, у нас в языке есть статические константы, то есть если есть тип T с любыми (неизвестными во время выполнения) термами и значениями, например со значениями T read_from_file() и термами some_func(read_from_file(), ...), то есть подтип T из значений которые суть статические константы, будем делать такие подтипы с помощью квалификатора constexpr — constexpt T <: T, constexpt T вкладывается в T, но не наоборот (read_from_file(), например, не вкладывается), дальше, очевидно, что на этот подтип можно сузить все примитивные операции и прочие функции — мы получаем constexpr операции и функции, а в итоге мы получаем constexpr термы вообще (constant + expression, собственно), то есть как some_constexpr_value, так и some_constexpr_func(some_constexpr_value, ...), и известно, что вычисления в рамках таких термов тьюринг-полные в compile-time, как и основной язык, равно как и типизированы, как и обычные термы. Причём семантика «статических констант» ловится именно квалификатором constexpr, более ранние const и static говорят только про память — если данный объект существовать в памяти будет, то мы можем стереть const квалификатор и изменить его значение (если это вообще можно на уровне памяти), или инициализировать const объект любым термом (read_from_file()), тогда как если не брать адреса constexpr, то ему быть в рантайме не обязательно, и инициализировать его чем угодно нельзя.

Теперь dependent product и индексированные типы. Вопрос — есть ли универсальные конструкции P(t : T). u[t] и P(t : T). U[t] (T, U — типы, t, u — термы) в языке? Очевидно, нет. Хорошо — есть ли такие типы T, что P(t : T). u[t] и P(t : T). U[t] существуют и работают — сколько угодно, constexpr типы (в языке они в <> скобочках — все constexpr). То есть как смотреть — либо эти конструкции работают для всех типов, но не для всех их термов, либо они работают не для всех типов (но для всех термов тех типов для которых они работают). Есть в функциях и (индуктивных) типах такие типы индексированные термами (какие-то типы, термами каких-то типов)? Есть.

Ты предлагаешь с каждой статической константой (вообще с канонически сконструированным в нормальной форме термом) t типа T связать тип {t} — t : {t}, {t} <: T, так что, например, в

constexpr int t = -5;

-5 это тип (кхм, дежавю). После чего все constexpt сужения операций и функции нужно поднять на уровень типов — допустим, у нас там тьюринг-полнота (не нужно, конечно, но пусть), а ещё всё так же выразительно как и в омеге, однако, нам нужно сохранить типизацию исходных функций, то есть нужно ввести отношение типизации на типах, то есть мы заменяем статические константы типами-синглетонами, так что нам нужно заменить их типы видами-синглетонами — {t} <: T <=> {t} : {T}, после чего constexpr T -> U типизируется как {T} -> {U}. В итоге P(t : constexpr T). ...[constexpr_func(t)] будет не обычным P(t : T). ...[func(t)] для constexpr T <: T, а forall (U : {T}). ...[TypeOp(U)] где всё поднято в типы. Да, и почему нужны виды — потому что ограниченная квантификация по T даст лишние подтипы (либо это должен быть специально подготовленный тип S(T) подтипы которого это ровно синглетоны — forall (U <: S(T)). ...[TypeOp(U)]). Ещё нам нужно опускать всё обратно, то есть вместо (implicit) constexpr T -> T преобразований нужны (implicit) преобразования {T} -> T (функция из вида в тип, то есть соответствие типов (синглетонов) и термов, либо S(T) -> T).

Другое дело, что у них может быть какой-то особый синтаксис

Ну (0: int) и x из (val x: int = 0) оба передаются на место int в аргумент функции в круглых скобочках, а в аргумент конструктора типа list (тоже в круглых скобочках) передаётся только (0: nat), но не x, причём компилятор жалуется, что оно не static (так же как плюсы жалуются на вещь в <> которая не constant expression).

То, что плюсы не чекают шаблон - проблема плюсов.

Всё верно. Концептов нет, шаблоны не чекаются — не есть хорошо. Можно, например, переписать какое-то простенькое доказательство из зависимых типов на шаблоны, но это бессмысленно — вся конструкция не чекается, никаких гарантий нет, они будут только для конкретных инстансов (никакой универсальности). Точно так же IsAbelianSemiGroup только подразумевается (по факту — есть operator+, считаем, что ты крякнул и утка).

template<T> void f();

<typename T>?

Ты, наверно, этот f начнёшь специализировать, ну хорошо, в агде это будет:

record f-Theory (_ : Set) : Set where
  field axiom-of : IO Void

f : ∀ {T} ⦃ _ : f-Theory T ⦄ → IO Void
f ⦃ model ⦄ = f-Theory.axiom-of model

-- ^ template <typename T> f();

SomeModel : f-Theory SomeType
SomeModel = record { axiom-of = ... proof ... }

-- ^ template <> f<SomeType>() { ... }

t = f ⦃ SomeModel ⦄

-- ^ f<SomeType>();

то есть сахар instance arguments (SomeModel будет выбираться автоматически, как в плюсах, если T ~ SomeType известно из контекста) над теми же базовыми вещами (тут индексации нет, просто полиморфизм по типу).

Давай я ещё раз расскажу как я вижу (и как я твою картинку понял).

Объясняем так, мол, ребята, у нас в языке есть статические константы, то есть если есть тип T с любыми (неизвестными во время выполнения) термами и значениями, например со значениями T read_from_file() и термами some_func(read_from_file(), ...), то есть подтип T из значений которые суть статические константы, будем делать такие подтипы с помощью квалификатора constexpr — constexpt T <: T, constexpt T вкладывается в T, но не наоборот (read_from_file(), например, не вкладывается), дальше, очевидно, что на этот подтип можно сузить все примитивные операции и прочие функции — мы получаем constexpr операции и функции, а в итоге мы получаем constexpr термы вообще (constant + expression, собственно), то есть как some_constexpr_value, так и some_constexpr_func(some_constexpr_value, ...), и известно, что вычисления в рамках таких термов тьюринг-полные в compile-time, как и основной язык, равно как и типизированы, как и обычные термы. Причём семантика «статических констант» ловится именно квалификатором constexpr, более ранние const и static говорят только про память — если данный объект существовать в памяти будет, то мы можем стереть const квалификатор и изменить его значение (если это вообще можно на уровне памяти), или инициализировать const объект любым термом (read_from_file()), тогда как если не брать адреса constexpr, то ему быть в рантайме не обязательно, и инициализировать его чем угодно нельзя.

Теперь dependent product и индексированные типы. Вопрос — есть ли универсальные конструкции P(t : T). u[t] и P(t : T). U[t] (T, U — типы, t, u — термы) в языке? Очевидно, нет. Хорошо — есть ли такие типы T, что P(t : T). u[t] и P(t : T). U[t] существуют и работают — сколько угодно, constexpr типы (в языке они в <> скобочках — все constexpr). То есть как смотреть — либо эти конструкции работают для всех типов, но не для всех их термов, либо они работают не для всех типов (но для всех термов тех типов для которых они работают). Есть в функциях и (индуктивных) типах такие типы индексированные термами (какие-то типы, термами каких-то типов)? Есть.

Ты предлагаешь с каждой статической константой (вообще с канонически сконструированным в нормальной форме термом) t типа T связать тип {t} — t : {t}, {t} <: T, так что, например, в

constexpr int t = -5;

-5 это тип (кхм, дежавю). После чего все constexpt сужения операций и функции нужно поднять на уровень типов — допустим, у нас там тьюринг-полнота (не нужно, конечно, но пусть), а ещё всё так же выразительно как и в омеге, однако, нам нужно сохранить типизацию исходных функций, то есть нужно ввести отношение типизации на типах, то есть мы заменяем статические константы типами-синглетонами, так что нам нужно заменить их типы видами-синглетонами — {t} <: T <=> {t} : {T}, после чего constexpr T -> U типизируется как {T} -> {U}. В итоге P(t : constexpr T). ...[constexpr_func(t)] будет не обычным P(t : T). ...[func(t)] для constexpr T <: T, а forall (U : {T}). ...[TypeOp(U)] где всё поднято в типы. Да, и почему нужны виды — потому что ограниченная квантификация по T даст лишние подтипы (либо это должен быть специально подготовленный тип S(T) подтипы которого это ровно синглетоны — forall (U <: S(T)). ...[TypeOp(U)]). Ещё нам нужно опускать всё обратно, то есть вместо (implicit) constexpr T -> T преобразований нужны (implicit) преобразования {T} -> T (функция из вида в тип, то есть соответствие типов (синглетонов) и термов, либо S(T) -> T).