Applicative

Applicative 型クラスは、Functor 型クラスの拡張であり、Monad 型クラスよりは制限された中間的な構造です。関数適用を一般化であり、計算効果をエンコードするものと見なすことができます。

定義

Applicative 型クラスは、大雑把に書けば次のように定義されています。(実際の定義はもっと複雑です)

class Applicative.{u, v} (f : Type u → Type v) where
  /-- `a : α` が与えられたとき、`pure a : f α` は「何もせずに `a` を返すアクション」を表す。 -/
  pure {α : Type u} : α → f α

  /--
  `<*>` 演算子の実装。
  モナドにおいては、`mf <*> mx` は `do let f ← mf; x ← mx; pure (f x)` と同じになる。
  つまり、まず関数を評価し、次に引数を評価して適用する。
  予期しない順序で評価されることを避けるために、`mx` は `Unit → f α` という関数を使って遅延的に取得される。
  -/
  seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

すなわち、関数 F : Type → TypeApplicative 型クラスのインスタンスにするということは、pure : α → F α(· <*> ·) : F (α → β) → F α → F β を定義するということです。

/-- 標準にある`Option`を真似て構成した関手 -/
inductive MyOption (α : Type) where
  | none
  | some (a : α)

/-- `MyOption`を`Applicative`のインスタンスにする -/
instance : Applicative MyOption where
  pure a := MyOption.some a
  seq f a :=
    match f, a () with
    | .some f, .some a => .some (f a)
    | _, _ => .none

Functor との関係

Applicative のインスタンスであるならば、自動的に Functor のインスタンスにもなります。これは、Functor.map を次のように実装することができるからです。

instance {F : Type → Type} [Applicative F]: Functor F where
  map f x := pure f <*> x

なぜ「関数適用の一般化」なのか

Functor.map メソッドは (α → β) → F α → F β という型を持ちます。これは、F = Id の場合を考えてみると分かるように、1引数の関数適用を一般化したものだと考えることができます。では2引数、3引数の時はどうなるでしょうか?

単純に拡張すると、2引数の時は (α → β → γ) → F α → F β → F γ という型になり、3引数の時は (α → β → γ → δ) → F α → F β → F γ → F δ という型になります。これらを Functor.map を使って表現するのは困難です。

しかし、FApplicative 型クラスのインスタンスになっていれば、n 引数の場合でも表現することができます。1

variable {α β γ δ : Type}
variable {F : Type → Type} [Applicative F]

/-- 1引数の場合 -/
example : (α → β) → F α → F β := fun f x =>
  pure f <*> x

/-- 2引数の場合 -/
example : (α → β → γ) → F α → F β → F γ := fun f x y =>
  pure f <*> x <*> y

/-- 3引数の場合 -/
example : (α → β → γ → δ) → F α → F β → F γ → F δ := fun f x y z =>
  pure f <*> x <*> y <*> z

  1. ここでの説明は 「プログラミングHaskell 第2版」(Graham Hutton 著、山本和彦訳)を参考にしました。