Вот, в том и смысл. Что система типов в С++ мета-система. У тебя в идрисе(как и в любом обычном языке) есть система типов в рамках которой ты существует. Там есть какой-то тайпчекер. В рамках ограничения которого ты существуешь и пишешь свою логику.

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

и из-за того, что все конструкции имеют больше смысла - они и быстрее

[In reply to Roman na]
https://www.cl.cam.ac.uk/~jrh13/papers/cade05.html пойдет?

[In reply to Alex Gryzlov]
"Real Arithmetic" здесь - это совершенно не то. К тому же, "где-то кое как пытаются" и используется - это две не одно и тоже.

[In reply to Roman na]
это статья от исследователей Intel, их работы использовались для дизайна процессоров

[In reply to Alex Gryzlov]
Это громкие слова. Пруфов у нас нет. Тут это как работает. Есть деньги - можно исследовать. Не важно поможет/нет - хуже не сделает, но вдруг в чём-то поможет.

в си нет уб - ты обгадился

и в С++ его нет

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

Ну с ложно. Базворд сам за себя говорит. Ну приводил я примеров много. Это слишком абстрактно - люди это просто называют "Опытом". Здесь нет каких-то формальных критериев. У этих знаний нет имени. Я просто знаю как работает машина, что нужно чтобы сгененрировать код с необходимыми свойствами. Я понимаю - что нужно для генерации подобного кода. Я понимаю как он генерируется. Я понимаю, что языку нужно дать генератору

Тут есть мнение что говно ваши функции: https://thecode.media/oop_battle/ Писать много и ничерта потом не понять.

Предлагаю идею для новой книги: Functional Programming Patterns, авторы - "Банда Трех" @graninas @dshevchenko и @bragilevsky

Первое что мне пришло в голову:
1. ООП в питоне наколхозили сбоку, но тут ладно, питон задолго до классов появился.
2. Сборка питон пакетов была концептуально сломана 20 лет подряд, пару лет назад ее полностью переписали на новый стандарт (wheel), но не все на него еще перешли.
3. несмотря на то, что теперь все питонисты пол рабочего дня аннотируют ПО с помощью mypy (его не просто заставить работать), питон все равно на каждом шаге выводит тип переменной, что делает его до 100x раз медленнее по сравнению с языками на жвм

Слушай, у тебя какие-то непонятные неправильные практики.

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

И.С. Тургенев «Межнар и сети»

https://t.iss.one/scala_jobs/64479

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

но что если есть некоторая типизационная дисфория? тоесть что если языковые предпочтения лежат не в плоскости невежества а в плоскости человеческой идентичности?

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

ну и собственно наоборот

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

Объяснить свойства монад все могут. Почему такие интродакшны не отвечают на вопрос зачем их ввели в язык? Эрланг справляется и без монад

В этом смысле реальный язык это монада над категорией всех типов