8. 関手・モナド・do記法（Functors, Monads and do-Notation）🔗

型クラス Functor ・ Applicative ・ Monad は関数型プログラミングの基本的なツールを提供します。 これらの抽象化を用いたプログラミングの入門書として Functional Programming in Lean があります。（訳注：日本語訳は こちら ） これらは圏論における関手とモナドの概念に触発されていますが、プログラミングに使われるバージョンはより限定的です。Lean の標準ライブラリの型クラスは一般的な数学的定義ではなく、プログラミングに使われる概念を表しています。

Functor のインスタンスは、何かしらの操作を多相コンテキスト全体で一貫して適用できるようにします。例えば、関数を適用してリストの各要素を変換したり、既存の IO アクションの結果に純粋関数を適用するようにアレンジして新しい IO アクションを作成したりすることができます。 Monad のインスタンスでは、データに依存する副作用をエンコードすることができます；例えば、タプルを使って可変状態をシミュレートしたり、直和型を使って例外をシミュレートしたり、 IO を使って実際の副作用を表現したりすることができます。 Applicative 関手 はその中間を占めます：モナドのように作用で計算された関数を、作用で計算された引数に適用することができますが、作用の出力が別の作用を持つ操作の入力を形成するような逐次的なデータ依存関係は許可しません。

追加の型クラス 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)

In functional programming, a "functor" is a function on types F : Type u → Type v equipped with an operator called map or <$> such that if f : α → β then map f : F α → F β, so f <$> x : F β if x : F α. This corresponds to the category-theory notion of functor in the special case where the category is the category of types and functions between them, except that this class supplies only the operations and not the laws (see LawfulFunctor).

Instance Constructor

Functor.mk.{u, v}

Methods

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

If f : α → β and x : F α then f <$> x : F β.

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

The special case const a <$> x, which can sometimes be implemented more efficiently.

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

The typeclass which supplies the pure function. See Monad.

Instance Constructor

Pure.mk.{u, v}

Methods

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

If a : α, then pure a : f α represents a monadic action that does nothing and returns a.

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

The typeclass which supplies the <*> "seq" function. See Applicative.

Instance Constructor

Seq.mk.{u, v}

Methods

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

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

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

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

The typeclass which supplies the <* "seqLeft" function. See Applicative.

Instance Constructor

SeqLeft.mk.{u, v}

Methods

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

If x : F α and y : F β, then x <* y evaluates x, then y, and returns the result of x.

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

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

The typeclass which supplies the *> "seqRight" function. See Applicative.

Instance Constructor

SeqRight.mk.{u, v}

Methods

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

If x : F α and y : F β, then x *> y evaluates x, then y, and returns the result of y.

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

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

An applicative functor is an intermediate structure between Functor and Monad. It mainly consists of two operations:

  • pure : α → F α

  • seq : F (α → β) → F α → F β (written as <*>)

The seq operator gives a notion of evaluation order to the effects, where the first argument is executed before the second, but unlike a monad the results of earlier computations cannot be used to define later actions.

Instance Constructor

Applicative.mk.{u, v}

Extends

Methods

map : {α β : Type u} → (α → β) → f α → f β
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
mapConst : {α β : Type u} → α → f β → f α
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
pure : {α : Type u} → α → f α
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
seqRight : {α β : Type u} → f α → (Unit → f β) → f β
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
アプリカティブ関手としての長さ付きリスト

構造体 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 <| α:Type uβ:Type un:Natxs:LenList (n + 1) α⊢ xs.list ≠ [] α:Type uβ:Type un:Natxs:LenList (n + 1) αh:xs.list = []⊢ False α:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:{ list := list✝, lengthOk := lengthOk✝ }.list = []⊢ False α:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:list✝ = []⊢ False All goals completed! 🐙 def LenList.tail (xs : LenList (n + 1) α) : LenList n α := match xs with | ⟨_ :: xs', _⟩ => ⟨xs', α:Type uβ:Type un:Natxs:LenList (n + 1) αhead✝:αxs':List αlengthOk✝:(head✝ :: xs').length = n + 1⊢ xs'.length = n All goals completed! 🐙⟩ def LenList.map (f : α → β) (xs : LenList n α) : LenList n β where list := xs.list.map f lengthOk := α:Type uβ:Type un:Natf:α → βxs:LenList n α⊢ (List.map f xs.list).length = n α:Type uβ:Type un:Natf:α → βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.map f { list := list✝, lengthOk := lengthOk✝ }.list).length = n All goals completed! 🐙 def LenList.zipWith (f : α → β → γ) (xs : LenList n α) (ys : LenList n β) : LenList n γ where list := xs.list.zipWith f ys.list lengthOk := α:Type uβ:Type un:Natf:α → β → γxs:LenList n αys:LenList n β⊢ (List.zipWith f xs.list ys.list).length = n α:Type uβ:Type un:Natf:α → β → γys:LenList n βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.zipWith f { list := list✝, lengthOk := lengthOk✝ }.list ys.list).length = n; α:Type uβ:Type un: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 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 := type mismatch LenList.zipWith (fun x1 x2 => ?m.118) fs (xs ()) has type LenList n γ : Type ?u.101 but is expected to have type LenList n β✝ : Type ?u.10fs.zipWith (type mismatch x1✝ x2✝ has type β✝ : Type ?u.10 but is expected to have type γ : Type ?u.101· ·) (xs ())

行儀よくふるまう Monad インスタンスは関数を適用した結果の対角を取ります：

@[simp] theorem LenList.list_length_eq (xs : LenList n α) : xs.list.length = n := α:Type un:Natxs:LenList n α⊢ xs.list.length = n α:Type un:Natlist✝:List αlengthOk✝:list✝.length = n⊢ { list := list✝, lengthOk := lengthOk✝ }.list.length = n All goals completed! 🐙 def fail to show termination for LenList.diagonal with errors failed to infer structural recursion: Not considering parameter α of LenList.diagonal: it is unchanged in the recursive calls Not considering parameter n of LenList.diagonal: it is unchanged in the recursive calls Cannot use parameter square: the type LenList n (LenList n α) does not have a `.brecOn` recursor failed to prove termination, possible solutions: - Use `have`-expressions to prove the remaining goals - Use `termination_by` to specify a different well-founded relation - Use `decreasing_by` to specify your own tactic for discharging this kind of goal α : Type u n n' : Nat square : LenList (n' + 1) (LenList (n' + 1) α) ⊢ sizeOf (sorry ()) < sizeOf squareLenList.diagonal (square : LenList n (LenList n α)) : LenList n α := match n with | 0 => ⟨[], rfl⟩ | n' + 1 => { list := square.head.head :: application type mismatch diagonal (map (fun x => ?m.284) square.tail) argument map (fun x => ?m.284) square.tail has type LenList n' ?m.279 : Type u but is expected to have type LenList n (LenList n α) : Type u(square.tail.map (·.tail)).diagonal.list, lengthOk := α:Type uβ:Type un:Natn':Natsquare:LenList (n' + 1) (LenList (n' + 1) α)⊢ (square.head.head :: (diagonal sorry).list).length = n' + 1 α:Type uβ:Type un:Natn':Natsquare:LenList (n' + 1) (LenList (n' + 1) α)⊢ n = n' }
🔗type class
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

Methods

map : {α β : Type u} → (α → β) → f α → f β
Inherited from
  1. Applicative f
mapConst : {α β : Type u} → α → f β → f α
Inherited from
  1. Applicative f
pure : {α : Type u} → α → f α
Inherited from
  1. Applicative f
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
Inherited from
  1. Applicative f
seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
Inherited from
  1. Applicative f
seqRight : {α β : Type u} → f α → (Unit → f β) → f β
Inherited from
  1. 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)

The typeclass which supplies the >>= "bind" function. See Monad.

Instance Constructor

Bind.mk.{u, v}

Methods

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

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.

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

A monad is a structure which abstracts the concept of sequential control flow. It mainly consists of two operations:

  • pure : α → F α

  • bind : F α → (α → F β) → F β (written as >>=)

Like many functional programming languages, Lean makes extensive use of monads for structuring programs. In particular, the do notation is a very powerful syntax over monad operations, and it depends on a Monad instance.

See the do notation chapter of the manual for details.

Instance Constructor

Monad.mk.{u, v}

Extends

Methods

map : {α β : Type u} → (α → β) → m α → m β
Inherited from
  1. Applicative m
  2. Bind m
mapConst : {α β : Type u} → α → m β → m α
Inherited from
  1. Applicative m
  2. Bind m
pure : {α : Type u} → α → m α
Inherited from
  1. Applicative m
  2. Bind m
seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β
Inherited from
  1. Applicative m
  2. Bind m
seqLeft : {α β : Type u} → m α → (Unit → m β) → m α
Inherited from
  1. Applicative m
  2. Bind m
seqRight : {α β : Type u} → m α → (Unit → m β) → m β
Inherited from
  1. Applicative m
  2. Bind m
bind : {α β : Type u} → m α → (α → m β) → m β
Inherited from
  1. Applicative m
  2. Bind m
  1. 8.1. 規則（Laws）
  2. 8.2. モナドの持ち上げ（Lifting Monads）
    1. 8.2.1. 持ち上げの引き下げ（Reversing Lifts）
      1. 8.2.1.1. モナド関手（Monad Functors）
      2. 8.2.1.2. MonadControl による持ち上げの引き下げ（Reversible Lifting with MonadControl）
  3. 8.3. 構文（Syntax）
    1. 8.3.1. 中置演算子（Infix Operators）
      1. 8.3.1.1. 関手（Functors）
      2. 8.3.1.2. アプリカティブ関手（Applicative Functors）
      3. 8.3.1.3. モナド（Monads）
    2. 8.3.2. do 記法（do-Notation）
      1. 8.3.2.1. 逐次計算（Sequential Computations）
      2. 8.3.2.2. 早期リターン（Early Return）
      3. 8.3.2.3. ローカルの可変状態（Local Mutable State）
      4. 8.3.2.4. 制御構造（Control Structures）
      5. 8.3.2.5. 反復処理（Iteration）
      6. 8.3.2.6. do ブロックの識別（Identifying do Blocks）
      7. 8.3.2.7. 反復処理のための型クラス（Type Classes for Iteration）
  4. 8.4. API リファレンス（API Reference）
    1. 8.4.1. 結果の破棄（Discarding Results）
    2. 8.4.2. フローの制御（Control Flow）
    3. 8.4.3. 真偽値演算子の持ち上げ（Lifting Boolean Operations）
    4. 8.4.4. Kleisli 合成（Kleisli Composition）
    5. 8.4.5. 並べ替え操作（Re-Ordered Operations）
  5. 8.5. さまざまなモナド（Varieties of Monads）
    1. 8.5.1. モナド型クラス（Monad Type Classes）
    2. 8.5.2. モナド変換子（Monad Transformers）
    3. 8.5.3. 恒等モナド（Identity）
    4. 8.5.4. 状態（State）
      1. 8.5.4.1. 一般的な状態の API（General State API）
      2. 8.5.4.2. タプルベースの状態モナド（Tuple-Based State Monads）
      3. 8.5.4.3. 継続渡しスタイルの状態モナド（State Monads in Continuation Passing Style）
      4. 8.5.4.4. 可変参照からの状態モナド（State Monads from Mutable References）
    5. 8.5.5. リーダ（Reader）
    6. 8.5.6. オプション（Option）
    7. 8.5.7. 例外（Exceptions）
      1. 8.5.7.1. 例外（Exceptions）
      2. 8.5.7.2. 型クラス（Type Class）
      3. 8.5.7.3. 「finally」の計算（“Finally” Computations）
      4. 8.5.7.4. 変換子（Transformer）
      5. 8.5.7.5. 継続渡しスタイルの例外モナド（Exception Monads in Continuation Passing Style）
    8. 8.5.8. エラーと状態モナドの結合（Combined Error and State Monads）
      1. 8.5.8.1. 状態のロールバック（State Rollback）
      2. 8.5.8.2. 実装（Implementations）