类型理论最早由英国逻辑学家B.罗素（Bertrand Russell，1872～1970）在20世纪初创建，用于避免德国逻辑学家G.弗雷格（Gottlob Frege，1848～1925）版本的朴素集合论中存在的悖论。

通俗来讲，类型是对象所能拥有的属性。在类型理论中，每个对象都是某种类型的项（term），而对象上的操作则限制为相应类型的项上面的重写规则。类型理论通过类型来对项进行分层，从而避免了朴素集合论中的悖论。类型可以分为简单类型、从属类型、递归类型等。

类型理论已经在很多不同的领域得到了广泛的应用。首先，类型理论为数学建立了坚实的基础。两种最有名的可以作为数学基础的类型理论是美国数学家A.邱奇（Alonzo Church，1903～1995）的类型λ演算和瑞典逻辑学家P.马丁-洛夫（Per Martin-Löf，1942～ ）的直觉类型理论。类型理论其他的变种包括F系统、LF、构造演算、同伦类型理论（homotopy type theory）等。而且，类型理论是很多计算机辅助证明工具的理论基础，比如直觉类型理论是Agda的理论基础、构造演算是Coq的理论基础，另外Isabelle也支持多个类型理论的变种。

类型理论在编程语言领域也得到广泛应用。在该领域，研究人员一般将类型理论等同于类型系统。类型系统通过给计算机程序的各种构造赋予一种称之为类型的性质，并且要求计算过程要与这些类型相容，以此来减少计算机程序的错误。

专门针对类型理论的国际会议TYPES，该会议对类型理论的各个方面及其应用（尤其是计算机程序的形式化分析与验证）进行研讨，到2018年已经召开了24届。