Он у тебя НЕ тайпчекается до переписывания.

Можно и до переписывания что-то проверить. Например, если у macro тип A x B -> Code, то в макро-аппликации (macro x y) можно уже проверить типы x и y и их несовпадение будет обнаружено до раскрытия макроса и сообщено будет именно с упоминанием кода macro, а не раскрытого. Проверка раскрытого кода это уже третья стадия.

Хоть кто-то читает то, что написано, а не то, что ему воображение шепчет.

Там два синтаксических модуля CalcGrammar и IncGrammar пересылают между собой информацию.

Я не вижу где и какую информацию они пересылают. Давай ты сам сперва напишешь пример того, чего от меня хочешь (где два макроса пересылают и блаблабла), причем не результат (в твоей ссылке на гитхаб - не сами макросы, а вызов макросов), а именн ореализацию этих макросов, чтобы видно было - какова логика передачи данных и что ты именн охочешь.

Правильно. И мои слова ни разу этому не противоречат.

То есть никаокго тайпчека до раскрытия не происходит, верно? Ведь до раскрытия у тебя корректные типы термам не приписываются.

Автор языка пишет типизацию для своего языка.

Ну да. То есть проверка этих правил - не является тайпчеком. Т.к. тот факт что у тебя все типизировано с точки зрения этих правил ничего тебе не гарантирует. Ведь никто не гарантирует корерктность этих правил.

Что ты вообще под этим термином понимаешь?

Я тебе уже дал определение тайпчека. Общепринятое.

После раскрытия у меня снова происходит тайпчек.

Не снова - а первый раз.

Только цель не сказать пользователю об ошибке.

Именно в этом и состоит его цель. До тайпчека (то есть того что происходит у тебя после экспанда) мы не можем гарантировать корректность программы с точки зрения типов.

Весь тайпчек языка который использует пользователь происходит строго до раскрытия.

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

И то, что написано в секции typing занимается именно «приписыванием термам типов в соответствии с определенными правилами».

Ты не понял. После того как «типы приписаны термам в соответствии с определенными правилами» - у нас в программе не остается ошибок типов. В то время как у тебя если есть терм (yoba x y) и он как-то до раскрытия «типизирован» - то это не значит, что ошибок нет.

Именно это там и происходит. Либо будет выведен тип. Либо пользователю скажут, что он if использует не правильно.

Нет, там так не происходит. Никто тебе не гарантирует, что если тип выведен, то ошибки типов нет (до типизации - не гарантирует. после экспанда и типизации - уже гарантируют).

Ох. После раскрытия работает строго тот же код что и до раскрытия. Но по каким-то не ясным для меня причинам ты утверждаешь, что до раскрытия это не тапчек, а после тайпчек.

Все просто - во втором случае термы типизируются и гарантируется отсутствие ошибок типов. В первом случае - проверяются заданные макрописаталем инварианты и ничего не гарнатируется. Так ясно? То, что происходит в этих двух фазах - веши принципиально разные.

Так я про это и пишу уже несколько сообщений подряд.

Немного оговорился. Ни на что не влияет та информация, что получена до раскрытия. То есть этот шаг («тайпчек» до экспанда) можно просто опустить и ничего не изменится.

Не так. Некоторые программы, на которых проявляются ошибки автора языка.

Ага, но мы этого (что правила не совсем корректны) никогда не узнаем. Нам просто будет выведена ошибка типов и мы полезем ее исправлять - все.

Можно и до переписывания что-то проверить. Например, если у macro тип A x B -> Code, то в макро-аппликации (macro x y) можно уже проверить типы x и y и их несовпадение будет обнаружено до раскрытия макроса и сообщено будет именно с упоминанием кода macro, а не раскрытого. Проверка раскрытого кода это уже третья стадия.

Проверить-то можно, но это никак с тайпчеком не связано. То есть в твоем примере - мы проверим, что X и Y должны совпадать, а потом (после настоящего тайпчека) окажется что как раз они совпадать не должны, а если совпадают - то программа некорректна. То есть это, как я и говорил, просто небольшой сахарок для перехвата внутренних ошибок и более-менее нормального их вывода. Принципиально оно ничего не меняет. Тут ключевой момент - что мы обязаны чекнуть раскрытый код. А это АД и ПОГИБЕЛЬ, потому что искать ошибки типов в раскрытом коде - это пиздец.

Да, я все еще жду примера макроса Б, который по-разному будет раскрываться в зависимости от того, находится ли он внутри макроса А.

Там два синтаксических модуля CalcGrammar и IncGrammar пересылают между собой информацию.

Собственно, приведу пример такой же, как тебя на гитхабе:

#lang racket
(require (for-syntax syntax/parse))

(begin-for-syntax
  
  (define-syntax-class yoba1
    (pattern x:yoba2))
  
  (define-syntax-class yoba2
    (pattern x:yoba1)))

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

ключевой момент - что мы обязаны чекнуть раскрытый код. А это АД и ПОГИБЕЛЬ, потому что искать ошибки типов в раскрытом коде - это пиздец.

А в Лиспе нет тайпчека раскрытого кода, как ошибки ищутся - в рантайме на раскрытом коде?

Но в обычном лиспе, конечно, не получится - тут реализация основана на том, что в racket макросы раскрываются не последовательно - сперва каждая форма раскрывается до тех пор, пока head формы - макрос, а потом уже начинают раскрываться внутренние формы. То есть в данном случае (define-syntax-class yoba ...) раскрывается как-то так:

(begin (define-syntax yoba (make-syntax-class *тут любая метаинформация*))
       (define (id) (macro *этот макрос потом раскрывается в код 
                           проверки метаинформации и генерения чего там хочется на ее основе*)))

в результате когда будет выполняться проверка и кодогенерация вся метаинформация уже доступна.

А в Лиспе нет тайпчека раскрытого кода, как ошибки ищутся - в рантайме на раскрытом коде?

Для этого достаточно прогонять макрос в итоге через квазицитирование, тогда просто будет выделяться нужный терм в теле определения макроса, автоматом. То есть в этом случае все будет так, как если бы у нас это был не макрос, а обычная функция. Собственно, и и дебагер дебажит по коду не раскрывая его (то есть де-факто код раскрывается и исполняется раскрытый, но этого не видно).

Проверить-то можно, но это никак с тайпчеком не связано.

В TH и MetaML/MetaOCaml это делается тем же тайпчекером. То есть можно устроить 2(multi)-stage выполняя обычный тайпчек до и после каждой стадии раскрытия, при этом тайпчекер будет один и тот же.

То есть в твоем примере - мы проверим, что X и Y должны совпадать, а потом (после настоящего тайпчека) окажется что как раз они совпадать не должны, а если совпадают - то программа некорректна.

Не понял - либо то, либо другое, совпадать и не совпадать одновременно они не могут. Если macro : A x A -> Code, то есть типы X и Y должны совпадать, то, за счёт статики, мы отловим их несовпадение ещё до раскрытия. Иначе, если аппликация макроса хорошо типизирована, у нас макрос раскроется и нужно будет проверить уже сгенерированный код.

Вообще, для терма X типа T цитирование должно сохранять тип, то есть из X : T следует (quote X) : (Quote T), где quote : (T : Type) -> Quote T - специальная форма (она прерывает вычисления оставляя нам AST само по себе) и конструктор терма Quote, а Quote : Type -> Type - конструктор типа. И обратно - (splice (quote X)) == X, splice : {T : Type} -> Quote T -> T, то есть просто аккессор. В качестве модели:

record ⟪_⟫ {l} (T : Set l) : Set l where
  constructor ⟦_⟧
  field $_ : T

splice-quote-identity : ∀ {l} {T : Set l} → $ ⟦ T ⟧ ≡ T
splice-quote-identity = refl

data Expr : Set → Set₁ where
  -- ...
  _==_ : {T : Set} → Expr T → Expr T → Expr Bool
  if_then_else_ : {T : Set} → Expr Bool → Expr T → Expr T → Expr T
  -- ...

switch : {T : Set} → ⟪ Expr ℕ ⟫ → List (⟪ Expr ℕ ⟫ × ⟪ Expr T ⟫) → ⟪ Expr T ⟫ → ⟪ Expr T ⟫
switch _ [] def = def
switch m ((n , res) ∷ rest) def = ⟦ if $ m == $ n then $ res else $ switch m rest def ⟧

Если запретить стирание типов при цитировании (чего нет в TH), то вопрос - а останется ли вообще что-то проверять после раскрытия макроса? Мне почему-то кажется, что нет - макрос не может быть написан плохо (тайпчек кода макроса) и не может быть применён плохо (тайпчек его аппликации до раскрытия).

То есть это, как я и говорил, просто небольшой сахарок для перехвата внутренних ошибок и более-менее нормального их вывода.

Если бы это (полноценный тайпчекер) был просто «сахарок», то в TH можно было бы сделать switch только от int-ов руками во время раскрытия макроса, то есть руками обеспечить все нужные гарантии, однако, это сводится к ручному тайпчеку кода - практически невозможно. Сам посуди - макросу на вход поступает нечто, мы хотим сразу зафиксировать тип этого нечто, следовательно, мы должны вызвать тайпчекер отдав ему нечто и предполагаемую сигнатуру. Это явно не просто для любого реального языка и сколько-нибудь сложной системы типов (даже просто с ФВП и полиморфизмом). Можно конечно заменить тайпчек на рантайм-контракт - это проще.

Тут ключевой момент - что мы обязаны чекнуть раскрытый код.

Возможно, что и не должны - чекать уже будет нечего.

А это АД и ПОГИБЕЛЬ, потому что искать ошибки типов в раскрытом коде - это пиздец.

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

Если запретить стирание типов при цитировании (чего нет в TH)

Точно также, если сохранять структуру обычных и HOAS термов в типах, то сразу получается делать гетерогенные коллекции и вещи аналогичные case classes Scalы, иначе - не получается, стирание структуры термов либо просто не позволяет достичь необходимого, либо ломает строгость и статичность системы типов (TH генерирует кривой код).

Так во тименно что это все - не тайпчек!

Вот макрос который генерирует код печатающий одну и ту же строку n раз:

macro :: Int -> String -> ExpQ
macro 0 _ = [| return () |]
macro n s = [| putStrLn s >> $(macro (n - 1) s) |]

если его использовать так:

$(macro () "foo")

то будет

    Couldn't match expected type `Int' with actual type `()'
    In the first argument of `macro', namely `()'
    In the expression: macro () "foo"
    In the expression: $(macro () "foo")

кто это пишет как не тайпчекер?

Для этого достаточно прогонять макрос в итоге через квазицитирование, тогда просто будет выделяться нужный терм в теле определения макроса, автоматом. То есть в этом случае все будет так, как если бы у нас это был не макрос, а обычная функция. Собственно, и и дебагер дебажит по коду не раскрывая его (то есть де-факто код раскрывается и исполняется раскрытый, но этого не видно).

Я ничего не понял :)

Зачем? Посмотри какой срач развели анонимусы из-за этого говна... Бери нормальный язык, вроде Ruby(если любишь динамику) или Scala(если статику)... Если вдруг нужна скорость, то придется мучиться с С++.

А собрание ботанического сада не слушай. Кто-то создает ПО, а кто-то читает о нем умные книжки, которые пишут умные дядьки, толком программ и не писавшие...

Не понял - либо то, либо другое, совпадать и не совпадать одновременно они не могут.

Конечно. В этом вся соль.

Если macro : A x A -> Code, то есть типы X и Y должны совпадать, то, за счёт статики, мы отловим их несовпадение ещё до раскрытия.

Так то что типы должны совпадать - это макрописатель написал. То что он так написал - ничего не значит, это никак не связано с корректностью кода. Он все что угодно мог написать. Повернем пример немного по-другому, вот макрописатель написал макрос if, но вместо равенства задекларировал неравенство типов. Что получится в итоге? Да очень просто. Если «предварительный» чекер пропустит макрос - то не пропустит реальный (т.к. в раскрытом коде разные типы там, где они должны быть одинаковыми), а если написать макрос так, что арскрытый код мог бы чекнуться - то его не пропустит «предварительный» чекер.

Мне почему-то кажется, что нет - макрос не может быть написан плохо (тайпчек кода макроса)

Конечно, может быть. Тот факт, что код макроса тайпчекается, говорит лишь о том, что макрос корректно отработает - то есть сгенерирует некое АСТ. Но это не гарантирует, что этот АСТ будет корректно типизирован, такой факт можно доказать только с теорем прувером. Либо следует ограничить код тела макроса так, чтобы он не был тьюринг-полон. А квазицитирование уже тьюринг-полно само по себе.

Но даже если вдруг мы добавили прувер и гарантировали что раскрытый АСТ будет типизирован в соответтсвии с семантическим правилом - учитывая свободное задание правил, мы можем добавить противоречивые правила и вывести на типах что угодно. В результате опять раскрытая программа не сможет быть корректно типизирвоана.

Если бы это (полноценный тайпчекер)

А где ты увидел полноценный тайпчекер? Там его нет. Там просто пользовательский код, котоырй смотрит типы термов и что-то делает на его основании.

Возможно, что и не должны - чекать уже будет нечего.

Будет, без прувера - будет.

(а я настаиваю, что этого не случится вообще)

Только с прувером.

среда покажет тебе код макроса, код его использования и раскрытый код с сообщением что не так в последнем.

Я пользователь макроса, я не хочу смотреть на раскрытый код. Хорошая макросистема от плохой тем и отличается, что пользователю макроса не нужно лезть в дебри его реализации. В противном случае макросистема просто тупо _не нужна_ - те профиты которые она дает не стоят затруднений при отладке, потому что искать ошибки в раскрытом коде - это будет посложнее отладки сегфолтов в сишке.

кто это пишет как не тайпчекер?

Это тайпчек тела макроса (первой фазы) мы же говорим о тайпчеке 0 фазы. То, что такое можно в TH, лишь из-за того что нельзя делать $() внутри $(). Чтобы можно было тайпчекать макрос до экспанда, надо, чтобы у макроса был какой-то такой тип: macro : Exp G A B C ... -> Exp F A B C .... - A B C - формальные параметры, по которым макрос может быть полиморфен, а F/G - задают неявную ф-ю, которая связывает типы в форме вызова с типами в теле. Ирл типы F/G могут выглядеть как-то так: F A B C = If Bool (App (B -> C) B) C. То есть фактически типы макроса декларативно описывают, что парсится и в какое дерево парсится, а тайпчекер должен доказать, что результирующее дерево будет всегда корректно - собственно этим доказательством и будет сама реализация макроса (описание того КАК парсится) в пруф ассистансе.

Вообще, если ограничиться достаточно гибким квазицитированием и сохранять определенный стиль (например писать макросы примерно так, как их пишу я :)) то доказательство должно быть достаточно простым.

Я не вижу где и какую информацию они пересылают.

Они ссылаются друг на друга. И проверяют наличие имен правил.

Код того как они это делает есть в репозитории. Только из-за того что он разбит на несколько фаз его пришлось размазать по коду. На фазы его разбивать пришлось по тому, что сначала все синтаксические модули должны собрать имена внутри себя. На следующей фазе они ходят по импортируемым модулям и достают оттуда имена, чтобы проверить то, что в правилах всё в порядке и вывести типы узлов АСТ.

Плюс сюда добавляются фазы компиляции самого немерла. Ибо там ровно те же проблемы. Только еще сложнее.

То есть никаокго тайпчека до раскрытия не происходит, верно? Ведь до раскрытия у тебя корректные типы термам не приписываются.

Происходит. Приписывается.

Ну да. То есть проверка этих правил - не является тайпчеком. Т.к. тот факт что у тебя все типизировано с точки зрения этих правил ничего тебе не гарантирует. Ведь никто не гарантирует корерктность этих правил.

Сказал адепт динамической типизации, где вообще даже теоритически ничего гарантировать нельзя. Меня реально прикалывают эти двойные стандарты. В своём любимом лиспе не замечаешь полнейшее отсутствие гарантий.

В моей системе называешь фатальным недостатком возможность накосячить при описании типов. Даже не смотря на то, что это косяк с вероятность 99,999% будет пойман при попытке что-то скомпилировать.

Именно в этом и состоит его цель. До тайпчека (то есть того что происходит у тебя после экспанда) мы не можем гарантировать корректность программы с точки зрения типов.

И до. И после. Работает строго один и тот же код.

Более того переписывание будет происходить итеративно пока есть что переписывать. Те получается у меня совсем нет тайпчека. Остается вопрос, что же выводит сообщения об ошибках и приписывает типы термам.

Так во тименно что это все - не тайпчек! Это просто проверка заданных автором макроса инвариантов.

Это и есть тайпчек. Ибо типы это не более чем инварианты.

Ничего общего с тайпчеком не имеющая и никаких гарантий корректности и отсутствия ошибок не дающая.

Ты так говоришь, как будто такие системы типов есть. Так их нет. Никакая система типов не гарантирует то, что программа делает, то, что нужно.

Вот после экспанда - происходит тайпчек, то есть проверка того, можно ли программе приписать корректные типы.

Так вызывается строго тот же код. Но раньше это был не тайпчек, а теперь этой тапчек. Я тебя совсем перестал понимать.

Так ясно? То, что происходит в этих двух фазах - веши принципиально разные.

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

Почему ты говоришь что один и тот же код в одной фазе не тапчек, а во второй тапчек?

Я тебя не понимаю.

Немного оговорился. Ни на что не влияет та информация, что получена до раскрытия. То есть этот шаг («тайпчек» до экспанда) можно просто опустить и ничего не изменится.

Все изменится с точностью до неузнаваемости. Во время типизации происходит распространение информации. Те мы узнаем, что вот этот набор букв класс. А вон тот - метод. Причем не метод вообще, а конкретный из десятка перегруженных. И очень многое другое.

Без этого переписывание невозможно. Просто по тому, что мы не будем знать, во что переписывать.

После переписывания снова вызывается типизатор. Ибо переписыватель кроме того что использует готовые узлы создает новые. Где типы еще не прописаны. И там тоже происходит распространение информации. Ибо без этой информации дальше переписавать нельзя.

Ты все это не понимаешь по тому, что в лиспе этого нет. А оно надо. Ибо без этого банально не сделать проверку того что функция существует.

написал макрос if, но вместо равенства задекларировал неравенство типов. Что получится в итоге?

Вообще-то может быть два «хороших» if-а, такой:

if₁ : {A : Set} → ⟪ Expr Bool ⟫ → ⟪ Expr A ⟫ → ⟪ Expr A ⟫ → ⟪ Expr A ⟫
if₁ = {!!}

и такой:

if₂ : {A B : Set} → ⟪ Expr Bool ⟫ → ⟪ Expr A ⟫ → ⟪ Expr B ⟫ → ⟪ Expr (A ⊎ B) ⟫
if₂ = {!!}

Оба варианта «хорошо» реализуемы.

Но допустим, что сигнатура вообще другая, тогда

«предварительный» чекер пропустит макрос - то не пропустит реальный (т.к. в раскрытом коде разные типы там, где они должны быть одинаковыми), а если написать макрос так, что арскрытый код мог бы чекнуться - то его не пропустит «предварительный» чекер.

^ это невозможно. Есть сигнатура if которая требует составить из выражений _параметризованных_ своими типами другое выражение тоже _параметризованное_ типом с _зависимостью_ от типов исходных цитированных выражений, кроме того, конструкторы этих выражений должны чисто аппликативно сочетаться и нужно ещё чтобы правила type formations были соблюдены. Главные вопросы - что такое «выражение» и как «правила type formations будут соблюдены». Если выражение - HOAS, то типизация получается автоматом (например, не пишется чекер, HOAS наследует свойства своего языка). А иначе будет настоящий multi-stage и выражением будет само AST языка - генерирующий код и сгенерированный код типизируются по _одним и тем же правилам_. Определение if которое может составить плохо-типизированный код само по себе плохо-типизированно и не проходит тайпчек (тайпчек определения макроса как обычной функции, отдельно ещё должен быть тайпчек применения такой функции в макроаппликации).

Только с прувером.

Язык со сколько-нибудь богатой (и непротиворечивой) системой типов сам по себе прувер, причём, не отдельно язык + прувер, а непосредственно прувер в смысле CH isomorphism. Даже хаскель - прувер (но противоречивый) на котором можно доказывать простенькие теоремы.

Либо следует ограничить код тела макроса так, чтобы он не был тьюринг-полон.

Строгой нормализацией можно обеспечить непротиворечивость, но при этом потерять Тьюринг-полноту, да.

Но даже если вдруг мы добавили прувер и гарантировали что раскрытый АСТ будет типизирован в соответтсвии с семантическим правилом - учитывая свободное задание правил, мы можем добавить противоречивые правила и вывести на типах что угодно. В результате опять раскрытая программа не сможет быть корректно типизирвоана.

А никаких «свободных правил» быть не должно, должна появится цикличность кодогенерации в рамках одного языка с такой-то «хорошей» системой типов.

В противном случае макросистема просто тупо _не нужна_ - те профиты которые она дает не стоят затруднений при отладке, потому что искать ошибки в раскрытом коде - это будет посложнее отладки сегфолтов в сишке.

То есть не нужна именно в статике? А в гомоиконной динамике зачем это нужно? Как-то любой код из конструкторов ADT сам по себе DSL и редко когда имеет какое-то нетривиальное отображение в алгоритмический код целевого языка выполняющийся, скажем, на порядок быстрее обычной обработки такого ADT функциями.

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

В немерле я тоже могу два класса написать. И они тоже будут друг о друге знать.

Но только по тому, что этот код уже написан в компиляторе.

А теперь давай то же самое, но для своих макросов. Чтобы они прошлись по тому коду, что в них вложен. Собрали информацию. После чего передали ее друг другу. И уже на основе этой информации и той, что собрали на первой фазе сгенерировали код.

А потом представь, что появляется еще один макрос, который на эту информацию влияет. Всё. Приехали. Императив склеивает ласты, отбрасывает коньки и ползёт на кладбище.

Вот тут вроде всё правильно. Только пруф ассистант = сам язык (по-челябински :)).

Они ссылаются друг на друга. И проверяют наличие имен правил.

Это я понял и привел пример таких же макросов, которые ссылаются друг на друга и проверяют наличие соответствубщих классов.

Происходит. Приписывается.

Ключевой момент был - «корректные типы». У тебя корректность типов до экспанда никак не гарантируется.

Сказал адепт динамической типизации, где вообще даже теоритически ничего гарантировать нельзя. Меня реально прикалывают эти двойные стандарты. В своём любимом лиспе не замечаешь полнейшее отсутствие гарантий.

Так и у тебя предварительный тайпчек точно так же ничего не гарантирует. Получается динамика та же.

В моей системе называешь фатальным недостатком возможность накосячить при описании типов. Даже не смотря на то, что это косяк с вероятность 99,999% будет пойман при попытке что-то скомпилировать.

Фатальный недостаток то, что придется копаться в раскрытом коде, чтобы узнать - где ошибка.

Ты так говоришь, как будто такие системы типов есть. Так их нет. Никакая система типов не гарантирует то, что программа делает, то, что нужно.

Есть такие которые, например, гарантируют, что я не сложу число со строкой. У тебя тайпчек до экспанда никаких таких гарантий не дает.

Почему ты говоришь что один и тот же код в одной фазе не тапчек, а во второй тапчек?

потому что в этих фазах происходят совершенно разные вещи и проверяется исполнение разных семантических правил. В первом случае проверяются правила заданные макрописаталем, а во втором - правила хост-языка.

Все изменится с точностью до неузнаваемости. Во время типизации происходит распространение информации. Те мы узнаем, что вот этот набор букв класс. А вон тот - метод. Причем не метод вообще, а конкретный из десятка перегруженных. И очень многое другое.

Но это все не важно, т.к. мы можем сперва все раскрыть - а потом уже узнавать, что там класс, а что нет.

Ты все это не понимаешь по тому, что в лиспе этого нет. А оно надо. Ибо без этого банально не сделать проверку того что функция существует.

Странно, но экспандер в internal definition ровно этим (проверкой того, что функция существует) и занимается. Как же ж так? Если бы нельзя было сделать такую проверку, то не получилось бы взаимно-рекурсивные функции определять. Потому что при экспанде первой функции экспандер бы нашел несвязанную переменную (ведь вторая функция определяется ниже) и кинул бы эррор.

Вообще-то может быть два «хороших» if-а, такой:

Это ясно, но допустим в хост-языке нету объединением. В общем - суть ты понял.

^ это невозможно.

С чего вдруг?

Есть сигнатура if которая требует составить из выражений _параметризованных_ своими типами другое выражение тоже _параметризованное_ типом с _зависимостью_ от типов исходных цитированных выражений

Ну да. ключевое слово - зависимость, которая вообще говоря произвольна. Чекеру надо доказать, что тело макроса сохраняет эту зависимость. Для этог осистема типов должна уметь работать с зависимыми типами.

То есть еще раз - тип функции это T1 -> T2, где T1 и T2 это на самом деле большие такие длинные типы, каждый из которых задает полную структуру АСТ. T1 - структура АСТ на входе, Т2 - структура АСТ на выходе. АСТ могут быть совершенно произвольными. Далее у нас есть функция, которая АСТ принимает и АСТ возвращает, так вот нам надо доказать, что это функция генерирует именно такой АСТ, структура которого указана в типе T2. Это задача неразрешимая, т.к. АСТ может зависеть, например, от правильности теоремы ферма. Типы вообще могут быть такими: T1 = X : Int, T2 = f(X), x - любая целочисленная функция. И доказывай теперь, что тело макроса считает именно это функцию. Самое веселое еще, когда у нас макрос раскрывается в АСТ, вводящий новые переменные.

Строгой нормализацией можно обеспечить непротиворечивость, но при этом потерять Тьюринг-полноту, да.

Угу, но проблема в том, что, как я уже говорил - даже банальное квазицитированье тьюринг-полно и доказательство корректности построенного АСТ в сколько-нибудь нетривиальных случаях уже может потребовать кучи лишнего кода.

А никаких «свободных правил» быть не должно

Тип макроса - это и есть семантическое правило. Тип макроса мы же свободно задаем? Вот. И если вдруг эти правила противоречивы - система типов накрывается.

То есть не нужна именно в статике?

Да нет при чем тут типизация? Ненужна система, при которой приходится отлаживать раскрытый код пользователю макроса. Такое может быть как в динамике (в каком-нибудь общелиспе) так и в статике. Просто в динамике макросистему все-таки _можно_ сделать нормально, а вот в статике - нет. Ну или жесткие ограничение, как уже говорилось выше. Но они очень негативно скжаутся на вербозности макросов, в результате инструмент станет неудобен, а неудобный инструмент - снова не нужен.

В немерле я тоже могу два класса написать. И они тоже будут друг о друге знать.

Ну ты ведь именно это и сделал. Вместо того чтобы написать обменивающиеяся информацией макросы.

А теперь давай то же самое, но для своих макросов.

Ты не понял. define-syntax-class - это обычный макрос. Я даже пояснил, как он работает.

Чтобы они прошлись по тому коду, что в них вложен. Собрали информацию. После чего передали ее друг другу. И уже на основе этой информации и той, что собрали на первой фазе сгенерировали код.

Именно так все и происходит. Сперва генерируется метаинформация для обоих классов, потом на основе этой метаинформации генерируется код.

А потом представь, что появляется еще один макрос, который на эту информацию влияет. Всё. Приехали.

Как именно влияет? Не вижу никаких сложностей и не понимаю, в чем проблема.

Это я понял и привел пример таких же макросов, которые ссылаются друг на друга и проверяют наличие соответствубщих классов.

И где там код проверки? Его там нет. Его кто-то написал за тебя.

Фатальный недостаток то, что придется копаться в раскрытом коде, чтобы узнать - где ошибка.

В 99.999% не придется.

потому что в этих фазах происходят совершенно разные вещи и проверяется исполнение разных семантических правил. В первом случае проверяются правила заданные макрописаталем, а во втором - правила хост-языка.

У меня нет хост языка. Понимаешь? Вообще нет.

Н2 это язык описания языков. И языки в Н2 раскрываться не будут. Если это конечно не сахар для Н2.

Правильность тайпчека на 100% зависит от того кто этот тапчек пишет.

Так что все твои претензии можно переправить автору любого компилятора. Где гарантия, что авторы хаскеля не накосячили с тайпчеком?

Её нет.

Но это все не важно, т.к. мы можем сперва все раскрыть - а потом уже узнавать, что там класс, а что нет.

Мы не можем. Ибо переписывание в общем случае зависит от той информации, которую мы получили от тапчека. Ты вообще читаешь, что я пишу? Или просто трындишь?

Странно, но экспандер в internal definition ровно этим (проверкой того, что функция существует) и занимается. Как же ж так? Если бы нельзя было сделать такую проверку, то не получилось бы взаимно-рекурсивные функции определять. Потому что при экспанде первой функции экспандер бы нашел несвязанную переменную (ведь вторая функция определяется ниже) и кинул бы эррор.

Это по тому, что этот код уже написан и захардкожен в компилятор.

Для этог осистема типов должна уметь работать с зависимыми типами.

Да. Но даже в обычном id :: a -> a есть зависимость - это id : П(a : Type).a.

Далее у нас есть функция, которая АСТ принимает и АСТ возвращает, так вот нам надо доказать, что это функция генерирует именно такой АСТ, структура которого указана в типе T2.

Чем это отличается от любой другой функции которая принимает и возвращает любые другие (co)inductive types с зависимостью? Такие функции и лежат в основе языков с зависимыми типами которые умеют доказывать что-то интересное.

Это задача неразрешимая, т.к. АСТ может зависеть, например, от правильности теоремы ферма.

Если она конструктивно и тотально (алгоритмически разрешимо) доказана (написана как функция) в другом месте - пусть используется, это ничему не помешает.

Типы вообще могут быть такими: T1 = X : Int, T2 = f(X), x - любая целочисленная функция. И доказывай теперь, что тело макроса считает именно это функцию.

f - любая целочисленная функция?

foo : {f : ℤ → ℤ} → (x : ℤ) → f x

не пишется вообще, даже как аксиома не добавляется.

Самое веселое еще, когда у нас макрос раскрывается в АСТ, вводящий новые переменные.

Вроде (aif (compute ...) (lexically-updated-form ... it ...))?

Угу, но проблема в том, что, как я уже говорил - даже банальное квазицитированье тьюринг-полно

Это, наверно, зависит от самого целевого языка, он сам может быть не Тьюринг-полон. Квазицитированье тут само по себе ничего не меняет. А в обычном языке с метасистемой макросы по смыслу должны быть Тьюринг-полными, эффектно-полными и уметь делать то же что и обычный код.

доказательство корректности построенного АСТ в сколько-нибудь нетривиальных случаях уже может потребовать кучи лишнего кода.

Ну тип макроса это его спецификация, а доказательство корректности согласно спецификации - сама реализация макроса.

И если вдруг эти правила противоречивы - система типов накрывается.

Накрывается бред который ей не соответствует, система типов просто работает.

Ну ты ведь именно это и сделал. Вместо того чтобы написать обменивающиеяся информацией макросы.

Я именно что написал обменивающиеся информацией макросы. За каждым syntax module стоит макрос. И они обмениваются информацией.

Именно так все и происходит. Сперва генерируется метаинформация для обоих классов, потом на основе этой метаинформации генерируется код.

Покажи код, который это делает.

Как именно влияет? Не вижу никаких сложностей и не понимаю, в чем проблема.

По тому, что ты этого никогда в жизни не делал. И даже не понимаешь про что разговор. Это ясно видно из твоих ответов.

не пишется вообще

Поясню - какой-нибудь 5 (типа ℤ) не может служить типом, терм типа 5 это абсурд.

Есть вот такие тезисы на тему обобщённого программирования:

http://dreixel.net/research/pdf/thesis.pdf

Метапрограммированию, правда, уделено всего пара абзацев:

Stage genericity A metaprogram is a program that writes or manipulates other programs. In combination with some form of staging or splicing, this allows for programs that manipulate themselves, or perform computations during type checking. Template Haskell [Sheard and Peyton Jones, 2002] is an implementation of metaprogramming in GHC; Agda has a reflection mechanism with similar expressiveness.

Metaprogramming mechanisms can be very expressive and allow for defining generic programs in all the senses of this section. For instance, one can define a Template Haskell program that takes a container type and then defines an appropriate length function for that type. This could in principle be done even in a non-polymorphic language. However, encoding generic behavior through metaprogramming is a tedious and error-prone task, since it involves direct manipulation of large abstract syntax trees.

И где там код проверки?

Он в определении макроса define-syntax-class. А где у тебя код проверки? Нету. Ты просил показать то, что у тебя в примере на гитхабе - я показал даже больше. Когда ты код проверки покажешь - то и я тебе покажу. Поскольку не совсем ясно, что ты от этого кода проверки ожидаешь. Кстати, кроме кода проверки я жду макрос Б, который раскрывается по-разному в зависимости от того, находится ли он внутри А. Но, видимо, не дождусь - для немерле с ТАКИМ-ТО тайпчекером это неразрешимая задача.

В 99.999% не придется.

А чего не 98.888%? Как вероятность измерил?

У меня нет хост языка. Понимаешь? Вообще нет.

тьфу блять, опять оговорился. Целевой, конечно же. Хост-язык у тебя - немерле.

Правильность тайпчека на 100% зависит от того кто этот тапчек пишет.

Охуенная у тебя статическая типизация. Нахуя она тогда нужна, если я случайно сажаю ошибку в своем ЙОБА ТИПИЗИРОВАННОМ ЙОБА ДСЛЕ и вся типизация идет по пизде?

Так что все твои претензии можно переправить автору любого компилятора. Где гарантия, что авторы хаскеля не накосячили с тайпчеком?

Видимо я не совсем понял, как вы позиционируете н2. Я предполагал, что это средства для dsl-driven development - то есть при решении задачи пишем дсли для решения подзадач, выражаем удобно эти подзадачи и компонуем дсли в итоговое решение - среда заботится о том, чтобы легко дсли написать, легко скомпоновать и легко потом это все поддерживать. Ты же сейчас говоришь про написание компиляторов хаскиля - да, для них корректность чекера доказывать не надо. Потому что над этим компилятором постоянно люди работают, куча людей ищет баги, пишет багрепорты, все фиксят, так что чекер предполагается «правильынм по умолчанию». Но никто не будет писать компиляторы хаскиля при помощи н2, их будут писать так, как и писали. С другой стороны, н2 можно было бы использовать в виде платформы для описанного выше dsl-driven development - но тут дсл тебе не будут тестировать на халяву десятки (если не сотни) тысяч человек. И вероятность того, что в чекере будет куча ошибок - близка к единице. Это только написанный чекер - нам нет времени его отлаживать, использовать надо. Если тратить время на отладку - да лучше уж не ебать мозги и безо всяких дслей решить задачу.

Мы не можем. Ибо переписывание в общем случае зависит от той информации, которую мы получили от тапчека.

Так это некорректная информация, нам ее все равно надо выкинуть.

Это по тому, что этот код уже написан и захардкожен в компилятор.

Дебил, а у тебя базовый алгоритм тайпчекера в компилятор не захардкожен? я хуею просто.

Поясню - какой-нибудь 5 (типа ℤ) не может служить типом, терм типа 5 это абсурд.

Типом может быть любой объект, никакого абсурда. 5 ни чем не хуже любого другого типа.

Небольшое пояснение: с тчоки зрения метапрограммирования тип - это _любой набор данных_ связанный с идентификатором в данном лексическом контексте. Так уж принято что большая часть типов - это просто символы, как 'Int например.

Да. Но даже в обычном id :: a -> a есть зависимость - это id : П(a : Type).a.

Ну не надо софистикой заниматься. Речь идет именно о неразрешимых зависимостях.

Чем это отличается от любой другой функции которая принимает и возвращает любые другие (co)inductive types с зависимостью?

Не понял, а почему оно должно отличаться?

Если она конструктивно и тотально (алгоритмически разрешимо) доказана (написана как функция) в другом месте

Ну так о чем и речь - макросы надо будет писать с прувером типа агды.

f - любая целочисленная функция?

Да, конечно.

не пишется вообще, даже как аксиома не добавляется.

Естественно, не пишется - она ведь целочисленная функция в метатеории, а ты пытаешься объявить ее целочисленной ф-й в теории :)

Вроде (aif (compute ...) (lexically-updated-form ... it ...))?

Да не не, это ж анафора. Тут нарушение гигиены и т.п., а может быть банальны макрос и не анафорический, но раскрывающийся в определение, ну например: (yoba x) -> (define x 1) (не надо исктаь смысла в примере, просто чтобы пояснить). Здесь макрос добавит переменную х в лексический контекст и в типе (то есть в семантическом правиле макроса, а правила мы задаем через типы) должно быть указано «положить в контекст переменную x». Ведь чекер когда будет дальше чекать должен знать что переменная х есть в контексте - но до экспанда. То есть ему придется узнавать это из типа. Короче у нас тип будет выглядеть как нечто среднее между обычным семантическим правилом (как при описании типизации) и декларативным описание преобразования АСТа как в syntax-rules.

Это, наверно, зависит от самого целевого языка, он сам может быть не Тьюринг-полон.

Угу. А квазицитирование меж тем БУДЕТ тьюринг полно :) Например, если взять язык с функциями, но без лямбд и без фвп, без циклов и без рекурсии, но с условным оператором, то он не будет тьюринг-полон, а макросы на квазицитировании - будут, т.к. им экспанд обеспечивает фвп и рекурсию (явную в том числе).

Накрывается бред который ей не соответствует, система типов просто работает.

Что значит «просто работает», если она противоречива? Дело просто в том, что в ней при желании можно будет корреткно чекнуть некорректный терм.

Ну тип макроса это его спецификация, а доказательство корректности согласно спецификации - сама реализация макроса.

Ну да, в пруверах примерно так и есть. Однако, у меня нету никакого желания пользоваться макросистемой, которая заставляет ДОКАЗЫВАТЬ корректность макроса через прувер - в любом случае количество кода резко возрастет. то есть я, безусловно, поигрался бы с такой системой, это интересно, прикольно, классно и т.п. - никто тут не спорит, но я бы не стал использовать ее на практике - в этом случае любую задачу будет проще решить без выебонов и метапрограммирования. Инструмент должен быть удобен - абстрактной «мощности» и «выразительности» мало.

Я именно что написал обменивающиеся информацией макросы. За каждым syntax module стоит макрос. И они обмениваются информацией.

Где эти макросы и где их определение?

Покажи код, который это делает.

Он в define-syntax-class. Но я вообще говоря тебе написал как этот макрос раскрывается - там 4 строчки. Вот это обмен данных и есть (всмысле эти 4 строчки - логика обмена данных, а логику самого макроса - то етсь добавление данных в контекст и трансформация АСТ я заскипал).

По тому, что ты этого никогда в жизни не делал.

Делал и не раз. И не встретил никаких проблем. ЧЯДНТ? Ты похож на человека, который аргументирует сложность одевания штанов тем, что они одеваются через голову.

Охуенная у тебя статическая типизация. Нахуя она тогда нужна, если я случайно сажаю ошибку в своем ЙОБА ТИПИЗИРОВАННОМ ЙОБА ДСЛЕ и вся типизация идет по пизде?

Остается понять, как же ты что-то пишешь. Ибо в случае с лиспом всё в 100% случаев идет в том направлении.

Дебил,

Дебил у нас тут ты. Уже сколько я тебе пытаюсь донести что такое Н2, а ты все со своими голосами в голове разговариваешь.

Ладно. Пора прекращать. Как выяснилось ничего интересного от лисподрочеров узнать нельзя. Что не удивительно. Ведь сколько я не общался с любителями динамической типизации, всегда наблюдал серьезные проблемы с логическим мышлением.

а у тебя базовый алгоритм тайпчекера в компилятор не захардкожен? я хуею просто.

Нет. Не захардкожен. Но только из-за того что у тебя отсутствует логическое мышление ты всё равно не поймешь как это работает.

Остается понять, как же ты что-то пишешь. Ибо в случае с лиспом всё в 100% случаев идет в том направлении.

Так я не против отсутствия статический типизации. Я против отсутствия статической типизации сопряженной с усложнением написания макросов для нее.

Нет. Не захардкожен.

Ты совсем охуел уже. Ты сам выше говорил что у тебя есть захардкоженный алгоритм, который можно расширить в узлах-типизаторах.

Но только из-за того что у тебя отсутствует логическое мышление ты всё равно не поймешь как это работает.

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

Как выяснилось ничего интересного от лисподрочеров узнать нельзя.

Как будто можно от немерлеблядей. Сколько с ними не общался - любые вопросы игнорируются, предложения продемонстрировать ЙОБА-ФИЧИ на примере игнорируются, предложения объяснить как что реализовано в общих чертах игнорируются, в ответ раздается только кукареканье типа «можнасделать!!1!» (любые просьбы продемонстрировать - игнорируются) и рекламные проспекты уровня «если вы будете исопльзовать н2, то волосы на вашем лобке будут длинные и шелковисты». Естественно, вопросы типа «за счет чего?» - игнорируются.

И не надоело лиспобляди своё поведение другим приписывать? Сам то, что показал? А ничего. Все вопросы проигнорировал. Где императивный типизатор? А нету. Ибо у лиспобляди ничего нет. На мой можно посмотреть, открыв код на гитхабе. Так что в отличие от тебя я знаю, о чем говорю.

Уважаемые лиспо- и немерле- бляди

Успокойтись уже. Лисп не нужен, Немерле перегружен, а н2 - вообще какая-то неведомая хуйня.

Форт хайль олл?

Все вопросы проигнорировал.

Я на все вопросы ответил, в отличии от тебя - на все. И все твои реквесты (типа привести то то и то) - выполнил. Все пруфы есть в прошлом треде. А ты, дебил, даже два макроса написать не смог.

Где императивный типизатор? А нету. Ибо у лиспобляди ничего нет.

Ты что, тупой? Я тебе привел пример и макросов и код в который они раскрываются. А вот ты кода не привел, только «можно посмотреть на гитхабе». Где на гитхабе? Ссылку ты дал? Где этот код-то чудесный? Реализацию define-syntax-class тоже можно посмотреть в репозитории, если уж на то пошло.

Типом может быть любой объект, никакого абсурда. 5 ни чем не хуже любого другого типа.

Я уже говорил - нам нужно (ну, то есть, мы это тут обсуждаем) сделать метасистему (multi-stage) в рамках языка с такой-то хорошей системой типов. В рамках такого языка - ? : 5 это бессмысленно, что можно в любом агда-хаскеле проверить. Если делать метасистему и при этом ломать систему типов, то это уже не интересно.

Однако, у меня нету никакого желания пользоваться макросистемой, которая заставляет ДОКАЗЫВАТЬ корректность макроса через прувер - в любом случае количество кода резко возрастет

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

в этом случае любую задачу будет проще решить без выебонов и метапрограммирования

И так обычно и происходит в большинстве языков.

? : 5 это бессмысленно

Это впонле осмысленно.

Если делать метасистему и при этом ломать систему типов, то это уже не интересно.

Не понял - зачем ломать систему типов? Иметь тип «5» - это банальный вопрос удобства. В любом случае, если система типов не говно, мы сможем закодировать числа через Nat = Zero | Succ Nat и соответствующие операции. И вообще, все что надо, сможем закодировать. И задать произвольные функциональные зависимости. В данном случае обычные объекты типа «5» в качестве типов - это просто некий синтаксических сахарок, который позволяет писать строчку понятного когда вместо 100 строк непонятного type-level-говна, имеющего тот же смысл.

Я уже говорил - нам нужно (ну, то есть, мы это тут обсуждаем) сделать метасистему (multi-stage) в рамках языка с такой-то хорошей системой типов.

Неверно. Мы обсуждаем возможность произвольного расширения этой системы типов, что необходимо предполагается наличием метасистемы.

И так обычно и происходит в большинстве языков.

Потому что в большинстве языков просто _нету_ нормального метапрограммирования. Как можно использовать инстумент, которого нет? Верно - никак :)

Ну вот если взять агду в пример - где там _резко_ возрастает количество кода?

Э... везде? Более-менее адекватно выглядят только факториалы. Доказательство корректности чуть менее чем всегда в разы (часто - в десятки и сотни раз) больше самой реализации. Другое дело, что подобные вещи на агде просто не пишут - ну не осилит никто такое.

? : 5 это бессмысленно

Вообще тут надо понимать так - значения фазы n+1 (метатеории) являются типами для фазы n (теории). Вопрос в том, какова выразительность нашей метатеории. В любом адекватном случае она все равно тьюринг-полна, так что мы что угодно выразим. Добавление списков, чисел и т.п. в явном виде не изменит выразительность - это то же самое, как в реальных ЯП мы добавляем списки, числа и т.п. к лямбда-исчислению, вместо того чтобы кодировать их на лямбдах.

Это впонле осмысленно.

Не понял

Тогда давай так - озвучь терм типа пять. Если множество термов данного типа пусто, то тип это, с точностью до, ⊥ - наличие термов такого типа автоматически означает противоречивость системы (ты можешь доказать абсурд).

Мы обсуждаем возможность произвольного расширения этой системы типов, что необходимо предполагается наличием метасистемы.

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

Доказательство корректности чуть менее чем всегда в разы (часто - в десятки и сотни раз) больше самой реализации.

Доказательство корректности = реализация. Если ты пишешь функцию с каким-нибудь не очень сложным типом, как в хаскеле, то она не будет намного сложней такой же функции в хаскеле. Типы макросов как раз не очень сложны, никто не пишет маросов код которых, с точность до, есть доказательство FLT :)

значения фазы n+1 (метатеории) являются типами для фазы n (теории)

[citation needed].

Макросы (сплайсящиеся функции превращающие код одной стадии в код другой, слова теория/метатеория я бы не стал использовать) превращают (цитированные) значения из универсума U(n) типизированные (цитированными) значениями из универсума U(n+1) снова в значения из универсума U(n) типизированные значениями из универсума U(n+1). 5 : Nat : U(0), при этом foo : 5; foo = не пишется.

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

Тогда давай так - озвучь терм типа пять.

Понятно же, что просьба озвучить «терм типа 5» не имеет смысла вне рамках языка и системы типизации? Мы можем построить огромное количество непротиворечивых и, более того, достаточно естественных систем в которых это будет вполне корреткный тип. Ну самое очевидное - терм типа «5» имеют термы, эквивалентные терму «5», а терм «5» имеет такой тип захардкожено (у нас в лбом системе есть набор «захардкоженых» типов). Второй вариант - 5 это просто любой символ, так что мы можем им заменить любой другой символ любого другого типа. Например - Integer, String, Bool. Или если мы наследуем не только 5 но и всю структуру моноида натуральных чисел - то тогда терм типа «n» - это, например, список длины n.

Я всё-таки предполагал случай когда система типов всё время одна и та же, то есть универсальна

Но так не получится. Если макрос чекается до экспанда, то правило типизации макроса добавляется как правило типизации в общую систему типов. То есть каждый вновь определенный макрос меняет систему типов. Вопрос тут состоит только в том, насколько сильно мы ее можем поменять - то есть семантические правила _какой формы_ мы можем определять (иными словами - какие могут быть типы у макросов?). На самом деле, это интересный вопрос, если мы имеем в ЯП систему типов T и в макросах систему типов T, то будет ли любая расширенная система эквивалентна T? Очевидный ответ, что, как минимум, не всегда, но вот интересно при каких T будет, а при каких - нет.

Доказательство корректности = реализация.

А ну это речь идет о том, что если программа реализована и чекнута, она по типам корректна. Да, понятно, но система типов ограничивает подобные «корректные» программы - и чем менее она выразительна, етм сильнее ограничения. В данном случае это ограничивает макросистему - то есть не всяких макрос (даже если он корректный) можно будет написать - аша система типов по-просту окажется недостаточно выразительной для того, чтобы мы могли доказать в ней корректность.

Типы макросов как раз не очень сложны

Они как раз очень сложны :) Простые типы будут только у простых макросов, сводящихся к банальной макроподстановке. Но такие макросы на 100% заменяются ленивыми функциями. Давайте еще раз вспомним, что такое тип макроса - этот тип описывает полностью АСТ, который подается на вход, ограничения на типы элементов этого АСТ, результирующий АСТ, модификации типового контекста после макровызова (внедрение новых переменных, например), связи на типы результирующего АСТа и исходного.

Чекер должен будет проверить, что код макроса действительно генерирует такой АСТ который нужен. Даже доказательство того, что генерируется нужная форма (то есть без учета типов) - это уже нетривиальная задача, если мы свободно можем собирать АСТ при помощи всяких там map/fold/рекурсии (даже на многих тривиальных примерах того же хаскеля для типизации уже не хватит, придется агду тянуть), но кроме этого нам надо вывести, что из ограничений на входе и тела действительно следуют связи на выходе. Как нормально обрабатывать семантические правила - это вообще тьма, я даже и представить себе не могу.

Конечно, мы всегда можем ограничить конструкции в теле макросов - до уровня ленивых функций :)

Макросы (сплайсящиеся функции превращающие код одной стадии в код другой, слова теория/метатеория я бы не стал использовать) превращают (цитированные) значения из универсума U(n) типизированные (цитированными) значениями из универсума U(n+1) снова в значения из универсума U(n) типизированные значениями из универсума U(n+1). 5 : Nat : U(0), при этом foo : 5; foo = не пишется.

Ну да, все так. При этом у нас есть язык, на котором мы пишем процитированные термы и есть язык, на котором эти процитированные термы обрабатываются (метаязык, который я несколько видимо некорректно обозвал метатеорией). Это, вообще говоря, два разных ЯП и никто не требует чтобы у них была одна система типов. Более того - сделать их разными это как раз проще, удобнее и естественнее. А делать систему типов общей - вообще никаких профитов не дает.

Определения макросов типизируются в метаязыке. Макровызовы - в языке.

Например какой-нибудь макрос if имеет тип (Expr (Dat if) (Type Bool) (Dat then) (Type A) (Dat else) (Type A)) -> (Case Bool A) - этот тип проверяется в метаязыке, а в языке у него будет тип if: Bool A A -> A, его должен вывести чекер из типа макроса. Кстати нам в метязыке обязательно нужно подтипирование, т.к. для цитат любых двух несовпадающих термов минимальные типы обязаны быть различны.

просьба озвучить «терм типа 5» не имеет смысла вне рамках языка и системы типизации?

Можно перечислить множество систем обладающих свойствами правильности, полноты, непротиворечивости (в тех или иных комбинациях) в которых эта просьба не имеет смыла - можно начать с лямбда-куба, потом пройтись по линейным типам, по расширениям с подтипами. Типы сами по себе имеют смысл только если нас интересуют те или иные свойства из перечисленных - безопасности, логичности, гарантий, ограничений, в переносе на ЯП. И все такие свойства для всех систем ещё доказывать нужно (причём в доказательствах можно сомневаться - в доказательствах непротиворечивости, например). Поэтому нет смысла говорить про какие-то гипотетические системы типов, не называя их.

Про захардкоженность - в агде можно сделать postulate который может ломать систему типов (например, непротиворечивость), но сделать z : a : A : Set вообще нельзя, то есть это что-то совсем плохое с точки зрения агды. Там принято, что определяемое должно иметь как _минимум_ тип из U(0), а отрицательных универсумов не существует (является ли A : U(0) _универсумом_ U(-1)? Как я понимаю, универсум это не только категория (подкатегория универсума, чем может быть A), но и топос). В большинстве систем вообще есть только термы и типы (и, возможно, U(0)), вот если взять иерархию универсумов в обе стороны... Но это уже другая тема.

иными словами - какие могут быть типы у макросов?

Я пока представляю это так - для всех уровней i для каждого универсума (категории-топоса) Set i есть эндо- точечный- коточечный- функтор Set i -> Set i как конструктор типа для операции цитирования «типа» (элемента : Set i), операция точечного функтора point это операция цитирования «терма» (элемента : T : Set i), операция коточечного функтора extract это операция подстановки цитированного «терма»:

postulate
  -- type quoting
  ⟪_⟫ : {l : Level} → Set l → Set l
  -- term quoting
  ⟦_⟧ : {l : Level} {T : Set l} → T → ⟪ T ⟫
  -- splicing
  $_ : {l : Level} {T : Set l} → ⟪ T ⟫ → T

  splice-quote-identity : ∀ {l} {T : Set l} → $ ⟦ T ⟧ ≡ T

  -- subtype relations?

нужно ещё требовать, чтобы всякая вещь вроде ⟦ 2 + 2 ⟧ : ⟪ ℕ ⟫ не вычислялась до нормальной формы ⟦ 4 ⟧ : ⟪ ℕ ⟫, а оставалась объектом с которым можно работать, то есть ⟦_⟧ это специальная форма.

Дальше я могу ввести ленивый switch как обычную функцию:

switch : {T : Set} → ℕ → List (ℕ × T) → T → T
switch _ [] def = def
switch m ((n , res) ∷ rest) def = if m == n then res else switch m rest def

И switch как макрос:

switch′ : {T : Set} → ⟪ ℕ ⟫ → List (⟪ ℕ ⟫ × ⟪ T ⟫) → ⟪ T ⟫ → ⟪ T ⟫
switch′ _ [] def = def
switch′ m ((n , res) ∷ rest) def = ⟦ if $ m == $ n then $ res else $ switch′ m rest def ⟧

(тип можно варьировать - List (⟪ A ⟫ × ⟪ B ⟫) ≅ List (⟪ A × B ⟫) ≅ ⟪ List (A × B) ⟫, ⟪ A ⟫ → ⟪ B ⟫ ≅ ⟪ A → B ⟫ и т.п.). Тут мы получаем правильную типизацию обоих switch, невозможность типизировать макрос как функцию и наоборот, невозможность перепутать функцию и макрос в комбинациях. А также возможность получить

List (Σ ⟪ ℕ ⟫ (λ x → ⟪ .T ⟫)) !=< ⟪ _78 m n res rest def ⟫ of type
Set
when checking that the expression rest has type
⟪ _78 m n res rest def ⟫

при опечатке :)

Макро-применение посредством сплайса:

app = $ switch′ ⟦ 5 ⟧ ((⟦ 0 ⟧ , ⟦ "0" ⟧) ∷ (⟦ 5 ⟧ , ⟦ "5" ⟧) ∷ []) ⟦ "def" ⟧

(у агды нет сахара для списков). Для app выводится тип String, ну и можно посмотреть нормальную форму app (то во что раскрывается макрос):

$
⟦
if (($ ⟦ 5 ⟧) == ($ ⟦ 0 ⟧) | $ ⟦ 5 ⟧ ≟ $ ⟦ 0 ⟧) then $ ⟦ "0" ⟧ else
$
⟦
if (($ ⟦ 5 ⟧) == ($ ⟦ 5 ⟧) | $ ⟦ 5 ⟧ ≟ $ ⟦ 5 ⟧) then $ ⟦ "5" ⟧ else
$ ⟦ "def" ⟧
⟧
⟧

(остались только примитивные цитирования «самовычисляющихся» термов). Специальная форма $_ должна гарантировать что это преобразование будет проведено на соответствующей стадии.

Обычный применённый switch (ленивая функция):

app′ = switch 5 ((0 , "5") ∷ (5 , "5") ∷ []) "def"

имеет тот же тип String, но просто «5» в качестве нормальной формы.

Да, понятно, но система типов ограничивает подобные «корректные» программы - и чем менее она выразительна, етм сильнее ограничения

Чем _более_ выразительна? :) Хорошо, какую «корректную» программу нельзя написать на хаскеле? Какую нельзя на агде?

Они как раз очень сложны :) Простые типы будут только у простых макросов, сводящихся к банальной макроподстановке. Но такие макросы на 100% заменяются ленивыми функциями.

Можно какой-нибудь модельный пример? А то на switch, который пишется ленивой функцией, трудно ставить опыты (трудно уловить разницу между макросом и обычной функцией), на внешних по отношению к языку DSL, задающих какие-нибудь конфиги - не интересно.

доказательство того, что генерируется нужная форма (то есть без учета типов) - это уже нетривиальная задача

Обычно доказательство того, что форма нужная это как раз задача системы типов.

Как нормально обрабатывать семантические правила - это вообще тьма, я даже и представить себе не могу.

STLC с определением синтаксиса термов и типов, отношением типирования и тайпчекером, интерпретатором и доказательством правильности (в качестве бонуса - макросу это не необходимо) занимает в Coq/Agda пару экранов. У зависимых типов тоже есть довольно лаконичные формы (LF, формы из «simply easy» или «tutorial implementation»).

Более того - сделать их разными это как раз проще, удобнее и естественнее.

А в динамической метасистеме они разве разные? Нормальных систем типов вообще не может быть много (либо они будут эквивалентны друг другу), а специализированные (линейные, например) хочется иметь как нечто встроенное в нормальные. Проще выбрать хорошую метатеорию (как это слово применяется по отношению к MLTT, например), добавить пару хаков (в том числе про multi-satge) и работать уже в ней, просто потому что вокруг ничего больше и нет.