12.9. ユニット型（The Unit Type）

ユニット型は最も情報量の少ない型です。これは、値は必要だがそれ以上の情報は必要ない場合に使用されます。ユニット型には2種類あります：

  • Unit は Type であり、最小の非命題 宇宙 に存在します。

悩ましい場合は、宇宙に関するエラーが発生するまでは Unit を使ってください。

🔗def
Unit : Type

The unit type, the canonical type with one element, named unit or (). In other words, it describes only a single value, which consists of said constructor applied to no arguments whatsoever. The Unit type is similar to void in languages derived from C.

Unit is actually defined as PUnit.{1} where PUnit is the universe polymorphic version. The Unit should be preferred over PUnit where possible to avoid unnecessary universe parameters.

In functional programming, Unit is the return type of things that "return nothing", since a type with one element conveys no additional information. When programming with monads, the type m Unit represents an action that has some side effects but does not return a value, while m α would be an action that has side effects and returns a value of type α.

🔗def
Unit.unit : Unit

Unit.unit : Unit is the canonical element of the unit type. It can also be written as ().

🔗inductive type
PUnit.{u} : Sort u

The unit type, the canonical type with one element, named unit or (). This is the universe-polymorphic version of Unit; it is preferred to use Unit instead where applicable. For more information about universe levels: Types as objects

Constructors

unit.{u} : PUnit

PUnit.unit : PUnit is the canonical element of the unit type.

12.9.1. Definitional Equality

unit-like 型 （unit-like type）は非証明のパラメータを取らない単一のコンストラクタを持つ帰納型です。 PUnit はそのような型の1つです。unit-like 型のすべての要素は、他のすべての要素と definitionally equal です。

Unit の definitional equality

Unit 型を持つすべての項は、 Unit 型を持つすべての項と definitionally equal tです：

example (e1 e2 : Unit) : e1 = e2 := rfl
unit-like 型の definitional equality

CustomUnit と AlsoUnit はどちらも unit-like 型であり、パラメータを取らないコンストラクタを1つ持ちます。どちらの型を持つ項のペアも definitionally equal tです。

inductive CustomUnit where | customUnit example (e1 e2 : CustomUnit) : e1 = e2 := rfl structure AlsoUnit where example (e1 e2 : AlsoUnit) : e1 = e2 := rfl

WithParam のようなパラメータを持つ型も、パラメータを取らないコンストラクタが1つあれば unit-like です。

inductive WithParam (n : Nat) where | mk example (x y : WithParam 3) : x = y := rfl

証明ではないパラメータを持つコンストラクタは、パラメータがすべて unit-like 型であっても unit-like になりません。

inductive NotUnitLike where | mk (u : Unit) example (e1 e2 : NotUnitLike) : e1 = e2 := type mismatch rfl has type ?m.13 = ?m.13 : Prop but is expected to have type e1 = e2 : Proprfl 
type mismatch
  rfl
has type
  ?m.13 = ?m.13 : Prop
but is expected to have type
  e1 = e2 : Prop

unit-like 型のコンストラクタは証明であるパラメータを取ることができます。

inductive ProofUnitLike where | mk : 2 = 2 → ProofUnitLike example (e1 e2 : ProofUnitLike) : e1 = e2 := rfl