Functor

Functor は圏論における 関手(functor) という概念からその名がある型クラスで、非常に雑な表現をすると、この型クラスを実装した型は「値を包んでいるコンテナのようなもの」として扱うことができます。特定のデータ構造に「包まれて」いる中の値に対して関数を適用していくという操作を行いたいことがありますが、Functor のインスタンスはそれを可能にします。

より詳細には、F : Type u → Type v に対して Functor はおおむね次のように定義されています。

universe u v

/-- 関手 -/
class Functor (F : Type u → Type v) : Type (max (u+1) v) where
  /-- 関数 `f : α → β` を関数 `F α → F β` に変換する -/
  map : {α β : Type u} → (α → β) → F α → F β

  /-- `a : α` に対して、定数関数 `const a : β → α` を関数 `F β → F α` に変換する。
  `map` を使うよりも効率的に実装できることがあるので、上書きできるように用意されている。-/
  mapConst : {α β : Type u} → α → F β → F α := Function.comp map (Function.const _)

つまり、Functor のインスタンスは map メソッドが使用できます。これは型からわかるように、関数を関数に写す高階関数で、「普通の関数 f : α → β」を「F に包まれた関数 F α → F β」に持ち上げます。Functor.map はよく使われる操作であるため、<$> という専用の記法が用意されています。

-- `F` は Functor であると仮定
variable (F : Type → Type) [Functor F]

-- 関数 `g : α → β` と `x : F α` が与えられたとする
variable {α β : Type} (g : α → β)

-- 高階関数を返す
#check (Functor.map g : F α → F β)

-- `<$>` は `map` と同じ
example (x : F α) : g <$> x = Functor.map g x := rfl

典型的なインスタンス

List

Functor 型クラスの典型的なインスタンスのひとつが List です。これにより「リストの各要素に関数を適用する」ための簡単な方法が提供されます。

-- リストの各要素を２倍する
#guard (fun x => x * 2) <$> [1, 2, 3, 4, 5] = [2, 4, 6, 8, 10]

Option

Option も Functor 型クラスのインスタンスになっています。これにより「x? : Option が some x の場合に関数を適用し、none なら none を返す」という操作のための簡単な方法が提供されます。

#guard (fun x => x * 2) <$> some 2 = some 4
#guard (fun x => x * 2) <$> (none : Option Nat) = none

Id

Id : Type u → Type u は「何もしない」関手です。

/- info: 20 -/
#eval (· * 2) <$> (10 : Id Nat)

(A → ·)

任意の型 A : Type u に対して、fun X => (A → X) という対応は関手になります。

section

  /-- 型から、その型への関数型を返す -/
  abbrev Hom (A : Type) (X : Type) := A → X

  /-- 関数合成を map として `Hom A` は関手になる -/
  instance {A : Type} : Functor (Hom A) where
    map f g := f ∘ g

  #guard
    let doubleLength : Hom String Nat := (· * 2) <$> String.length
    doubleLength "hello" = 10 && doubleLength "world!" = 12

end

上記で定義した Hom は Lean の標準ライブラリでは ReaderM と呼ばれます。

/-- 上で定義した Hom は ReaderM に等しい -/
example (A : Type) : ReaderM A = Hom A := rfl

(A × ·)

任意の型 A : Type に対して、A との直積を取る対応 fun X => A × X は関手になります。

section
  -- 最初 Functor インスタンスは用意されていない
  #check_failure (· * 2) <$> ("hello", 20)

  abbrev prodWith (A : Type) (X : Type) := A × X

  local instance {A : Type} : Functor (prodWith A) where
    map f := fun (a, x) => (a, f x)

  #guard (· * 2) <$> ("hello", 20) = ("hello", 40)
end

(A ⊕ ·)

任意の型 A : Type に対して、A との直和を取る対応 fun X => A ⊕ X は関手になります。

section
  -- 最初 Functor インスタンスは用意されていない
  #check_failure (· * 2) <$> (Sum.inr 20 : String ⊕ Nat)

  abbrev sumWith (A : Type) (X : Type) := Sum A X

  local instance {A : Type} : Functor (sumWith A) where
    map f := fun z =>
      match z with
      | .inl a => Sum.inl a
      | .inr x => Sum.inr (f x)

  #eval (· * 2) <$> (Sum.inr 20 : String ⊕ Nat)
end

Functor 則

Functor 型クラスのインスタンスには満たすべきルールがあります。このルールを破っていても Functor 型クラスのインスタンスにすることは可能ですが、避けるべきです。Functor 型クラスがルールを満たしていることを証明するためには、LawfulFunctor 型クラスを使います。

Lean by Example