18. 函子、Monad 和 `do` 表示法🔗

类型类 Functor、Applicative 和 Monad 提供了函数式编程的基本工具。Lean函数式编程 中提供了使用这些抽象进行编程的介绍。虽然它们受到范畴论中函子和单子概念的启发，但用于编程的版本更加有限。 Lean 标准库中的类型类表示用于编程的概念，而不是一般的数学定义。

Functor 的实例允许在整个多态上下文中一致地应用操作。示例包括通过应用函数来转换列表的每个元素，以及通过安排将纯函数应用于现有 IO 操作的结果来创建新的 IO 操作。 Monad的实例允许对具有数据依赖性的副作用进行编码；示例包括使用元组来模拟可变状态、使用求和类型来模拟异常以及使用 IO 表示实际副作用。 Applicative 函子占据中间立场：与 monad 一样，它们允许将使用效果计算的函数应用于使用效果计算的参数，但它们不允许顺序数据依赖关系，其中效果的输出形成另一个有效操作的输入。

附加类型类 Pure、Bind、SeqLeft、SeqRight 和 Seq 捕获来自 Applicative 和 Monad 的各个操作，允许它们重载并与不一定是 Applicative 的类型一起使用函子或 Monad。 Alternative 类型类描述了另外具有一些失败和恢复概念的应用函子。

type class

Functor.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Functor.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

A functor in the sense used in functional programming, which means a function f : Type u → Type v has a way of mapping a function over its contents. This map operator is written <$>, and overloaded via Functor instances.

This map function should respect identity and function composition. In other words, for all terms v : f α, it should be the case that:

id <$> v = v
For all functions h : β → γ and g : α → β, (h ∘ g) <$> v = h <$> g <$> v

While all Functor instances should live up to these requirements, they are not required to prove that they do. Proofs may be required or provided via the LawfulFunctor class.

Assuming that instances are lawful, this definition corresponds to the category-theoretic notion of functor in the special case where the category is the category of types and functions between them.

Instance Constructor

Functor.mk.{u, v}

Methods

map : {α β : Type u} → (α → β) → f α → f β

Applies a function inside a functor. This is used to overload the <$> operator.

When mapping a constant function, use Functor.mapConst instead, because it may be more efficient.

Conventions for notations in identifiers:

The recommended spelling of <$> in identifiers is map.

mapConst : {α β : Type u} → α → f β → f α

Mapping a constant function.

Given a : α and v : f β, mapConst a v is equivalent to (fun _ => a) <$> v. For some functors, this can be implemented more efficiently; for all other functors, the default implementation may be used.

type class

Pure.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Pure.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

The pure function is overloaded via Pure instances.

Pure is typically accessed via Monad or Applicative instances.

Instance Constructor

Pure.mk.{u, v}

Methods

pure : {α : Type u} → α → f α

Given a : α, then pure a : f α represents an action that does nothing and returns a.

Examples:

(pure "hello" : Option String) = some "hello"
(pure "hello" : Except (Array String) String) = Except.ok "hello"
(pure "hello" : StateM Nat String).run 105 = ("hello", 105)

type class

Seq.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Seq.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

The <*> operator is overloaded using the function Seq.seq.

While <$> from the class Functor allows an ordinary function to be mapped over its contents, <*> allows a function that's “inside” the functor to be applied. When thinking about f as possible side effects, this captures evaluation order: seq arranges for the effects that produce the function to occur prior to those that produce the argument value.

For most applications, Applicative or Monad should be used rather than Seq itself.

Instance Constructor

Seq.mk.{u, v}

Methods

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

The implementation of the <*> operator.

In a monad, mf <*> mx is the same as do let f ← mf; x ← mx; pure (f x): it evaluates the function first, then the argument, and applies one to the other.

To avoid surprising evaluation semantics, mx is taken "lazily", using a Unit → f α function.

Conventions for notations in identifiers:

The recommended spelling of <*> in identifiers is seq.

type class

SeqLeft.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
SeqLeft.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

The <* operator is overloaded using seqLeft.

When thinking about f as potential side effects, <* evaluates first the left and then the right argument for their side effects, discarding the value of the right argument and returning the value of the left argument.

For most applications, Applicative or Monad should be used rather than SeqLeft itself.

Instance Constructor

SeqLeft.mk.{u, v}

Methods

seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

Sequences the effects of two terms, discarding the value of the second. This function is usually invoked via the <* operator.

Given x : f α and y : f β, x <* y runs x, then runs y, and finally returns the result of x.

The evaluation of the second argument is delayed by wrapping it in a function, enabling “short-circuiting” behavior from f.

Conventions for notations in identifiers:

The recommended spelling of <* in identifiers is seqLeft.

type class

SeqRight.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
SeqRight.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

The *> operator is overloaded using seqRight.

When thinking about f as potential side effects, *> evaluates first the left and then the right argument for their side effects, discarding the value of the left argument and returning the value of the right argument.

For most applications, Applicative or Monad should be used rather than SeqRight itself.

Instance Constructor

SeqRight.mk.{u, v}

Methods

seqRight : {α β : Type u} → f α → (Unit → f β) → f β

Sequences the effects of two terms, discarding the value of the first. This function is usually invoked via the *> operator.

Given x : f α and y : f β, x *> y runs x, then runs y, and finally returns the result of y.

The evaluation of the second argument is delayed by wrapping it in a function, enabling “short-circuiting” behavior from f.

Conventions for notations in identifiers:

The recommended spelling of *> in identifiers is seqRight.

type class

Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Applicative.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

An applicative functor is more powerful than a Functor, but less powerful than a Monad.

Applicative functors capture sequencing of effects with the <*> operator, overloaded as seq, but not data-dependent effects. The results of earlier computations cannot be used to control later effects.

Applicative functors should satisfy four laws. Instances of Applicative are not required to prove that they satisfy these laws, which are part of the LawfulApplicative class.

Instance Constructor

Applicative.mk.{u, v}

Extends

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

Methods

map : {α β : Type u} → (α → β) → f α → f β

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

mapConst : {α β : Type u} → α → f β → f α

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

pure : {α : Type u} → α → f α

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

seqRight : {α β : Type u} → f α → (Unit → f β) → f β

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

Lists with Lengths as Applicative Functors

结构 LenList 将列表与具有所需长度的证明配对。因此，如果输入长度不同，其 zipWith 运算符不需要回退。

structure LenList (length : Nat) (α : Type u) where
  list : List α
  lengthOk : list.length = length

def LenList.head (xs : LenList (n + 1) α) : α :=
  xs.list.head <| byα:Type uβ:Type un:Natxs:LenList (n + 1) α⊢ xs.list ≠ []
    intro hα:Type uβ:Type un:Natxs:LenList (n + 1) αh:xs.list = []⊢ False
    cases xsmkα:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:{ list := list✝, lengthOk := lengthOk✝ }.list = []⊢ False
    simp_allmkα:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:list✝ = []⊢ False
    subst_eqsAll goals completed! 🐙

def LenList.tail (xs : LenList (n + 1) α) : LenList n α :=
  match xs with
  | ⟨_ :: xs', _⟩ => ⟨xs', byα:Type uβ:Type un:Natxs:LenList (n + 1) αhead✝:αxs':List αlengthOk✝:(head✝ :: xs').length = n + 1⊢ xs'.length = n simp_allAll goals completed! 🐙⟩

def LenList.map (f : α → β) (xs : LenList n α) : LenList n β where
  list := xs.list.map f
  lengthOk := byα:Type uβ:Type un:Natf:α → βxs:LenList n α⊢ (List.map f xs.list).length = n
    cases xsmkα:Type uβ:Type un:Natf:α → βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.map f { list := list✝, lengthOk := lengthOk✝ }.list).length = n
    simp [List.length_map, *]All goals completed! 🐙

def LenList.zipWith (f : α → β → γ)
    (xs : LenList n α) (ys : LenList n β) :
    LenList n γ where
  list := xs.list.zipWith f ys.list
  lengthOk := byα:Type uβ:Type uγ:Type ?u.15n:Natf:α → β → γxs:LenList n αys:LenList n β⊢ (List.zipWith f xs.list ys.list).length = n
    cases xsmkα:Type uβ:Type uγ:Type ?u.15n:Natf:α → β → γys:LenList n βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.zipWith f { list := list✝, lengthOk := lengthOk✝ }.list ys.list).length = n; cases ysmk.mkα:Type uβ:Type uγ:Type ?u.15n:Natf:α → β → γlist✝¹:List αlengthOk✝¹:list✝.length = nlist✝:List βlengthOk✝:list✝.length = n⊢ (List.zipWith f { list := list✝¹, lengthOk := lengthOk✝¹ }.list { list := list✝, lengthOk := lengthOk✝ }.list).length =
  n
    simp [List.length_zipWith, *]All goals completed! 🐙

行为良好的 Applicative 实例将函数按元素应用于参数。由于 Applicative 扩展了 Functor，因此不需要单独的 Functor 实例，并且 map 可以定义为 Applicative 实例的一部分。

instance : Applicative (LenList n) where
  map := LenList.map
  pure x := {
    list := List.replicate n x
    lengthOk := List.length_replicate
  }
  seq {α β} fs xs := fs.zipWith (· ·) (xs ())

表现良好的 Monad 实例采用应用函数结果的对角线：

@[simp]
theorem LenList.list_length_eq (xs : LenList n α) :
    xs.list.length = n := byα:Type un:Natxs:LenList n α⊢ xs.list.length = n
  cases xsmkα:Type un:Natlist✝:List αlengthOk✝:list✝.length = n⊢ { list := list✝, lengthOk := lengthOk✝ }.list.length = n
  simp [*]All goals completed! 🐙

def LenList.diagonal (square : LenList n (LenList n α)) : LenList n α :=
  match n with
  | 0 => ⟨[], rfl⟩
  | n' + 1 => {
    list :=
      square.head.head :: (square.tail.map (·.tail)).diagonal.list
    lengthOk := byα:Type uβ:Type un:Natn':Natsquare:LenList (n' + 1) (LenList (n' + 1) α)⊢ (square.head.head :: (diagonal (map (fun x => x.tail) square.tail)).list).length = n' + 1 simpAll goals completed! 🐙
  }

Live ↪

type class

Alternative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Alternative.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

An Alternative functor is an Applicative functor that can "fail" or be "empty" and a binary operation <|> that “collects values” or finds the “left-most success”.

Important instances include

Option, where failure := none and <|> returns the left-most some.
Parser combinators typically provide an Applicative instance for error-handling and backtracking.

Error recovery and state can interact subtly. For example, the implementation of Alternative for OptionT (StateT σ Id) keeps modifications made to the state while recovering from failure, while StateT σ (OptionT Id) discards them.

Instance Constructor

Alternative.mk.{u, v}

Extends

Applicative f

Methods

map : {α β : Type u} → (α → β) → f α → f β

Inherited from

Applicative f

mapConst : {α β : Type u} → α → f β → f α

Inherited from

Applicative f

pure : {α : Type u} → α → f α

Inherited from

Applicative f

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

Inherited from

Applicative f

seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

Inherited from

Applicative f

seqRight : {α β : Type u} → f α → (Unit → f β) → f β

Inherited from

Applicative f

failure : {α : Type u} → f α

Produces an empty collection or recoverable failure. The <|> operator collects values or recovers from failures. See Alternative for more details.

orElse : {α : Type u} → f α → (Unit → f α) → f α

Depending on the Alternative instance, collects values or recovers from failures by returning the leftmost success. Can be written using the <|> operator syntax.

type class

Bind.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
Bind.{u, v} (m : Type u → Type v) :
  Type (max (u + 1) v)

The >>= operator is overloaded via instances of bind.

Bind is typically used via Monad, which extends it.

Instance Constructor

Bind.mk.{u, v}

Methods

bind : {α β : Type u} → m α → (α → m β) → m β

Sequences two computations, allowing the second to depend on the value computed by the first.

If x : m α and f : α → m β, then x >>= f : m β represents the result of executing x to get a value of type α and then passing it to f.

Conventions for notations in identifiers:

The recommended spelling of >>= in identifiers is bind.

type class

Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
Monad.{u, v} (m : Type u → Type v) :
  Type (max (u + 1) v)

Monads are an abstraction of sequential control flow and side effects used in functional programming. Monads allow both sequencing of effects and data-dependent effects: the values that result from an early step may influence the effects carried out in a later step.

The Monad API may be used directly. However, it is most commonly accessed through do-notation.

Most Monad instances provide implementations of pure and bind, and use default implementations for the other methods inherited from Applicative. Monads should satisfy certain laws, but instances are not required to prove this. An instance of LawfulMonad expresses that a given monad's operations are lawful.

Instance Constructor

Monad.mk.{u, v}

Extends

Applicative m
Bind m

Methods

map : {α β : Type u} → (α → β) → m α → m β

Inherited from

Applicative m
Bind m

mapConst : {α β : Type u} → α → m β → m α

Inherited from

Applicative m
Bind m

pure : {α : Type u} → α → m α

Inherited from

Applicative m
Bind m

seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β

Inherited from

Applicative m
Bind m

seqLeft : {α β : Type u} → m α → (Unit → m β) → m α

Inherited from

Applicative m
Bind m

seqRight : {α β : Type u} → m α → (Unit → m β) → m β

Inherited from

Applicative m
Bind m

bind : {α β : Type u} → m α → (α → m β) → m β

Inherited from

Applicative m
Bind m

18. 函子、Monad 和 do 表示法🔗

Instance Constructor

Methods

Instance Constructor

Methods

Instance Constructor

Methods

Instance Constructor

Methods

Instance Constructor

Methods

Instance Constructor

Extends

Methods

Instance Constructor

Extends

Methods

Instance Constructor

Methods

Instance Constructor

Extends

Methods

18. 函子、Monad 和 `do` 表示法🔗