Void
void 在诸如 C/C++ 等编程语言中是一个关键字，表示一个函数“不返回值”。注意这并不意味着某个函数永不返回，只是说“该函数的返回值没有意义、调用方应当无视”。 在参数表中的 void 代表该函数没有参数。 void* 在指针基类型位置的 void 表示这个指针可以指向任何类型的数据（函数除外）。 参考资料
标签：#类型论
共 46 篇文章
类型签名
在计算机科学中，类型签名（）或类型注解（）是对程序的函数、方法、子过程、以及变量等给出其类型。特别是对函数给出其输入参数数量、类型与次序及输出结果的类型。 许多编译器产生的内部使用的函数名包含了其类型特征，这称为名字修饰，為链接器辨别不同的函数提供了方便。 类型特征的现代应用： 面向对象语言使用的interface，实际上是利用了函数类型特征的模板。 C++支持的函数重载实际上用不同的类型特征来辨识。 多继承要求考虑函数特征，以避免不可…
新基础集合论
在数理逻辑中，新基础集合論（NF）是公理化集合論的一種，由蒯因构想出來作为对《数学原理》中类型论的简化。蒯因1937年於《数理逻辑的新基础》一文中首次提及NF（此即其名稱的由來）。請注意，此条目大多是在談论NFU，這是Jensen於1969年所提出，並由Holmes於1998年闡述的一重要变体。 类型论TST 改进版本的类型论TST的基本谓词是等於和成员关系。TST有一个线性的类型层次：类型0由不加描述的个体组成。对于每个（元-）自然数…
数学结构
在数学中，数学结构（mathematical structure）简称结构（structure），是指在集合之上附加的额外数学对象（如运算、关系、度量等），使得该集合具备了特定的性质和规律。 一个数学结构通常由以下三个部分定义：底层集合（基集或支撑集）、附加对象（运算、关系、子集族）和公理。狭义上，数学结构是在集合上定义的映射、关系或族；广义上，数学结构是指一个多元组，包含了基集和所有规则。 通论 在数学中，一个集合（或若干集合）上的“…
单值类型
在数理逻辑、计算机科学和类型论中，单值类型（unit type）是只允许1个值的数据类型。单值类型的基础集(underlying set)是单元素集合。由于任何2个单元素集合同构，因而习惯称“这个单值集合”（ the unit type），不必考虑具体的值是什么。也可以把单值类型视作0-元组，如无类型的积。 单值类型是范畴论中类型和有类型函数的终对象，不应与 zero或混淆。后两者允许no值，是范畴的始对象。类似的，布尔类型是有2个值的…
依值类型
在计算机科学和逻辑中，依值类型（旧译依赖-{}-类型，dependent type）是指依赖于值的类型，其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中，依值类型可对应于谓词逻辑中的全称量词和存在量词；在依值类型函数式编程语言如、Agda、、、F和Idris中，依值类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查，从而有效减少程序错误…
柯里-霍华德对应
寫作的：在Coq軟件中自然數加法交換性的證明。nat_ind 代表數學归纳，eq_ind 代替等於，f_equal 代表在等式兩邊取同樣的函數。 前面的定理參照顯示 m = m + 0和S（m + y）= m + S y。]] 柯里-霍華德对应（）是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和数学运算之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里…
构造演算
构造演算(CoC)是高阶有类型 lambda 演算，这里的类型是一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数，同从整数到整数的函数一样。CoC 是强规范化的。 CoC 最初由 Thierry Coquand 开发。 CoC 是 Coq 定理证明器早期版本的基础；它后来的版本建造在归纳构造演算之上，这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中，归纳数据类型必须模拟为它们的多态解构函数。 构…
逻辑框架
在类型论中，LF 逻辑框架提供了定义(或表示)逻辑的一种方式。它基于了通过有依赖类型的lambda 演算方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 Per Martin-Löf 文章中的系统的风格来处理。 要描述一个逻辑框架，你必须提供如下: 1. 对要表示的那一类对象-逻辑的特征描述； 2. 适当的元-语言； 3. 对表示对象-逻辑的机制的特征描述。 总结为: :“框架 = 语言 + 表示”。 在 LF 逻辑框架的…
简单类型λ演算
简单类型 lambda 演算(\lambda^\to)是连接词只有 \to (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、陪积或自然数(系统 T)甚至完全的递归(如PCF)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在…
有类型λ演算
有类型lambda演算是使用lambda符号（\lambda）指示匿名函数抽象的一种有类型的形式化。有类型lambda演算是基础编程语言并且是有类型的函数式编程语言如ML和Haskell和更间接的指令式编程语言的基础。它们通过Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型lambda演算是笛卡尔闭范畴（CCC）的语言。 传统上，有类型lambda演算被看作无类型lambda演算的精细化。更现…
系统F
系统F，也叫做多态lambda演算或二阶lambda演算，是有类型lambda演算。它由逻辑学家和计算机科学家独立发现的。系统F形式化了编程语言中的参数多态的概念。 正如同lambda演算有取值于（range over）函数的变量，和来自它们的粘合子（binder）；二阶lambda演算取值自类型，和来自它们的粘合子。 作为一个例子，恒等函数有形如A→ A的任何类型的事实可以在系统F中被形式化为判断 :\vdash \Lambda\al…
类型居留问题
在简单类型lambda演算中，类型居留（Type inhabitation）问题是如下问题：给定一个类型 \tau，是否存在一个 \lambda-项 M 使得对于某个类型环境 \Gamma 有 \Gamma \vdash M : \tau？在空的类型环境中，如果回答是肯定的，则 M 被称为 \tau 的居留元（inhabitant）。 因为在简单类型的 lambda 演算中类型对应于极小蕴涵逻辑(参见 Curry-Howard 同构)，…
Λ立方
在数理逻辑和类型论中，λ立方是探索Coquand的构造演算中细化轴的框架，以简单类型λ演算（在立方图中写作λ→）作为原点放在立方体的顶点，而构造演算（即高阶依赖类型化λ演算，在图中写作λPω）则是其空间对顶点。立方体的每个轴都表示一种新的抽象形式： 值依赖类型，或多态。系统F，即二阶λ演算（图中写作λ2）就是通过只加入此性质得到的。 类型依赖类型，或类型构造器。带类型构造器的简单类型λ演算（图中为\lambda\underline{\o…
协变与逆变
协变与逆变（Covariance and contravariance）是在计算机科学中，描述具有父/子型别关系的多个型别通过型别构造器、构造出的多个复杂型别之间是否有父/子型别关系的用语。 概述 許多程式設計語言的型別系統支持子型別。例如，如果是的子型別，那麼型別的表達式可用於任何出現型別表達式的地方。所謂的變型（variance）是指如何根據組成型別之間的子型別關係，來確定更複雜的型別之間（例如之於，回傳的函數之於回傳的函數...等…
強弱型別
強弱型別（Strong and weak typing）表示在電腦科學以及程式設計中，經常把程式語言的类型系统分为強型別（）和弱型別（）两种。這兩個術語並沒有非常明確的定義，但主要用以描述程式語言對於混入不同資料型別的值進行運算時的處理方式。強型別的語言遇到函式引數型別和實際叫用型別不符合的情況經常會直接出錯或者編譯失敗；而弱型別的語言常常會實行隐式转换，或者产生难以意料的结果。這對術語在短短的電腦歷史中，早已含括了更多的意義，而且時常…
類型系統
在计算机科学中，类型系統（）用于定義如何將程式語言中的數值和運算式归類为许多不同的型別，如何操作这些型別，这些型別如何互相作用。型別可以确认一个值或者一组值具有特定的意义和目的（雖然某些型別，如抽象型別和函式型別，在程式執行中，可能不表示為值）。型別系統在各種語言之間有非常大的不同，也許，最主要的差異存在於編譯時期的語法，以及執行時期的操作实现方式。 編譯器可能使用值的靜態型別以最佳化所需的儲存區，並選取對值運算時的較佳演算法。例如，在…
型別安全
在電腦科學中，一部分程式語言具備型別安全（-{zh:中國大陸;zh-tw:中國大陸;zh-cn:台湾;}-用語習慣稱型別為-{zh:类型;zh-tw:类型;zh-cn:型别;}-；-{zh:稱資料為数据;zh-tw:稱資料為数据;zh-cn:依据上下文、意思、特定用语的不同，常称数据为资料;}-）的性質。這個術語在不同的社群中有不同的定義，特別是正規的型別理論上的定義遠遠強過大多數的程式員的理解，但對於使用型別系統的認知，皆旨在避免必然…
类型类
在计算机科学中，类型类（type class），是支持特设多态的类型系统构造。这是通过向参数多态类型的类型变量增加约束完成的。这种约束典型的涉及到一个类型类T和一个a，并意味着a所能实例化的类型，其成员必须支持关联于T的重载运算。 类型类首先在Haskell中实现，当时Philip Wadler和Stephen Blott提出它，作为对Standard ML的eqtype的扩展，并且最初构想为以本原方式实现重载算术及等式算符的一种途径。…
参数多态
参数多态在程序设计语言与类型论中是指声明与定义函数、复合类型、变量时不指定其具体的类型，而把这部分类型作为参数使用，使得该定义对各种具体类型都适用。参数化多态使得语言更具表达力，同时保持了完全的静态类型安全。 这被称为泛化函数、泛化数据类型、泛型变量，形成了泛型编程的基础。 概述 参数多态允许函数或数据类型被一般性的书写，从而它可以“统一”的处理值而不用依赖于它们的类型。参数多态是使语言更加有表现力而仍维持完全的静态类型安全的一种方式。…