Is there any work in type theory where no base types are assumed, e.g., that there are only function types in place ($t_1 \to t_2$ is a type whenever $t1$ and $t_2$ are types)? If not, are there specific reasons for that?