Init.Control.Id

Id definition

(type : Type u) : Type u

Full source

/--
The identity function on types, used primarily for its `Monad` instance.

The identity monad is useful together with monad transformers to construct monads for particular
purposes. Additionally, it can be used with `do`-notation in order to use control structures such as
local mutability, `for`-loops, and early returns in code that does not otherwise use monads.

Examples:
```lean example
def containsFive (xs : List Nat) : Bool := Id.run do
  for x in xs do
    if x == 5 then return true
  return false
```

```lean example
#eval containsFive [1, 3, 5, 7]
```
```output
true
```
-/
def Id (type : Type u) : Type u := type

Identity type constructor

Informal description

The identity type constructor, which maps any type `type` to itself. This is primarily used for its monad instance, enabling monadic operations like `do`-notation to be used in non-monadic contexts for control flow and local mutability.

Id.instMonad instance

: Monad Id

Full source

@[always_inline]
instance : Monad Id where
  pure x := x
  bind x f := f x
  map f x := f x

Monad Instance for Identity Type

Informal description

The identity type constructor `Id` forms a monad, where the `pure` operation is the identity function and the `bind` operation is function application.

Id.hasBind definition

: Bind Id

Full source

/--
The identity monad has a `bind` operator.
-/
def hasBind : Bind Id :=
  inferInstance

Bind operation for the identity monad

Informal description

The identity monad has a bind operation `>>=` defined, which is simply function application.

Id.run definition

(x : Id α) : α

Full source

/--
Runs a computation in the identity monad.

This function is the identity function. Because its parameter has type `Id α`, it causes
`do`-notation in its arguments to use the `Monad Id` instance.
-/
@[always_inline, inline]
protected def run (x : Id α) : α := x

Run identity monad computation

Informal description

The function `Id.run` takes a value `x` of type `Id α` and returns the underlying value of type `α`. It is essentially the identity function, used to run computations in the identity monad.

Id.instOfNat instance

[OfNat α n] : OfNat (Id α) n

Full source

instance [OfNat α n] : OfNat (Id α) n :=
  inferInstanceAs (OfNat α n)

Numeric Literal Interpretation for Identity Type Constructor

Informal description

For any type $\alpha$ with a numeric literal interpretation (i.e., an instance of `OfNat α n` for some natural number $n$), the identity type constructor `Id α` also inherits this interpretation. Specifically, any numeric literal that can be interpreted as an element of $\alpha$ can also be interpreted as an element of `Id α$.