I think it comes down historically to Church's https://en.m.wikipedia.org/wiki/Simply_typed_lambda_calculus https://en.m.wikipedia.org/wiki/Simply_typed_lambda_

I think it comes down historically to Church's https://en.m.wikipedia.org/wiki/Simply_typed_lambda_calculus https://en.m.wikipedia.org/wiki/Simply_typed_lambda_calculus . It originated the most popular form of type theory and also used the simplest functional programming language, lambda calculus.