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

Я тип template<T> void f(); спрашивал

Где T это какой-то тип, так? То есть int, ..., SomeType (определённый как struct SomeType) и т.п. Иначе это не валидная синтаксически конструкция и нужно template<typename> void f(); — как я сначала понял, когда написал про instance agruments. Ну а если template<T> void f(); в первом смысле, то тоже уже выяснили, только по-твоему есть какие-то проблемы иметь constexpr T в виде типа (скорее наоборот — в абстрактной системе типов со строгой нормализацией (как в лямбда кубе) всё изначально constexpr, вопрос в том как расширять это до частичности, памяти, эффектов).

Они ни для чего больше не нужны. Они ничем больше неинтересны. Они ничем больше не полезны.

Таки акцентирую внимание на мой вопрос — Agda, буфер с кодом на ней в Emacs, чек (C-c C-l) и выяснение того какие типы установились в результате этого чека (C-c C-d), всё compile-time, constexpr и известно до рантайма (которого просто нет, иначе пример — чего не известно). Зависимые типы — по горло. А если добавить таки рантайм, то вопрос — как там с getNat >>= \(n : Nat) -> replicate n 0 : Array Int n? Будет работать или нет? С точки зрения базовой агды это уже в нормальной форме, так как >>= это примитив, работать тут нечему — эту форму нужно отдать интерпретатору или компилятору, пусть он решает что с ней делать (но пусть лучше работает). Но индифферентно же — зависимые типы _уже_ есть, без всякого рантайма, «неизвестные» n не в базовой агде, а в монаде IO, и если кто-то не может толком смоделировать эту монаду (пример не компилируется дальнейшим бакендом), то это не отменяет существование зависимых типов в базовой агде.

Я тип template<T> void f(); спрашивал

Где T это какой-то тип, так? То есть int, ..., SomeType (определённый как struct SomeType) и т.п. Иначе это не валидная синтаксически конструкция и нужно template<typename> void f(); — как я сначала понял, когда написал про instance agruments. Ну а если template<T> void f(); в первом смысле, то тоже уже выяснили, только по-твоему есть какие-то проблемы иметь constexpr T в виде типа (скорее наоборот — в абстрактной системе типов со строгой нормализацией (как в лямбда кубе) всё изначально constexpr, вопрос в том как расширять это до частичности, памяти, эффектов).

Они ни для чего больше не нужны. Они ничем больше неинтересны. Они ничем больше не полезны.

Таки акцентирую внимание на мой вопрос — Agda, буфер с кодом на ней в Emacs, чек (C-c C-l) и выяснение того какие типы установились в результате этого чека (C-c C-d), всё compile-time, constexpr и известно до рантайма (которого просто нет, иначе пример — чего не известно). Зависимые типы — по горло. А если добавить таки рантайм, то вопрос — как там с getNat >>= \(n : Nat) -> replicate n 0 : Array Int n? Будет работать или нет? С точки зрения базовой агды это уже в нормальной форме, так как >>= это примитив, работать тут нечему — эту форму нужно отдать интерпретатору или компилятору, пусть он решает что с ней делать (но пусть лучше работает). Но индифферентно же — зависимые типы _уже_ есть, без всякого рантайма, «неизвестные» n не в базовой агде, а в монаде IO, и если кто-то не может толком смоделировать эту монаду (пример компилируется дальнейшим бакендом), то это не отменяет существование зависимых типов в базовой агде.