Option型
const std = @import("std"); const print = std.io.getStdOut().writer().print; const Compute = struct { value: ?i32, pub fn init(value: ?i32) Compute { return Compute{ .value = value }; } pub fn format( self: @This(), comptime fmt: []const u8, options: std.fmt.FormatOptions, out_stream: anytype, ) !void { _ = fmt; _ = options; if (self.value) |n| { return out_stream.print("The value is: {}", .{n}); } else { return out_stream.print("No value", .{}); } } }; pub fn main() !void { const full = Compute.init(42); const empty = Compute.init(null); try print("full -> {}\n", .{full}); try print("empty -> {}\n", .{empty}); }
それぞれのプログラミング言語において、Option型は様々な名前と定義がある。
Agdaでは、nothingとjust aという要素を持ち、Maybeという名前で定義されている。
Coqでは、Inductive option (A:Type) : Type := | Some : A -> option A | None : option A.として定義されている。
Elmでは、Maybeという名前でtype Maybe a = Just a | Nothingとして定義されている。
Haskellでは、Maybeという名前でdata Maybe a = Nothing | Just aとして定義されている。
Idris(英語版)では、data Maybe a = Nothing | Just aとして定義されている。
型理論において、Option型は A ? = A + 1 {\displaystyle A^{?}=A+1} のように記述することができる。これは与えられた値の組 A {\displaystyle A} に対して、Option型は A {\displaystyle A} の有効な値の組に正確に1つの追加の値(空の値)を追加するという事実を表している。これはタグ付き共用体(英語版)を持つ言語において、Option型がカプセル化型とUnit型(英語版)のタグ付き共用体として表現できるという事実によってプログラミングに反映されている。
カリー=ハワード同型対応において、Option型は∨: x∨1=1の消滅法則に関連している。
Option型は1個または0個の要素を含むコレクション(英語版)と見なすこともできる。
Option型もモナドであり、次のようになる:
Option型のモナディックな性質は、失敗とエラーを効率的に追跡するのに役立つ。