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

Я говорю, что агда прекрасно чекает типы без редукций.

Но она не чекает без них sup?, 5!≡12*10 и a+0≡a. Как и все прочие программы которые могут задействовать в типах произвольные вычисления.

я тебе показываю пример где агда все прекрасно чекает ничего не редуцируя, при том редукция по-твоему там очевидно нужна.

Если для проверки какой-то конкретной программы редукция не нужна — ради бога. Но я показываю примеры где она нужна. В общем случае и для множества конкретных же программ она нужна. То есть вообще на уровне системы типов.

Твоя риторика это как рассуждать про то что для всех целых чисел x и y имеет место быть x * y = 0, потому что, видите ли, при x = 0 (ты нашёл _одну_ программу без редукций) это так. Ну или «все вороны белые». Рассматривай общий случай.

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

Так оно любых, но _некоторого_ набора типов. В ATTAPL сказано, что есть T t (типы к термам), при этом множество типов никак не оговорено — может у нас чистый и тотальный лямбда-куб и полностью constexpr — теоретико-доказательной силы и CH это не отменяет, а может у нас монада IO (чтобы чистоту не ломать), тогда нужно думать как поселять в ней чистые функции и будут ли образовываться типы динамически или всё будет сильно restricted в этой IO.

И оно тогда не будет чекаться.

Ну то есть если где-то валяется closed source чекер шаблонов то всё тут же становится ок? По факту плохие программы не доживут до рантайма (чекнутся после раскрытия) что с ним, что без него.

А ни к чему не буду.

Вот и у меня — просто template с обычной такой индексацией, типа concat для std::array.

Уже сто раз пример приводился с открытым термом. Который ты на плюсах не напишешь.

Пиши вместо sym === lambda (x : T). U[x] — template <T x> ... sym() { U[x] } и sym(T[...]) — sym<T[...]>(). Что ещё нужно?

По такой логике любой язык обладает зависимыми типами

Ну то есть ты согласен с тем, что любой динамический язык обладает зависимыми типами (и вообще любыми типами), и на этом можно разойтись, так?

Значит и статической типизации нету.

У тебя как-то отрицание ради отрицания.

Всё есть, суть в теоретико-доказательной силе системы типов как _синтаксического_ средства, равно как и в её непротиворичивости и CH.

Если считать П-типы шаблонами, то тогда ты вообще не имеешь права в плюсах использовать простые функции.

И соответствующее подмножество из шаблонов и constexpr функций тогда чем будет? Имею я право видеть в индексации П-типы?

Я говорю, что агда прекрасно чекает типы без редукций.

Но она не чекает без них sup?, 5!≡12*10 и a+0≡a. Как и все прочие программы которые могут задействовать в типах произвольные вычисления.

я тебе показываю пример где агда все прекрасно чекает ничего не редуцируя, при том редукция по-твоему там очевидно нужна.

Если для проверки какой-то конкретной программы редукция не нужна — ради бога. Но я показываю примеры где она нужна. В общем случае и для множества конкретных же программ она нужна. То есть вообще на уровне системы типов.

Твоя риторика это как рассуждать про то что для всех целых чисел x и y имеет место быть x * y = 0, потому что, видите ли, при x = 0 (ты нашёл _одну_ программу без редукций) это так. Ну или «все вороны белые». Рассматривай общий случай.

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

Так оно любых, но _некоторого_ набора типов. В ATTAPL сказано, что есть T t (типы к термам), при этом множество типов никак не оговорено — может у нас чистый и тотальный лямбда-куб и полностью constexpr — теоретико-доказательной силы и CH это не отменяет, а может у нас монада IO (чтобы чистоту не ломать), тогда нужно думать как поселять в ней чистые функции и будут ли образовываться типы динамически или всё будет сильно restricted в этой IO.

И оно тогда не будет чекаться.

Ну то есть если где-то валяется closed source чекер шаблонов то всё тут же становится ок? По факту плохие программы не доживут до рантайма (чекнутся после раскрытия) что с ним, что без него.

А ни к чему не буду.

Вот и у меня — просто template с обычной такой индексацией, типа concat для std::array.

Уже сто раз пример приводился с открытым термом. Который ты на плюсах не напишешь.

Пиши вместо sym === lambda (x : T). U[x] — template <T x> ... sym() { U[x] } и sym(T[...]) — sym<T[...]>(). Что ещё нужно?

По такой логике любой язык обладает зависимыми типами

Ну то есть ты согласен с тем, что любой динамический язык обладает зависимыми типами (и вообще любыми типами), и на этом можно разойтись, так?

У тебя как-то отрицание ради отрицания.

Суть в теоретико-доказательной силе системы типов как _синтаксического_ средства, равно как и в её непротиворичивости и CH.

Если считать П-типы шаблонами, то тогда ты вообще не имеешь права в плюсах использовать простые функции.

И соответствующее подмножество из шаблонов и constexpr функций тогда чем будет? Имею я право видеть в индексации П-типы?