选项类型

在编程语言（尤其是函数式编程语言）和类型理论中，选项类型或也许类型是一种多态类型，它表示对可选值的封装；例如，它被用作函数的返回类型，这些函数在应用时可能返回也可能不返回一个有意义的值。它由一个构造函数组成，这个构造函数要么是空的（通常命名为None或Nothing），要么是封装了原始数据类型A（通常写成JustA或SomeA）。在函数式编程之外的一个独特但相关的概念，在面向对象编程中很流行，它被称为可空类型（通常表示为A?）选项类型和可空类型的核心区别在于，选项类型支持嵌套（例如：Maybe(MaybeString)≠MaybeString），而可空类型不支持嵌套（例如：String??=String?）。理论方面(了解如何以及何时删除此模板信息)在类型理论中，它可以写成。.这表达了这样一个事实：对于给定的一组值，在{displaystyleA}中的一个给定的值集，一个选项类型正好为该值集增加了一个额外的值（空值）。

的有效值集，一个选项类型正好增加了一个额外的值（空值）。{displaystyleA}的有效值集合中增加一个额外的值（空值）。.这反映在编程中，在具有标记联盟的语言中，选项类型可以被表达为封装类型和单元类型的标记联盟。在Curry-Howard对应中，选项类型与∨的湮灭法则有关：x∨1=1。一个选项类型也可以看成是一个包含一个或零个元素的集合。选项类型也是一个单体，其中。选项类型的单体性质对于有效地跟踪失败和错误非常有用。

Agda在Agda中，选项类型被命名为Maybe，其变体是nothing和justa。Coq在Coq中，选项类型被定义为Inductiveoption(A:Type)。Type:=|Some:A->optionA|None:optionA.。Scala在Scala中，选项类型被定义为密封的抽象类Option[+A]，该类型由finalcaseclassSome[+A](value:A)和caseobjectNone扩展。showValue(full)->值是。