Пожалуйста, объясните, наконец, дураку, чем же так хороши были бы типы в λ-исчислении, если бы его можно было типизировать (известно, что нельзя) полностью. Какие от этого выгоды? (Чур сильную нормализуемость в пример не приводить, так как именно из-за нее-то и нельзя.)
no subject
Date: 2012-02-20 10:58 am (UTC)