Статья
Типизированное лямбда-исчисление и соответствие Карри-Ховарда
Что происходит, когда к лямбда-исчислению приделывают типы: часть программ перестаёт компилироваться, зато оставшиеся гарантированно завершаются — и внезапно оказывается, …