Исправление quasimoto, (текущая версия) :
Так ты не показал ни одной редукции открытого терма
А закрытого?
Начать с того, что ты называешь редукциями только редукции закрытых термов, так что должен спрашивать сначала про них (если они есть, то и твои «редукции» есть) — ну так вот я тебе и показал, что любой закрытый терм редуцируется. Если ты считаешь, что редукций (пусть хотя бы закрытых термов) нет, то тебе не составит труда привести пример закрытого терма не в нормальной форме который не редуцируется до нормальной — но ты не приведёшь, так как они редуцируются. Иначе получится Теория Типов которая не в состоянии доказать (= пруф/тайп-чекнуть принадлежность терма-доказательства к типу-утверждению) 2 + 2 = 4 (потому что она не хочет делать 2 + 2 => 4). Просто офигенная ТТ :)
Редукции открытых термов я тоже показывал. Ниже ещё раз покажу. Без них получится Теория Типов которая не может доказать forall a. a + 0 = a. Это при том, что в задумке MLTT как минимум мощнее PA (а вообще равносильна IZF/CZF).
есть только a+1. Давай, редуцируй.
Данный терм в нормальной форме. Так же как a, suc a, a + 0 или suc (a + 0). С другой стороны, вот примеры редукций открытых термов — 0 + a => a, 1 + a => suc a, a + (2 + 2) => a + 4 или suc a + b => suc (a + b). Поэтому для доказательства forall a. a + 0 = a мы разбираем «a» в PM — в base case получается 0 + 0 = 0 => 0 = 0, что тривиально тип refl, а в step case — suc a + 0 = suc a => suc (a + 0) = suc a, что выражается рекурсивно (индукция!) через предыдущий case. И ещё раз напоминаю, что _=_ это обычный индуктивный тип, подобные ситуации и редукции возникают повсеместно.
* Тут везде считается, что N : Set; 0 : N; suc : N -> N это индуктивный тип, а _+_ определён на нём рекурсивно (индуктивно) через левый аргумент, то есть _+_ : N -> N -> N; 0 + y => y; suc x + y => suc (x + y) (вспоминаем копипасту про категорию с объектами-типами, стрелками-функциями и 2-стрелками-классами-эквивалентности-редукций :)).
У меня - абсолютно строгий формализм системы с зависимыми типами. Общепризнанные определения, которые используются в научных статьях, монографиях и т.д. - ну везде короче.
Ты хоть одну ссылку привёл? Ты берёшь понятие из математической логики (http://ncatlab.org/nlab/show/dependent product#references_34) и переосмысливаешь его в соответствии со своей программистской интуицией в расчёте на какой-то типичный ЯП («выдрал из системы все интересное, ради чего система создавалась» — ты решил для чего она создавалась, ага, не создавалась она для того чего ты ожидаешь — бери для примера любой пруф-ассистент на основе зависимых типов образца 80-ых/90-ых), при этом отвергаешь другие возможные существующие модели.
Ты под наборами А/В подразумеваешь констекспры/неконстэкспры?
Вообще constexpr это костыль. В любой системе лямбда куба (со связанной непротиворечивой теорией с CH) всё по определению «constexpr», без костылей (точнее, это единственный известный мне вариант) у нас будет система лямбда куба + незапускаемые монады Partiality и IO.
Нету. Откуда они взялись?
В LF (синтаксис + отношение типизации + отношение эквивалентности) нет зависимых типов, так и запишем. И я считаю, что в LF всё по определению constexpr (чисто, тотально, без IO, то есть известно на момент «компиляции»), да.
можешь привести хоть один параметр по которому он, быть может, не соответствует тому, чего ты ждал?
Я жду что при попытке населить
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);
программой которая возвращает пустой массив или вообще массив длинна которого не есть a + b (при аргументах с длинами a и b — зависимость! пусть a и b и compile-time known) мы получим ошибку времени проверки типов. То есть ты в сигнатуре утверждаешь факт о длинах, после чего чисто по построению (синтаксически) можно будет написать только программу которая соответствует этому факту. То есть _правильность_ — если теория (типов) говорит, что что-то _так_, то оно будет работать именно _так_ в модели (читай «рантайм» = RTS), без исключений. В динамическом языке ты ничего не утверждаешь, сигнатуры не пишешь и можешь сделать себе concat который возвращает всегда '() — в данном примере на C++ так не получится.
С КАКИМ ИМЕННО из этих утверждений ты споришь?
0. В теории типов все термы constexpr, поэтому мне не понятно требование на «любой терм». Ты хочешь ввести грязные функции как в C++, сломать теорию типов и потом что-то от неё требовать?
1. Допустим, но для любых термов каких типов, для всего универсума, а если он сломан?
2. Не вижу проблем в том чтобы конструкция не была универсальной. Исходное утверждение нужно понимать как «конкретные пи-типы формируются», что уже что-то (вообще у нас шаблоны, так что правильнее сказать «можно заставить прикидываться конкретными пи-типами в определённом подмножестве языка», но для простейших вещей вроде std::array и concat даже заставлять не нужно, и ещё — динамический язык с нормальными макросами тоже (теоретически) можно заставить, я не против).
3. А concat нам приснился :)
4. и 5. Мне не интересно есть или нет эквивалентность с омегой или её расширениями. Зачем мне делать ненужную искусственную интерпретацию (пусть значения это типы, пусть их типы это виды и так далее), когда всё и так понятно?
Исходная версия quasimoto, :
Так ты не показал ни одной редукции открытого терма
А закрытого?
Начать с того, что ты называешь редукциями только редукции закрытых термов, так что должен спрашивать сначала про них (если они есть, то и твои «редукции» есть) — ну так вот я тебе и показал, что любой закрытый терм редуцируется. Если ты считаешь, что редукций (пусть хотя бы закрытых термов) нет, то тебе не составит труда привести пример закрытого терма не в нормальной форме который не редуцируется до нормальной — но ты не приведёшь, так как они редуцируются. Иначе получится Теория Типов которая не в состоянии доказать (= пруф/тайп-чекнуть принадлежность терма-доказательства к типу-утверждению) 2 + 2 = 4 (потому что она не хочет делать 2 + 2 => 4). Просто офигенная ТТ :)
Редукции открытых термов я тоже показывал. Ниже ещё раз покажу. Без них получится Теория Типов которая не может доказать forall a. a + 0 = a. Это при том, что в задумке MLTT как минимум мощнее PA (а вообще равносильна IZF/CZF).
есть только a+1. Давай, редуцируй.
Данный терм в нормальной форме. Так же как a, suc a, a + 0 или suc (a + 0). С другой стороны, вот примеры редукций открытых термов — 0 + a => a, 1 + a => suc a или a + (2 + 2) => a + 4. Поэтому для доказательства forall a. a + 0 = a мы разбираем «a» в PM — в base case получается 0 + 0 = 0 => 0 = 0, что тривиально тип refl, а в step case — suc a + 0 = suc a => suc (a + 0) = suc a, что выражается рекурсивно (индукция!) через предыдущий case. И ещё раз напоминаю, что _=_ это обычный индуктивный тип, подобные ситуации и редукции возникают повсеместно.
* Тут везде считается, что N : Set; 0 : N; suc : N -> N это индуктивный тип, а _+_ определён на нём рекурсивно (индуктивно) через левый аргумент, то есть _+_ : N -> N -> N; 0 + y => y; suc x + y => suc (x + y) (вспоминаем копипасту про категорию с объектами-типами, стрелками-функциями и 2-стрелками-классами-эквивалентности-редукций :)).
У меня - абсолютно строгий формализм системы с зависимыми типами. Общепризнанные определения, которые используются в научных статьях, монографиях и т.д. - ну везде короче.
Ты хоть одну ссылку привёл? Ты берёшь понятие из математической логики (http://ncatlab.org/nlab/show/dependent product#references_34) и переосмысливаешь его в соответствии со своей программистской интуицией в расчёте на какой-то типичный ЯП («выдрал из системы все интересное, ради чего система создавалась» — ты решил для чего она создавалась, ага, не создавалась она для того чего ты ожидаешь — бери для примера любой пруф-ассистент на основе зависимых типов образца 80-ых/90-ых), при этом отвергаешь другие возможные существующие модели.
Ты под наборами А/В подразумеваешь констекспры/неконстэкспры?
Вообще constexpr это костыль. В любой системе лямбда куба (со связанной непротиворечивой теорией с CH) всё по определению «constexpr», без костылей (точнее, это единственный известный мне вариант) у нас будет система лямбда куба + незапускаемые монады Partiality и IO.
Нету. Откуда они взялись?
В LF (синтаксис + отношение типизации + отношение эквивалентности) нет зависимых типов, так и запишем. И я считаю, что в LF всё по определению constexpr (чисто, тотально, без IO, то есть известно на момент «компиляции»), да.
можешь привести хоть один параметр по которому он, быть может, не соответствует тому, чего ты ждал?
Я жду что при попытке населить
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);
программой которая возвращает пустой массив или вообще массив длинна которого не есть a + b (при аргументах с длинами a и b — зависимость! пусть a и b и compile-time known) мы получим ошибку времени проверки типов. То есть ты в сигнатуре утверждаешь факт о длинах, после чего чисто по построению (синтаксически) можно будет написать только программу которая соответствует этому факту. То есть _правильность_ — если теория (типов) говорит, что что-то _так_, то оно будет работать именно _так_ в модели (читай «рантайм» = RTS), без исключений. В динамическом языке ты ничего не утверждаешь, сигнатуры не пишешь и можешь сделать себе concat который возвращает всегда '() — в данном примере на C++ так не получится.
С КАКИМ ИМЕННО из этих утверждений ты споришь?
0. В теории типов все термы constexpr, поэтому мне не понятно требование на «любой терм». Ты хочешь ввести грязные функции как в C++, сломать теорию типов и потом что-то от неё требовать?
1. Допустим, но для любых термов каких типов, для всего универсума, а если он сломан?
2. Не вижу проблем в том чтобы конструкция не была универсальной. Исходное утверждение нужно понимать как «конкретные пи-типы формируются», что уже что-то (вообще у нас шаблоны, так что правильнее сказать «можно заставить прикидываться конкретными пи-типами в определённом подмножестве языка», но для простейших вещей вроде std::array и concat даже заставлять не нужно, и ещё — динамический язык с нормальными макросами тоже (теоретически) можно заставить, я не против).
3. А concat нам приснился :)
4. и 5. Мне не интересно есть или нет эквивалентность с омегой или её расширениями. Зачем мне делать ненужную искусственную интерпретацию (пусть значения это типы, пусть их типы это виды и так далее), когда всё и так понятно?