A surprising observation
A certain class of lambda-terms is "the same shape as" their types.
Specifically, the class of lambda-terms is BCI-terms in normal form.
- A lambda-terms is a BCI-term if each lambda-node is the target of a leaf, and no lambda-node is the target of more than one leaf.
-
A lambda-term is in normal form if the left child of an apply-node is never a lambda-node.
If you know the definition of beta-reduction, it is easy to see that the set of BCI-terms is closed under beta-reduction.