Что-то пока нет в примерах ничего, что качественно отличает типизированные варианты от бестипового λ-исчисления. А ограничений вместо этого сразу накладывается целая куча. Чтобы делать анализ программ, совсем не обязательно использовать типы при их написании. Ну, а логика разве не остановилась на конструктивной линейной, из которой, собственно, и получен теоретический предел эффективности вычислений в виде оптимальной редукции?