Человеческое метапрограммирование

F#

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

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

Данная модель изначально создана для параллельных вычислений. Но я утилизирую её в своих целях.

Алгоритмически неразрешимо, извини :(

Это твои фантазии. А у меня полный по Тьюрингу типизатор. И он может типизировать всё.

Да любой номральный динамический ЯП. Все есть.

Что есть? Ловля ошибок еще до запуска? Быстрое исполнение? ИДЕ которую нельзя запутать десятком строк? ИДЕ для статики и на десятках миллионов спокойно живут.

Хватит врать то. Не смешно уже.

Нет, никакой сложности. Наоборот - это наиболее удобный способ борьбы со сложностью.

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

С тремя справится будет уже не реально.

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

Что за бред? Если типизация не закончится, то она не закончится. И программа просто не будет скомпилирована. Ты вообще видел что бывает когда на С++ напишут шаблон который слишком долго работает? Компилятор просто говорит, что не смогла.

То есть макросы не типизируются до экспанда.

Я утверждал и утверждаю, что типизирую код до раскрытия.

Типизируется уже раскрытый код.

И после раскрытия тоже. Ибо программисты косячат.

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

Если макрос при раскрытии породил ошибку, то это в 100% случаев косяк автора макроса. Их быть не должно. Что касается ада и погибели то у меня прямо противоположное мнение. То, что система будет ловить ошибки разработчиков макросов это просто замечательно. Даже то что ловит немерле экономит массу времени при создании макросов.

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

Пользователю будет сказано, что при раскрытии макроса ASFIUGDF произошла ошибка JHGBUIDFKSHIDFHI пинай автора макроса. И в этом нет ничего страшного. Что ICE никогда не ловил? Тут то же самое. Только диагностика гораздо точнее и полностью автоматичнская. В случае же с лиспом всё будет просто глючить.

Придется все ошибки типов перехватывать и формировать нормальные сообщения руками.

Не руками, а автоматом.

При этом лисп для данного случая вообще ничего не предлагает кроме того что программа просто будет молча глючить.

При этом лисп для данного случая вообще ничего не предлагает кроме того что программа просто будет молча глючить.

Ты так говоришь, как будто в лиспе спокойно выполняется (+ 1 «abc») и он продолжает дальше глючить.

А в Лиспе вообще можно вводить свои типы?..

Ты так говоришь, как будто в лиспе спокойно выполняется (+ 1 «abc») и он продолжает дальше глючить.

Если сделать этот код чуть сложнее. Скажем, положить в массив. Потом перемешать его содержимое и потом сделать сложение то концы ты искать будешь долго. Бага примерно того же класса противности как запоротая память в С.

А в Лиспе вообще можно вводить свои типы?..

В CL defstruct, defclass, deftype. В Racket struct, class, interface, контракты.

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

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

Какая еще логика?

Логика распространения информации.

Все остальное сделает Н2.

Откуда он знает какую информацию как откуда и куда надо передавать? Он телепат? Читает мои мысли? Или у вас просто захардкожены определенные способы передачи, котоыре никак не поменять? Что боженька дал - то и юзаем?

О да. Покажи, какой умеет и при этом показывает скорость на уровне хотя бы ANTLR.

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

Согласен. Провернуть такой фокус с типизатором будет проще.

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

Тебя послушать так их должно быть на каждом углу. А их нет. Почему?

Они есть, просто применяются для специфических задач. Для 99% задач «мутабельные» парсеры просто не нужны.

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

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

В начале работы переменная не будет иметь значение. Соответственно макрос Б при попытке чтения данной переменной просто зависнет.

То есть макрос Б в любом случае будет раскрываться после А? И раскрыть его ДО А нету никакого способа? Печально. Ладно, а если переменная есть с самого начала и макрос Б оценивает лишь изменилась ли она относительно определенного значения? Ну например внутренние макросы могут считать какую-то вложенность. Если макрос Б вложен в макрос А и в макросе А значение переменной равно n, то в макросе Б оно будет n+1. Как гарантировать то, что результат не зависит от порядка раскрытия?

Это твои фантазии. А у меня полный по Тьюрингу типизатор. И он может типизировать всё.

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

Что есть? Ловля ошибок еще до запуска? Быстрое исполнение? ИДЕ которую нельзя запутать десятком строк?

Быстрое исполнение есть. Иде есть. Ловля ошибок етсь - только не до запуска. Зачем ловить до запускА, если можно ловить во время запуска в тот же момент что и до?

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

Извини, но ты хуйню писал.

Что за бред? Если типизация не закончится, то она не закончится.

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

Я утверждал и утверждаю, что типизирую код до раскрытия.

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

И после раскрытия тоже. Ибо программисты косячат.

Зачем их типизировать после раскрытия, я не понял? Ты же их до тайпчекнул? Значит все заведомо корректно. Чтто ты вообще подразумевашеь под «типизацией»? Я так чувствую у тебя собственно определение, ничего общего не имеющее с тем, что известно современной науке. Ты вообще у нас революционер, я смотрю - ничего не знаешь, но при том срываешь покровы, решаешь общепризнанно неразрешимые задачи и вообще...

Если макрос при раскрытии породил ошибку, то это в 100% случаев косяк автора макроса.

С чего ты взял? 90% случаев когда макрос порождает ошибку - это случаи _неверного исопльзования макроса_. Автор макроса никак не несет ответственность за то, что его макрос неверно используют.

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

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

Пользователю будет сказано, что при раскрытии макроса ASFIUGDF произошла ошибка JHGBUIDFKSHIDFHI пинай автора макроса.

За что пинать? За то, что он предусмотрел 14543 варинатов неправлиьного использования (в результате на 10 строк макроса, которые задают логику его работы, пришлось около 231232 строк, которые перехватывают ошибки), но осталось еще 45348753487 непредусмотренных способов?

Не руками, а автоматом.

Откуда макрос АВТОМАТИЧЕСКИ знает какие ошибки надо перехватить, как и к чему преобразовать и в каком виде вывести? Этой информации нету нигде кроме головы макрописателя. и то - если он о ней задумывался. Если не задумывался - этой иофнрмации НЕТ ВООБЩЕ.

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

То есть макрос Б в любом случае будет раскрываться после А? И раскрыть его ДО А нету никакого способа? Печально.

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

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

Ладно, а если переменная есть с самого начала и макрос Б оценивает лишь изменилась ли она относительно определенного значения?

Опять твое воображение. Читай что написано.

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

Я это знаю. И я сразу сказал что «типизировать все что можно типизировать». Что тебе в этой фразе не ясно?

Быстрое исполнение есть. Иде есть. Ловля ошибок етсь - только не до запуска. Зачем ловить до запускА, если можно ловить во время запуска в тот же момент что и до?

Лож. Покажи хоть одну ну хотябы на уровне MSVS C#. Про IDEA я даже не заикаюсь. За тем что во время исполнения нет никаких гарантий что ты их поймаешь.

Извини, но ты хуйню писал.

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

Не важно закончиться она или нет.

Это как это не важно?

Тебе надо доказать корректность семантических правил еще ДО того как типизация начнется.

Зачем?

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

С чего это?

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

Они типизируются и до и после. Читай что написано. А то меня уже начинает утомлять, что ты отвечаешь своему воображению, а не мне.

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

До я проверил контракты, которые должен соблюсти пользователь мкроса. После я проверил контракты, которые должен соблюсти автор мароса.

С чего ты взял? 90% случаев когда макрос порождает ошибку - это случаи _неверного исопльзования макроса_. Автор макроса никак не несет ответственность за то, что его макрос неверно используют.

Для этого автор макроса задает правила типизации. И они говорят пользователю, что не так. Это те правила, что выполняются до раскрытия.

Но если эти правила сказали что все ОК. И автор макроса сгенерировал код, который после раскрытия нельзя типизировать то это косяк автора макроса.

Он либо не правильно сгенерировал код. Либо плохо прописал контракты для своего макроса.

Так в том и дело что она не будет ловить ошибки разработчиков макросов. Она будет ловить ошибки тех, кто использует эти макросы.

И снова твое воображение.

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

Что в лоб, что по лбу. Итак, еще раз, у нас етсь макрос Б, которой будучи внутри А - должен раскрыться «так», а не будучи внутри «а» - эдак. Как реализовать эту схему?

Опять твое воображение.

Какое воображение? Я вопрос задал. Видимо, ты на другую цитату отвечал? Повторяю вопрос:

Ладно, а если переменная есть с самого начала и макрос Б оценивает лишь
изменилась ли она относительно определенного значения?

Я это знаю. И я сразу сказал что «типизировать все что можно типизировать».

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

Лож. Покажи хоть одну ну хотябы на уровне MSVS C#.

Emacs. Конечно, со студией не сравнить - в том смысле, что студии до емакс + слайм пилить и пилить... но какие-то подвижки есть, да.

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

О каких императивных типизиторах речь? Я говорил об императивном контрол-флоу в рамках одного экспанда, что, с одной стороны, позволяет гибко и удобно передавать информацию откуда угодно и куда угодно - с другой стороны избавляет от путаницы типа «если раскрытие макроса Б зхависит от того, был ли раскрыт макрос А - то что будет с этой йоба-системой?».

Это как это не важно?

Да вот так. Мы даже не дойдем до ее запуска :( Но, еще раз - это все можно опустить, у тебя ведь макросы до экспанда не типизируются.

Зачем?

Я ниже написал.

С чего это?

Что значит «с чего»? Если семантическое правило некорректно - то это ошибка типов. То есть де-факто в терме лежит строка - а чекер будет думать что там число, например. Как в Qi/Shen.

Они типизируются и до и после.

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

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

Вобще было бы неплохо, если бы ты привел пример небольшого кода строк на 20 с парой-тройкой макросов и описал что и как будет типизироваться. Не важно, что сейчас еще не сделано - ты же знаешь как это _будет_ сделано? То есть код и описание в таком стиле: «вот тут типизируем, такие-то типы приписали, тут макрос раскрыли, получили такой код, типизировали, приписали ...» - и было бы все понятно, а то ты чересчур часто используешь общепринятые термины не в их общепринятом значении, что значительно усложняет общение.

До я проверил контракты, которые должен соблюсти пользователь мкроса. После я проверил контракты, которые должен соблюсти автор мароса.

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

Для этого автор макроса задает правила типизации. И они говорят пользователю, что не так. Это те правила, что выполняются до раскрытия.

Ну так при определении макроса типизатор должен проверить, что эти правила корректны, то есть то, что макрос с текущим телом ДЕЙСТВИТЕЛЬНО ведет себя в соовтетствии с этими правилами. Это как раз и есть та задача, которую надо решать с прувером. У тебя немерле этой задачи, как видно, не решает, в результате может сложиться ситуация как в QI - некорректная типизация. И именно за тем, чтобы она не сложилась, макросы потом чекаются после экспанда. Теперь все ясно. Проблема в том, что эта теория хороша лишь до тех пор, пока правила типизации (те самые которые должны проверяться, но у тебя не проверяются) корректны. Если вдруг они окажутся некорректны - то пользователь получит невнятную говно-лапшу.

Он либо не правильно сгенерировал код. Либо плохо прописал контракты для своего макроса.

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

Кстати, typed/racket, походу, умеет такое искаробки. Ну или с минимальными правками.

Что в лоб, что по лбу.

Во-во. Вообще не читаешь, что тебе пишут.

Итак, еще раз, у нас етсь макрос Б, которой будучи внутри А - должен раскрыться «так», а не будучи внутри «а» - эдак. Как реализовать эту схему?

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

Соответственно макрос Б на этапе типизации узнает что он находится в макросе А и на этапе переписывания воспользуется этой информацией.

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

Ограничение одно: Система типов должна быть разрешима.

Emacs. Конечно, со студией не сравнить - в том смысле, что студии до емакс + слайм пилить и пилить... но какие-то подвижки есть, да.

Понятно. Показать не можешь. Ибо нету.

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

Ох. Это не работает. Вообще не работает.

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

Не избавляет, а создает.

Слушай. Ты вообще хоть раз делал то о чем говоришь? Вот я делал. Второй раз не хочу.

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

Перестань разговаривать со своим воображением. И уже не раз написал что происходит. А ты все твердишь одно и то же.

Что значит «с чего»? Если семантическое правило некорректно - то это ошибка типов. То есть де-факто в терме лежит строка - а чекер будет думать что там число, например. Как в Qi/Shen.

Ссылку на описание проблемы дай.

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

Это ты не понимаешь и главное не пытаешься понять, что я тебе говорю.

Я вообще не собираюсь доказывать правильность переписывания. Оно будет проверено после раскрытия. Более того у меня переписыватели вообще не будут напрямую связаны с синтаксическими конструкциями.

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

Я же уже подробно написал что происходит. И почему так не получится. Ты вообще читаешь?

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

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

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

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

syntax Expr
typing
{
  Type : NemerleType; // Наследуется всеми узлами которые расширяют Expr
}

syntax IfExpr is Expr
parsing "if" "(" Cond ")" ThenExpr "else" ElseExpr
{
  syntax Cond     = Expr;
  syntax ThenExpr = Expr; 
  syntax ElseExpr = Expr;
}
typing
{
  assert Cond.Type == #Bool;
  assert Type <= ThenExpr.Type;
  assert Type <= ElseExpr.Type;
}
transform
{
  <[
    match ($Condition)
    {
      | true  => $ThenExpr
      | false => $ElseExpr
    }
  ]>
}

Первый этап парсинг. На нем мы берем все файлы проекта и парсим.

Второй этап типизация. Мы запускаем на исполнение сразу все блоки типизации.

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

Третий этап. Мы по одному вызываем блоки transform. Они будут порождать нетипизированное АСТ. В данном случае MatchExpr и еще несколько узлов.

После чего мы эти узлы типизируем. Все данные в узлах Cond, ThenExpr, ElseExpr и том узле куда вставляется данное выражение заморожены.

Если при типизации случилась ошибка это косяк разработчика языка. Ибо либо он не поймал проблемы раньше. Либо накосячил с генерацией.

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

Что означает кончтрукция «Type <= ThenExpr.Type»? В transform может быть только квазицитирование, или код тоже (как в N1)?

Что означает кончтрукция «Type <= ThenExpr.Type»?

Что ThenExpr.Type равен или может быть приведен к Type.

В transform может быть только квазицитирование, или код тоже (как в N1)?

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

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

Это примерный прототип.

В Haskell/Agda if пишется как обычная функция (за счёт нестрогости). В агде ещё есть mixfix, там такой пример будет выглядеть как

if[_]_else_ : ∀ {i} {A : Set i} → Bool → A → A → A
if[ true ] x else _ = x
if[ false ] _ else y = y

или

if[_]_else_ : ∀ {i j} {A : Set i} {B : Set j} → Bool → A → B → A ⊎ B
if[ true ] x else _ = inj₁ x
if[ false ] _ else y = inj₂ y

разве что круглые скобки нельзя после if устроить. Перегрузить if[_]_else_ - можно.

ThenExpr.Type равен или может быть приведен к Type.

А NemerleType - это корень иерархии типов, и значение любого типа может быть приведено к нему?

Честно говоря, очень хочется обойтись без императива вообще.

Хм. А можно пример конструкции, аналогичной switch в Си (или match в N1), с произвольным количеством ветвей? Я не очень понимаю, как ее сделать на одном квазицитировании.

В Haskell/Agda if пишется как обычная функция (за счёт нестрогости).

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

Да и если конструкция будет чуть сложнее, то они тоже сдуются.

А NemerleType - это корень иерархии типов, и значение любого типа может быть приведено к нему?

Н2 не немерле. Это совершенно отдельный язык.

NemerleType это тип, используемый в языке немерле. Который будет сделан на Н2.

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

Хм. А можно пример конструкции, аналогичной switch в Си (или match в N1), с произвольным количеством ветвей? Я не очень понимаю, как ее сделать на одном квазицитировании.

Я думаю над этим. Убрать весь императив это такая хотелка. Но не ясно осуществима ли. В типизаторе и парсере точно осуществима. Да и выбора нет.

Да и если конструкция будет чуть сложнее, то они тоже сдуются.

Есть некоторое сходство - mixfix агды похож на parsing, но семантически всё - просто функции с наперёд заданной стратегией вычисления; «макросы» TH похожи тем что они статически типизированы (там макрос - функция типа (набор любых типов -> Q Dec/Expr) которая будет использоваться в сплайсе $()), но, наоборот, без возможности вроде parsing, то есть использование генератора кода всегда регламентировано - $(macro ...) вместо обычной аппликации (fun ...).

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

Да. Точнее, в Haskell (хм, то есть в GHC) средствами QQ можно из произвольного текста между [your_name_here| и |] сгенерировать произвольный код или декларации. Ну и TH позволяет писать типизированные генераторы из произвольных вещей в код и декларации, как я уже сказал. Хотя в целом там крайне неполная и незамкнутая система, её хватает для вещей вроде

term :: SomeType
term = [myQuote| ASCII art DSL |]

(myQuote требует написать/взять парсер и составить хаскельный код конструкторами) или

data SomeADT = ...
  deriving ( ..., Data )

genSomeCode "foobar" 5 'SomeADT

term = ... $(genAnotherCode ...)

где genSomeCode - функция (сплайс можно опускать в top-level) из строки, числа и имени в нужные декларации. С использованием информации доступной для всех инстансов Data будет проанализирован данный SomeADT и сгенерировать любой нужный код. genAnotherCode - то же самое, но локально.

NemerleType это тип, используемый в языке немерле. Который будет сделан на Н2.

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

Проверяет ли этот учебный пример то, что обе ветви match имеют одинаковый тип?

А можно пример конструкции, аналогичной switch в Си (или match в N1), с произвольным количеством ветвей? Я не очень понимаю, как ее сделать на одном квазицитировании.

Я думаю над этим. Убрать весь императив это такая хотелка. Но не ясно осуществима ли

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

Проверяет ли этот учебный пример то, что обе ветви match имеют одинаковый тип?

Он проверяет, что обе ветки if имею тип, приводимый к одному и тому же типу.

После чего находит этот тип и делает его типов узла if.

Если ты про раскрытый код. То тоже проверяет. Но уже при типизации сгенерированного узла match. И если будет облом, то сообщит о нем как об ошибке разработчика макроса.

И я об этом писал.

Если ты про раскрытый код

Нет, с раскрытым кодом всё понятно.

И я об этом писал.

Картинка стоит тысячи слов.

А можно пример конструкции, аналогичной switch в Си (или match в N1), с произвольным количеством ветвей? Я не очень понимаю, как ее сделать на одном квазицитировании.

Если делать обычный switch без паттерн матчинга, то можно просто рекурсивно пройтись по списку ветвей генерируя цепочку if-ов в квазицитировании:

switch :: ExpQ -> [(ExpQ, ExpQ)] -> ExpQ -> ExpQ
switch exp cases def = go cases where
  go ((x,z):zs) = [| if $exp == $x then $z else $(go zs) |]
  go [] = def

test =
  $(switch [| 2 + 2 |]
    [
      ( [| 0 |], [| print "0" |]),
      ( [| 4 |], [| print "4" |])
    ]
    [| print "?" |]
   )

чисто функционально. Проверка типов проводится на раскрытом коде, например ( [| «0» |], [| print «0» |]) не скомпилируется с сообщением о «строка != число» (ghc при этом печатает раскрытый код, а emacs-mode тыкает на начало switch).

чисто функционально

И даже тотально :)

Проверка типов проводится на раскрытом коде, например ( [| «0» |], [| print «0» |]) не скомпилируется с сообщением о «строка != число» (ghc при этом печатает раскрытый код

Это как бы похеривает всю идею контроля до стадии экспанда.

Это как бы похеривает всю идею контроля до стадии экспанда.

У switch тип очень общий - ExpQ это любой цитированый код, [(ExpQ, ExpQ)] - список пар любого цитированного кода, почти динамика, проверять нечего, вот когда получится if exp == x1 then z1 else if exp == x2 then z2 ... то на этом коде уже можно проверять что exp, x1, x2, ... все типов Eq t => t, что типы z1, z2, ... совпадают и т.п. Можно типизировать switch более конкретно, например String -> [(String, ExpQ)] -> ExpQ -> ExpQ, тогда проверка на String будет проводиться до стадии экспанда (ghc печатает код нераскрытого switch, emacs показывает место где не совпадает тип внутри switch).

У switch тип очень общий

Я не стану притворяться, что понял все эти заклинания с ExpQ, но у switch тип как раз очень частный - void; у выражения в switch - int. Проверить второе - это слишком сложно для TH?

Ну и то что там именно три аргумента и именно список пар проверяется до экспанда.

Соответственно макрос Б на этапе типизации узнает что он находится в макросе А и на этапе переписывания воспользуется этой информацией.

Как он это узнает? Пример можно?

Ограничение одно: Система типов должна быть разрешима.

Это весьма существенное ограничение.

Понятно. Показать не можешь. Ибо нету.

Как нету? Вон же он емакс. Бери, да смотри.

Ох. Это не работает. Вообще не работает.

Это прекрасно работает. А вот твои фантазии - пока что не работают никак. Вообще никак. Потому что это на данный момент - только фантазии.

Слушай. Ты вообще хоть раз делал то о чем говоришь?

Конечно. И я вижу огромное количество преимуществ по сравнению с тем, что ты описываешь.

Не избавляет, а создает.

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

Перестань разговаривать со своим воображением. И уже не раз написал что происходит.

Тем, что ты написал 0 можно подтереться, так как ты используешь терминологию отличную от общепринятой. Но по ксовенным признакам я таки понял что у тебя происходит. Так вот - это никак не связано с тайпчеком во время экспанда. Тайпчекается у тебя все строго после экспанда. И когда тебя следующий раз спросят о времени тайпчека, то так и говори: «после экспанда». Потмоу что иначе тебя опять люди неверно поймут.

Ссылку на описание проблемы дай.

Какую ссылку? Откуда должна взяться такая ссылка? О чем ты вообще?

Я вообще не собираюсь доказывать правильность переписывания. Оно будет проверено после раскрытия.

Я это прекрасно понял. «оно проверено после раскрытия» - это и означает «тайпчек будет проводиться после раскрытия». Ты же ввел меня в заблуждения своими «макросы чекаются до раскрытия».

Я же уже подробно написал что происходит. И почему так не получится.

Нет, ты написал о своих _фантазиях_, а я тебе описал то, что реально будет. Я прекрасно понял, что и как у тебя происходит - так вот, не вы первые и не вы последние наступаете на эти грабли.

Я использую термины правильно.

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

Подскажите кто-нибудь ЯП с развитой метасистемой, только нормальный, а не лисп.

fasm? :D

Это примерный прототип.

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

У тебя пока что объяснения такие: «сперва у нас парсер, который пиздато парсит, потом типизатор, который чудесным образом пиздато ищет ошибки».

В данном случае у нас есть вся информация

Повторяю - информации вообще НИГДЕ НЕТУ, кроме головы макрописателя. И то только в том случае, если он об этой проблеме думла. Если не думал - ее нету вообще. И в твоем типзиаторе она чудесным образом изниоткуда не появится.

у выражения в switch - int

Изначально я написал вариант работающий с Int, Integer, Double, String и любым другим сравнимым на равенство типом (инстансом класса Eq, то есть с любым типом для которого реализован интерфейс (==) :: Eq t => t -> t -> Bool).

но у switch тип как раз очень частный - void

Это у применённого switch, да и то, мы говорим про генератор/трансформатор кода, поэтому его тип это то что он принимает (типы разных кусков AST или типы обычных данных языка) и что он возвращает (типы для кода внутри функций, для кода типов или для кода top-level определений).

Проверить второе - это слишком сложно для TH?

Автоматически я не знаю как это сделать. Можно написать полноценный switch который будет работать только для Int и сообщать про «не Int» после экспанда (то есть тайпчекая раскрытый код). Нужно взять не полиморфную функцию вместо (==). Либо switch от runtime независимых значений только типа Int который сможет говорить «не Int» до экспанда. Будет Int -> [(Int, ExpQ)] -> ExpQ -> ExpQ. А полноценный switch с проверкой на «не Int» до экспанда пишется, но это нужно непосредственно работать с монадой Q в do-нотации, то есть без квазицитирования, с разборкой/сборкой AST, выяснением типов имён, вытаскиванием локаций исходников и далее вплоть до выполнения произвольного императивного кода с помощью runIO, например, ручным печатанием сообщений об ошибках.

assert Cond.Type == #Bool;
assert Type <= ThenExpr.Type;
assert Type <= ElseExpr.Type;

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

Это как бы похеривает всю идею контроля до стадии экспанда.

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

Ну а, собственно, в том случае, когда чекер указанное соответствие не проверяет эта «типизация» - не более чем немного синтаксического сахара над кодом для обработки ошибок. Можно вообще эти правила не писать - это на ход типизации никак не повлияет.

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

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

полноценный switch с проверкой на «не Int» до экспанда пишется

Хотя это уже «во время экспанда», кодом до обратной кавычки, выражаясь терминами CL. И то, если там будет $(switch [| сложное выражение |] ...), непонятно как гарантировать тип сложного выражения, это нужно какое-то GHC API для TH.

Проверить второе - это слишком сложно для TH?

Собственно, вот - http://hackage.haskell.org/trac/ghc/blog/Template Haskell Proposal#PartB:AddM....

Ограничение одно: Система типов должна быть разрешима.

Это весьма существенное ограничение.

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

Как нету? Вон же он емакс. Бери, да смотри.

Смотрел. Унылое говно. Если это лучшее что есть, то, как я и говорил нормальных ИДЕ для динамики нет.

Конечно. И я вижу огромное количество преимуществ по сравнению с тем, что ты описываешь.

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

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

Общепринятой среди тебя одного? Возможно.

Но по ксовенным признакам я таки понял что у тебя происходит. Так вот - это никак не связано с тайпчеком во время экспанда. Тайпчекается у тебя все строго после экспанда. И когда тебя следующий раз спросят о времени тайпчека, то так и говори: «после экспанда». Потмоу что иначе тебя опять люди неверно поймут.

У меня весь код тайпчекается и до переписывания и после переписывания.

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

Какую ссылку? Откуда должна взяться такая ссылка? О чем ты вообще?

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

Я это прекрасно понял. «оно проверено после раскрытия» - это и означает «тайпчек будет проводиться после раскрытия». Ты же ввел меня в заблуждения своими «макросы чекаются до раскрытия».

Они и чекаются. Сначала проверяется то, что написано в секции typing у узлов которые получил парсер из исходника. Потом после перепиывания. Проверяется то, что написано в секции typing у раскрытых узлов которые сгенерировал переписыватель.

Нет, не правильно. Тайпчек у тебя (согласно определению тайпчека) происходит после экспанда.

Давай ты приведешь определения экспанда и тайпчека, которые ты используешь.

Ибо у меня тайпчек это то, что написано в секции typing. А экспанд/трансформация/переписывание это то, что написпано в секции transform.

То, что происходит с нераскрытым кодом (проверка тела макроса на соответствие заданному макрописаталем семантическому правилу) НЕ является тайпчеком.

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

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

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

В чем проблема - гипотетически неточных сообщениях об ошибке?

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

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

Конкретно эти да. if'у больше ничего не нужно.

То есть в этом блоке typing мы только уравнения для унификации задавать и можем?

Не только. Будет полный по Тьюрингу язык, который мощнее чем функциональщина.

Смотрел. Унылое говно. Если это лучшее что есть, то, как я и говорил нормальных ИДЕ для динамики нет.

Ну он лучше студии, по крайней мере, с которой ты сравнивал. У статических языков и такого «говна» нет - все хуже гораздо. О чем речь-то тогда?

Код двух взаимодействующих императивных типизаторов в студию. Так чтобы там все было просто и красиво. Циклический обмен информацией обязателен.

(define (f x context) (when (pred context) blah-blah-blah (g x)))

(define (g x context) (when (pred2 context) blah blah blah (f x)))

Вот тебе два типизиатора, которые в цикле обмениваются информацией друг с другой. Реализованы в виде двух взаимно-рекурсивных ф-й. Какие проблемы?

А тепреь напиши мне код где экспанд макроса Б зависит от того, находится ли он внутри А или нет. Я уже хз сколько жду от тебя эти 3 строчки.

Общепринятой среди тебя одного?

Общепринятой для всего cs-сообщшества, хз.

У меня весь код тайпчекается и до переписывания

О боже. Он у тебя НЕ тайпчекается до переписывания. Если код тайпчекнут - это значит в нем НЕТ ошибок типов. То, что у тебя чекер делает до переписывания, отсутствие ошибок типов НЕ гарантирует. Более того - эту часть тайпчека вообще можно тупо УБРАТЬ. И результат работы алгоритмы никак не изменится. То, что все люди называют тайпчеком, у тебя происходит после экспанда.

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

Ну да, так и есть. Можешь сам скачать Qi и попробовать - очень занимательно :) Вон, thesz на говно по этому поводу как-то исходил.

Вот и дай мне ссылку на подробное описание данной проблемы.

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

И повторю еще раз - это в любом случае неважно, т.к. в н2 код чекается после раскрытия а не до.

Они и чекаются. Сначала проверяется то, что написано в секции typing у узлов которые получил парсер из исходника.

Нда. Терм типизирован, если ему приписан корректный в соответствии с системой типизации тип. У тебя такого не происходит - никто не гарантирует, что указанный автором макроса тип будет для терма корректен (в большинстве случаев это будет не так). Типизация термов у тебя происходит уже после раскрытия. До раскрытия у тебя просто исполняется некий код обработки ошибок, ну то есть это совершенно эквивалентно тому, как если бы я написал так: (define-syntax (yoba stx) (syntax-parse [(f x blablabla) (when (eq? (type #'x) (type #'blablabla)) (error «ошибка типов блаблабла»)) (код макротрансформации)]). Естественно, что это никакой не тайпчек.

Ибо у меня тайпчек это то, что написано в секции typing.

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

Смотрел. Унылое говно. Если это лучшее что есть, то, как я и говорил нормальных ИДЕ для динамики нет.

Ну он лучше студии, по крайней мере, с которой ты сравнивал. У статических языков и такого «говна» нет - все хуже гораздо. О чем речь-то тогда?

Код двух взаимодействующих императивных типизаторов в студию. Так чтобы там все было просто и красиво. Циклический обмен информацией обязателен.

(define (f x context) (when (pred context) blah-blah-blah (g x)))

(define (g x context) (when (pred2 context) blah blah blah (f x)))

Вот тебе два типизиатора, которые в цикле обмениваются информацией друг с другой. Реализованы в виде двух взаимно-рекурсивных ф-й. Какие проблемы?

А тепреь напиши мне код где экспанд макроса Б зависит от того, находится ли он внутри А или нет. Я уже хз сколько жду от тебя эти 3 строчки.

Общепринятой среди тебя одного?

Общепринятой для всего cs-сообщшества, хз.

У меня весь код тайпчекается и до переписывания

О боже. Он у тебя НЕ тайпчекается до переписывания. Если код тайпчекнут - это значит в нем НЕТ ошибок типов. То, что у тебя чекер делает до переписывания, отсутствие ошибок типов НЕ гарантирует. Более того - эту часть тайпчека вообще можно тупо УБРАТЬ. И результат работы алгоритмы никак не изменится. То, что все люди называют тайпчеком, у тебя происходит после экспанда.

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

Ну да, так и есть. Можешь сам скачать Qi и попробовать - очень занимательно :) Вон, thesz на говно по этому поводу как-то исходил.

Вот и дай мне ссылку на подробное описание данной проблемы.

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

И повторю еще раз - это в любом случае неважно, т.к. в н2 код чекается после раскрытия а не до.

Они и чекаются. Сначала проверяется то, что написано в секции typing у узлов которые получил парсер из исходника.

Нда. Терм типизирован, если ему приписан корректный в соответствии с системой типизации тип. У тебя такого не происходит - никто не гарантирует, что указанный автором макроса тип будет для терма корректен (в большинстве случаев это будет не так). Типизация термов у тебя происходит уже после раскрытия. До раскрытия у тебя просто исполняется некий код обработки ошибок, ну то есть это совершенно эквивалентно тому, как если бы я написал так: (define-syntax (yoba stx) (syntax-parse [(f x blablabla) (when (eq? (type #'x) (type #'blablabla)) (error «ошибка типов блаблабла»)) (код макротрансформации)]). Естественно, что это никакой не тайпчек.

Ибо у меня тайпчек это то, что написано в секции typing.

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

Не только. Будет полный по Тьюрингу язык

Печально. Каким же образом будет проходить унификация?

Ну он лучше студии, по крайней мере, с которой ты сравнивал. У статических языков и такого «говна» нет - все хуже гораздо. О чем речь-то тогда?

А как по мне, то унылое говно.

Вот тебе два типизиатора, которые в цикле обмениваются информацией друг с другой. Реализованы в виде двух взаимно-рекурсивных ф-й. Какие проблемы?

Мда. Ты даже не понял о чем разговор.

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

Чтобы как тут https://github.com/rampelstinskin/ParserGenerator/blob/8d02b02b76ed08ab9f71a5...

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

О боже. Он у тебя НЕ тайпчекается до переписывания. Если код тайпчекнут - это значит в нем НЕТ ошибок типов.

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

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

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

Типизация термов у тебя происходит уже после раскрытия. До раскрытия у тебя просто исполняется некий код обработки ошибок, ну то есть это совершенно эквивалентно тому, как если бы я написал так: (define-syntax (yoba stx) (syntax-parse [(f x blablabla) (when (eq? (type #'x) (type #'blablabla)) (error «ошибка типов блаблабла»)) (код макротрансформации)]). Естественно, что это никакой не тайпчек.

А что это? Что же тогда такое тайпчек если не проверка типов конструкций языка?

Что ты вообще под этим термином понимаешь? Ты вообще сам-то понимаешь что говоришь?

После раскрытия у меня снова происходит тайпчек. Только цель не сказать пользователю об ошибке. Это работа типизатора той конструкции, которая раскрывается. А проверить правильно ли раскрыта конструкция. Ты вообще термин internal compiler error слышал? Так вот это автоматический поиск таких ошибок. Не более того.

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

У нормальных людей тайпчек - это не то, что написано в секции typing (что если в ЯП вообще нету такой секции? Тайпчека нету там, видимо?), а процесс приписывания термам типов в соответствии с определенными правилами.

Ох. Н2 это не язык на котором решают прикладную задачу. Это язык, на котором пишут другие языки.

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

Смотри на if. Там заданы 3 правила которые нужно проверить. И выводится тип всей конструкции. Этот тип будет использован другими конструкциями для того чтобы выводить свои типы и проверять свои правила.

Так что это именно тайпчек.

И терм чекнут, если приписан корректный тип. А если не приписан - ошибка.

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

У тебя тип приписывается уже после раскрытия

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

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

Так я про это и пишу уже несколько сообщений подряд. Это способ автоматического поиска ICE. Не более того.

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

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

Печально. Каким же образом будет проходить унификация?

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