Forwarded from Иван Федоров
типа красное – то что поймал компилятор, белое – то что сломалось в проде
Forwarded from Anton Chikin
Ну системы типов мы наблюдаем как не работают
Forwarded from Deleted Account
У меня есть вопрос к знающим людям. Всё никак понять не могу. Вот есть язык C++ и там нет завтипов, насколько я понял. И вот меня интересует следующие - почему. Т.е. чего системе типов С++ не хватает и что нужно добавить, чтобы каким-то образом реализовать/добавить завтипы?
Forwarded from Alexander Pikeev
Тогда какой смысл от кортежей если списки можно также использовать?
Forwarded from Deleted Account
Кто функциональное программирование умеет?
Forwarded from Deleted Account
Вот, в том и смысл. Что система типов в С++ мета-система. У тебя в идрисе(как и в любом обычном языке) есть система типов в рамках которой ты существует. Там есть какой-то тайпчекер. В рамках ограничения которого ты существуешь и пишешь свою логику.
С++ же язык следующего порядка, о чём я уже говорил ранее. И его система типов так же. Т.е. ты не пишешь логику в рамках крестового тайпчекера - ты пишешь свой тайпчекер
С++ же язык следующего порядка, о чём я уже говорил ранее. И его система типов так же. Т.е. ты не пишешь логику в рамках крестового тайпчекера - ты пишешь свой тайпчекер
Forwarded from Deleted Account
и из-за того, что все конструкции имеют больше смысла - они и быстрее
[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://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]
Это громкие слова. Пруфов у нас нет. Тут это как работает. Есть деньги - можно исследовать. Не важно поможет/нет - хуже не сделает, но вдруг в чём-то поможет.
Forwarded from Deleted Account
ну вот так. УБ - это понятие стандарта. Это значит, что стандарт поведение для чего-то не определяет. У раста нет стандарта, а значит стандарт не определяет поведения ничего. Значит - весь раст УБ. Либо мы убираем стандарт в обоих случаях и тогда понятия УБ вообще нет
Forwarded from Deleted Account
Ну с ложно. Базворд сам за себя говорит. Ну приводил я примеров много. Это слишком абстрактно - люди это просто называют "Опытом". Здесь нет каких-то формальных критериев. У этих знаний нет имени. Я просто знаю как работает машина, что нужно чтобы сгененрировать код с необходимыми свойствами. Я понимаю - что нужно для генерации подобного кода. Я понимаю как он генерируется. Я понимаю, что языку нужно дать генератору