The Parigot encoding solves the Church encoding's problem of inefficient predecessor.  It can be typed using positive-recursive types, which preserve normalization of the type theory.