. Потому как основания систем и теорий типов и видны в математике
Так о чем и речь. Для систем типов есть элементарные теории, пиши диссеры - не хочу. Тем более что уже все написано, а для переливания из пустого в порожнее и думать ообо не нужно.
В них как раз можно, есть куча интереснейших тем. Да та же гигиена, понятно что можно определить ее как макросистема сохраняющую альфа-эквивалентность вовремя экспанда - и сразу вопрос: а можно ди и как проверить сохранение не дедая экспанд? Формальные модели есть толькл для подмнлжеств которые уже даже syntax-rules, а между тем мы сразу получим идеальный формальный фреймворк для исследования возможностей полного тайпчека до экспанда, что было бы охренительно круто - но никто этим не занимается, потому что сложно. Все занимаются пересказом на новый лад устаревших результатлв теории типов, в коьорой на даный момент изучать тупо нечего.
. Ну, то есть, ты можешь делать в них всё что можешь делать в любом компиляторе
Обычная типизированная лямбда тоже не представдяет особого интереса, пока мы еене расширим тем илииным образом. А макросы надо тем или иным образом огоаничивать. Макросы и системы типов - две противоположные стороны метапрограммирования, но в системах типов мы изучаем разные возможности расширения, а в макросах - возможности ограничения.
Ну ты дебил! Зачем ограничивать сами макросы чем-то кроме корректности полученного AST?!? Система типов ограничивает код, полученный при раскрутке макросов.
Видел, крайне негодная штука, ИМХО. Нет, серьёзно, куда ни ткни — просто ужас :)
произвольно мощная система типов строится на основе метапрограммирования.
А datatype это что? Макрос на Shen? Или таки часть реализации? Даже если макрос — ок, в реализацию макроса зашито всё это самодельное исчисление последовательностей (привет, 30-ые годы, вот уж где любовь к традициям) над символами, примитивными типами и функциями, никто ж не спорит что это можно сделать, просто разницы нет — что в макросе реализации, что в компиляторе её же.
Ну и (непротиворечивая!) мощность не засвидетельствована — ничего не написано.
«элементарные» это как? Вот HoTT демонстрирует, что, нет — очень «сложные» теории. Они вообще утверждают, что теория типов — подходящий язык для формальной математики (вплоть до действительного анализа).
Как изоморфизм карри-говарда придумали, так воз и поныне там
Зависимые типы (MLTT, CoC) были после, как и категорные интерпретации (Lambek, Seely). А что с линейными, модальными системами, содержанием ATTAPL, например? Что с категорными представлениями ADT и эффектов, в частности (функторы, алгебры, монады и т.п.)?
Протухший костыль сущетвующий с того момента как появиись атд
Ну да — есть ADT, можно генерировать свёртки/развёртки вообще и их частные случаи как в том примере. Только непонятно чем это плохо и как может протухать полезность таких возможностей.
а между тем мы сразу получим идеальный формальный фреймворк для исследования возможностей полного тайпчека до экспанда, что было бы охренительно круто
Почему нельзя просто сделать тайпчек на исходном AST до экспанда? Потому что у нас особые sophisticated макросы которые должны сами всё уметь? И вот тут бы хорошо примеры таких простейших тайпчекеров для тех же игрушечных языков из первых глав TAPL.
Почему нельзя просто сделать тайпчек на исходном AST до экспанда?
Потому что это алгоритмически неразрешимая задача. Даже биндинги переменных до экспанда установить - уже задача алгоритмически неразрешимая. Делать же до экспанда тайпчек - это вообще полый рокетсаенс о котором даже никто и не задумывается. Вот я и говорю о некотором упрощении (хотя бы биндинги трекать, так как без биндингов ты нифига не айпчекнешь) которое хотя бы укажет в какой области строить матаппарат для можелирования таких вещей, потому что опять же его и близко нет, только самые начальные наметки. Потому что это все сложно, это не тривиальщина и переписыванхе старых диссеров на новый лад
. Они вообще утверждают, что теория типов —подходящий язык для формальной математики (вплоть до действительного анализа
ЭТо язык логики первого порядка (с точностью до обозначений). С чего бы ему не быть подходящим для основанй математит, если эти оснлвания уже на нем изложены? Вот он классический пример - пересказали другими словами результат столетней давности и кричат о рокет саенсе. А даже если бы это и был новый язык - кому какое жело? Какая разница что там под капотом яву?
Mltt, coc - пересказ того что было очевидно с появлением изоморфизма, все связанное с теоркатом - опять же не более чем переформулирование известных фактов, линейные типы - ну вот это интересно, да, вообще подобные «неоьычные» типизации интересны, но опять же там сложно и этим занимается меньшинсвто, а большинство радостно занимается переписыванием одного и того же на разные лады, благо теоркат для этого идеальный инструмент. Маклейн крутится в гробу.
О каком source locatio ебалай, я про ошибки типов говорил
Ты сучка тупая, мне насрать что ты там говорил или думал, но для отладки макросов более чем достаточно source location. Если ты настолько тупая блядь, что не справляешься с элементарной отладкой, то тебе вообще нельзя программировать.
Потому что это алгоритмически неразрешимая задача.
А откуда такие проблемы? Это связано именно с подходом «берём нечто с макросами, ограничиваем их сверху вниз»? Потому что при индуктивном подходе с типами всё прекрасно разрешимо.
Я думал речь про проверку eDSL до компиляции в хост язык — если у последнего есть статическая система типов, то после компиляции тоже можно чего-то проверить, но не всё, да и синтаксическая структура сотрётся.
«Понятие топоса представляет в объективной категорной форме сущность логики высшего порядка» (с) Ловер. Внутренний язык элементарного топоса без ограничений это многосортная интуитивистская логика высшего порядка (которая превращается в классическую при допущениях). Это в случае 1-топосов. А HoTT вообще изучает внутренние языки (\inf, 1)-топосов, то есть n-категорное обобщение.
Ну и да — а какой толк? А какой толк от таблицы Менделеева?
Еще раз, неразрешим не толькл тайпчек, а даже связывание переменных (то есть до того как все макросы будут раскрыты нельзя сказать аакая переменная в каком контекте связана). Вот есть у тебя макрос (yoba x x), и ты никак не опркдклишь пока не раскроешь макрос - это иксы из внешнего контекста? Ии из внутреннего? Из разных или из одного?
Ты путаешь внутреный язык с внешним. Основания - это внешний язык, то есть метатеория. А метатеория hott может быть погружена в zfc (она вообще и погружена, по определению)
A set-based topos (i.e., one formed within a conventional set theory) must by definition satisfy all the axioms for a topos. Hence both the «internal» and the «external» constructions apply to such a topos. But when a topos is regarded as a possible foundation for mathematics, as in Chapter VI, only the internal concepts apply.
А метатеория hott может быть погружена в zfc
Теоретико-множественные модели есть, но, как бы, ZFC тут сбоку — непонятно, почему это оно должно занимать особое положение и участвовать в выявлении общезначимости с самой собой всего и вся и погружать всё и вся в самую себя же.
она вообще и погружена, по определению
Типа как «нет оснований кроме теории множеств» и далее по тексту.
мы сразу получим идеальный формальный фреймворк для исследования возможностей полного тайпчека до экспанда, что было бы охренительно круто - но никто этим не занимается, потому что сложно.
А тут про что? Изначально же вообще была речь про то что макросы «лучше» и «перспективнее» систем типов — хотелось бы увидеть как делаются на них хотя бы простейшие вещи уровня арифметически-булевых выражений (у термов всего два типа — числа и булевый, нужно следить чтобы сложные термы были well-formed относительно соответсвующих правил типизации — с обычной проверкой AST функцией это элементарно).
При чем тут модели? ZFC - это метатеория для hott (то есть hott формулируется на языке zfc), а теория не может быть сильнее метатеории. Так что ничего нового hott добавить не может.
—непонятно, почему это оно должно занимать особое положение
Вот и мне непонятно - hott и теоря множеств не отличаюься ничем кроме обозначений. Так зачем оно надо?
При чем тут модели? ZFC - это метатеория для hott (то есть hott формулируется на языке zfc)
При том что HOTT не формулируется на языке ZFC (никаких «по определению») — оно формулируется на языке (гомотопической) теории типов, то есть неформально, а потом уже — формальные модели в чём угодно, вместе с моделями чего угодно в теории типов, обратно (из их книжки — «Homotopy type theory is (among other things) a foundational language for mathematics, i.e., an alternative to Zermelo–Fraenkel set theory», «all of the constructions and axioms considered in this book have a model in the category of Kan complexes, due to Voevodsky [KLV12] (see [LS13b] for higher inductive types). Thus, they are known to be consistent relative to ZFC (with as many inaccessible cardinals as we need nested univalent universes).», «Theorem 10.5.11. In type theory with AC and a universe U, the cumulative hierarchy V is a model of Zermelo–Fraenkel set theory with choice, ZFC.», «Conway’s metatheorem would then correspond to the fact we have referred to several times that we can construct a model of univalent foundations inside ZFC (which is outside the scope of this book).»).
То есть, чтобы построить формальную систему для оснований и, например, реализовать её в виде пруф-ассистента никаких ZFC особо не нужно (сама ZFC — такая формальная система). Оно может понадобиться для выявления теоретико-доказательной силы новой теории.
Так что ничего нового hott добавить не может.
hott и теоря множеств не отличаюься ничем кроме обозначений. Так зачем оно надо?
По твоему, вообще теперь ничего кроме ZFC не может существовать? Потому как — допустим, появилось что-то новое (в смысле — язык для оснований), оно («по определению») «формулируется в рамках метатеории ZFC», «теория не может быть сильнее метатеории» — новое не нужно :)
Ну а разница между тем как с вещами работают в голой теории множеств, теории категорий, теории n-категорий, теории типов или HoTT очевидна, так что, например, вовремя перейти от множеств со структурой и биективных функций сохраняющих структуру к категории объектов и изоморфизмам может быть полезно, так же как и строить логические рассуждения исходя из соображений населённости и конструктивных построений, или выявить понятие гомотопического типа и уровня.
То есть макросы к системам типов прямого отношения таки не имеют, их заменить не могут и «более перспективная область исследований» в каком-то другом, особом смысле. Ну и слава богу.
Почему ты называешь элементарной задачу, которая даже в упрощенном варианте (без типизации, просто проверить корректность аст), неразрешима?
Потому что обычно не создают себе проблем (макросы, гигиена, биндинги) для героического их решения — просто разбирают AST, чекают его относительно правил типизации, всё разрешимо и правильно.
