Типы дают частичные спецификации, предупреждая возникновение определенных классов червоточин. Обсуждаемая, кстати, ни в одной известной мне типизированной версии лямбда исчисления не имеет места (кроме тех, конечно, в которых все термы имеют тип).