Пожалуйста, объясните, наконец, дураку, чем же так хороши были бы типы в λ-исчислении, если бы его можно было типизировать (известно, что нельзя) полностью. Какие от этого выгоды? (Чур сильную нормализуемость в пример не приводить, так как именно из-за нее-то и нельзя.)
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2012-02-20 10:58 am (UTC)