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

Но опять-таки, к теории типов и тем более сабтайпингу это отношения не имеет вообще

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

По теории типов применительно к ЯП, я читал "Types and programming languages", хорошая книжка, достаточно понятная.

По теории типов в плане альтернативны для оснований математики, с ходу не вспомню все источники, как-то читал HoTT (Homotopy Type Theory), но достаточно мельком. Ну и там везде хардкор, нужна хорошая математическая грамотность и интуиция.

По теории множеств и основаниям математики ещё читал что-то в универе, но уже не вспомню кого именно.

Можно ещё поиграться с каким-нибудь языком с зав типами, можно с той же агдой или coq

хардкорной литературы хватает, но она написана профессионалами для профессионалов, для аматеров вроде меня это недоступное чтиво: просто нет возможности потратить столько времени на это, пренебрегая всем остальным. но обычно хватает первую четверть/половину книги прочесть, а дальше уже идут доказательства и следствия второстепенных вещей или их связь с другими областями математики, которые можно и оставить непрочтенными, но при этом уловить суть. "Types and programming languages" звучит безопасно))))

Types and programming languages - хорошо написана, там можно читать вообще отдельными главами или темами. В начале книги есть граф зависимостей глав книги друг от друга.

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

кстати, мб кто-нить подскажет
можно ли сделать свою функцию с текст форматтером? Чтоб как printf только с кастомным поведением. Чтоб прям в функцию можно аргументом было передать "%A %i" и компилятор распарсил, что туда нужно 2 параметра передать

в лоб не получается, даже если прописать у параметра тип текст форматтер, он все равно читает параметр как обычную строку, игнорируя всякие` %i `

Модуль Printf

Kprintf

Там

не совсем то, что я имею ввиду, но мб и поможет

Оно и есть

Ща пример кину

о да, вроде работает

фак еа, спасибо @Liminiens  @vshapenko