История изменений
Исправление quasimoto, (текущая версия) :
Никто не доказал, что такую агду написать _можно_ :)
То есть не доказал, что можно сделать полезный язык общего назначения на основе теории типов?
Разница между динамикой и статикой только в том, как конкретно делается эта обработка/виделение, при чем разница именно во «внешних» проявлениях, в сути ее нет.
Метрика тут ранние (статические) / поздние (динамические) assert-ы / контракты. Если всё сдвигать в сторону динамических, то это требует обязательного тегирования всех объектов (хотя всё больше реализаций языков и так это делают, но не все), а возникновение самих коллизий растягивается на неопределённое время. Сдвиг всего в сторону статики, наоборот, нетривиален (смотрим на теории типов от Рассела и до сего дня).
Исходная версия quasimoto, :
Никто не доказал, что такую агду написать _можно_ :)
То есть не доказал, что можно сделать полезный язык общего назначения на основе теории типов?
Разница между динамикой и статикой только в том, как конкретно делается эта обработка/виделение, при чем разница именно во «внешних» проявлениях, в сути ее нет.
Метрика тут ранние (статические) / поздние (динамические) assert-ы / контракты. Если всё сдвигать в сторону динамических, то это требует обязательного тегирования всех объектов (хотя всё больше языков так делают, но не все), а возникновение самих коллизий растягивается на неопределённое время. Сдвиг всего в сторону статики, наоборот, нетривиален (смотрим на теории типов от Рассела и до сего дня).