目录
型別構造器
类型构造器也称类型构造子，是把若干已知类型组合成一新类型的手段。可以看作是类型的构造函数。打个比方，如果说普通的函数操作变量并产生新值，那么类型构造器就是操作类型返回新类型。 例如，数组 T 是若干相同类型 T 元素的有序集合，我们说从 T 类型构造出“T 的数组”这一类型的类型构造器是（后缀）、即“加上数组”。.
多型 (计算机科学)
在编程语言和类型论中，多型（polymorphism）指为不同数据类型的实体提供统一的接口。 多态类型（polymorphic type）可以将自身所支持的操作套用到其它类型的值上。: "Polymorphic types are types whose operations are applicable to values of more than one type." 计算机程序執行時，相同的訊息可能會送給多個不同的類別之物件，而系統可依據物件所屬類別，引發對應類別的方法，而有不同的行為。簡單來說，所謂多型意指相同的訊息給予不同的物件會引發不同的動作。 多态也可定义为“一种将不同的特殊行为和单个泛化记号相关联的能力”。 多态可分为变量多态与函数多态。变量多态是指：基类型的变量（对于C++是引用或指针）可以被赋值基类型对象，也可以被赋值派生类型的对象。函数多态是指，相同的函数调用界面（函数名与实参表），传送给一个对象变量，可以有不同的行为，这视该对象变量所指向的对象类型而定。因此，变量多态是函数多态的基础。 多态还可分为：.
子类型
在编程语言理论中，子类型（动名词，subtyping）是一种类型多态的形式。这种形式下，子类型（名词，subtype）可以替换另一种相关的数据类型（超类型，supertype）。也就是说，针对超类型元素进行操作的子程序、函数等程序元素，也可以操作相应的子类型。如果 S 是 T 的子类型，这种子类型关系通常写作 S number 的语言。在第一种情况下，整数类型将是浮点数类型的子类型；在第二种情况下，这两个类型都是 number 的子类型而相互之间无子类型关系。 编程者可利用子类型来以比没有它更抽象的方式来写代码。考虑下面的例子: 如果整数和实数都是 number 的子类型，则二者任何类型都可以传递给这个函数。为此，子类型经常被认为是一种形式的多态性。上述例子也可以比较于 C++ 语言的模板。 在类型论中，子类型关系经常写为 <:，有着 A<:B 意味着 A 是 B 的子类型。在类型论中子类型可用如下事实来特征化，如果 A<:B，类型 A 的任何表达式也可被给予类型 B；立法这个特征化的形式类型规则叫做“包容”规则。.
依赖类型
在计算机科学和逻辑中，依赖类型（或依存类型，dependent type）是指依赖于值的类型，其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中，依赖类型可对应于谓词逻辑中的全称量词和存在量词；在依赖类型函数式编程语言如 ATS、Agda、Dependent ML、Epigram、F* 和 Idris 中，依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查，从而有效减少程序错误。 依赖类型的两个常见实例是依赖函数类型（又称依赖乘积类型、Π-类型）和依赖值对类型（又称依赖总和类型、Σ-类型）。一个依赖类型函数的返回值类型可以依赖于某个参数的具体值，而非仅仅参数的类型，例如，一个输入参数为整型值n的函数可能返回一个长度为n的数组；一个依赖类型值对中的第二个值可以依赖于第一个值，例如，依赖类型可表示这样的类型：它由一对整数组成，其中的第二个数总是大于第一个数。 依赖类型增加了类型系统的复杂度。由于确定两个依赖于值的类型的等价性需要涉及具体的计算，若允许在依赖类型中使用任意值的话，其类型检查将会成为不可判定问题；换言之，无法确保程序的类型检查一定会停机。 由于Curry-Howard同构揭示了程序语言的类型论与证明论的直觉逻辑之间的紧密关联性，以依赖类型系统为基础的编程语言大多同时也作为构造证明与可验证程序的辅助工具而存在，如 Coq 和 Agda（但并非所有证明辅助工具都以类型论为基础）；近年来，一些以通用和系统编程为目的的编程语言被设计出来，如 Idris。 一些以证明辅助为主要目的的编程语言采用强函数式编程（total functional programming），这消除了停机问题，同时也意味着通过它们自身的核心语言无法实现任意无限递归，不是图灵完全的，如 Coq 和 Agda；另外一些依赖类型编程语言则是图灵完全的，如 Idris、由 ML 衍生而来的 ATS 和 由 F# 衍生而来的 F*。.
简单类型λ演算
单类型 lambda 演算(\lambda^\to)是连接词只有 \to (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、陪积或自然数(系统 T)甚至完全的递归(如PCF)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。.
类型论
在最广泛的层面上，类型论是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。在这种意义上，它与类型的形而上学概念有关。现代类型论在部分上是响应罗素悖论而发明的，并在伯特兰·罗素和阿弗烈·诺夫·怀海德的《数学原理》中起到重要作用。 在计算机科学分支中的编程语言理论中，类型论提供了设计分析和研究类型系统的形式基础。实际上，很多计算机科学家使用术语“类型论”来称呼对编程语言的类型语言的形式研究，尽管有些人把它限制于对更加抽象的形式化如有类型lambda演算的研究。.
系统F
系统F，也叫做多态lambda演算或二阶lambda演算，是有类型lambda演算。它由逻辑学家Jean-Yves Girard和计算机科学家John C. Reynolds独立发现的。系统F形式化了编程语言中的参数多态的概念。 正如同lambda演算有取值于（rang over）函数的变量，和来自它们的粘合子（binder）；二阶lambda演算取值自类型，和来自它们的粘合子。 作为一个例子，恒等函数有形如A→ A的任何类型的事实可以在系统F中被形式化为判断 这里的α是类型变量。 在Curry-Howard同构下，系统F对应于二阶逻辑。 系统F，和甚至更加有表达力的lambda演算一起，可被看作Lambda立方体的一部分。.
规范化性质
在数理逻辑和理论计算机科学中，一个重写系统有规范化性质，如果所有项都是强规范化的；就是说所有重写序列都最终终止于规范形式的项。 纯粹无类型 lambda 演算不是强规范化的。考虑项 \lambda x. x x x。它有如下重写规则: 对于任何项 t， 但是考虑在应用 \lambda x.
逻辑框架
在类型论中，LF 逻辑框架提供了定义(或表示)逻辑的一种方式。它基于了通过有依赖类型的lambda 演算方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 Per Martin-Löf 文章中的系统的风格来处理。 要描述一个逻辑框架，你必须提供如下: 1.
构造演算
构造演算(CoC)是高阶有类型 lambda 演算，这里的类型是一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数，同从整数到整数的函数一样。CoC 是强规范化的。 CoC 最初由 Thierry Coquand 开发。 CoC 是 Coq 定理证明器早期版本的基础；它后来的版本建造在归纳构造演算之上，这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中，归纳数据类型必须模拟为它们的多态解构函数。.
数理逻辑
数理逻辑是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。 数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑（相对于哲学逻辑），又称元数学，后者的使用现已局限于证明论的某些方面。.
另见
Lambda演算
- Λ演算
- B,C,K,W系统
- Beta范式
- Lambda立方体
- SKI组合子演算
- 不动点组合子
- 匿名函数
- 有类型λ演算
- 构造演算
- 柯里化
- 笛卡儿闭范畴
- 简单类型λ演算
- 类型居留问题
- 系统F
- 组合子逻辑
- 蒙塔古語法
- 邱奇数
- 高阶函数