7.4. インスタンス導出（Deriving Instances）🔗

Lean は多くのクラスに対して自動的にインスタンスを生成することができます。これはインスタンスの導出（deriving）と呼ばれる処理です。インスタンスの導出は型を定義する時に呼び出すことも、独立したコマンドとして呼び出すこともできます。

syntax

新しい帰納型を作成するコマンドの一部としての Lean.Parser.Command.declaration : commandderiving 句には、その型からインスタンスが生成されるべきクラス名のカンマ区切りのリストを指定します：

optDeriving ::=
    (deriving ident,*)?

syntax

独立した Lean.Parser.Command.deriving : commandderiving コマンドには複数のクラスと対象の名前を指定します。指定された各クラスは指定された各対象に対して導出されます。

command ::= ...
    | deriving instance ident,* for ident,*

複数クラスの導出

このコードのように、複数の型に対して導出する複数のクラスを指定した場合：

structure A where
structure B where

deriving instance BEq, Repr for A, B

すべての型にすべてのインスタンスが存在するため、4つの Lean.Parser.Command.synth : command#synth コマンドはすべて成功します：

instBEqA#synth BEq A
instBEqB#synth BEq B
instReprA#synth Repr A
instReprB#synth Repr B

7.4.1. 導出ハンドラ（Deriving Handlers）🔗

インスタンスの導出は 導出ハンドラ （deriving handler）のテーブルを使用し、型クラス名をインスタンスを導出するメタプログラムにマッピングします。導出ハンドラは registerDerivingHandler を使用してテーブルに追加することができます。これは Lean.Parser.Command.initialize : commandinitialize ブロック内で呼び出す必要があります。それぞれの導出ハンドラは Array Name → CommandElabM Bool 型を持つ必要があります。ユーザがクラスのインスタンス導出を要求すると、登録されているハンドラが1つずつ呼び出されます。これらのハンドラにはインスタンスを導出させる相互ブロック内のすべての名前が提供され、正しくインスタンスを導出した場合は true を、そうでない場合は何もせずに false を返します。ハンドラが true を返すと、それ以降のハンドラは呼び出されません。

Lean には以下のクラスの導出ハンドラがあります：

def

Lean.Elab.registerDerivingHandler
    (className : Name)
    (handler : DerivingHandler) : IO Unit

A DerivingHandler is called on the fully qualified names of all types it is running for as well as the syntax of a with argument, if present.

For example, deriving instance Foo with fooArgs for Bar, Baz invokes fooHandler #[`Bar, `Baz] `(fooArgs).

導出ハンドラ

IsEnum クラスのインスタンスは型に対して適切なサイズの Fin との間に全単射を提供することによって型が有限に列挙されることを示します：

class IsEnum (α : Type) where
  size : Nat
  toIdx : α → Fin size
  fromIdx : Fin size → α
  to_from_id : ∀ (i : Fin size), toIdx (fromIdx i) = i
  from_to_id : ∀ (x : α), fromIdx (toIdx x) = x

帰納型は自明な列挙であり、コンストラクタがパラメータを期待しない帰納型ではこのクラスのインスタンスにおいては非常に繰り返しが多いコードになります。 Bool のインスタンスが典型的です：

instance : IsEnum Bool where
  size := 2
  toIdx
    | false => 0
    | true => 1
  fromIdx
    | 0 => false
    | 1 => true
  to_from_id
    | 0 => rfl
    | 1 => rfl
  from_to_id
    | false => rfl
    | true => rfl

導出ハンドラは IsEnum Bool の実装をなぞるようにそれぞれのパターンのケースをプログラムで構築します：

open Lean Elab Parser Term Command

def deriveIsEnum (declNames : Array Name) : CommandElabM Bool := do
  if h : declNames.size = 1 then
    let env ← getEnv
    if let some (.inductInfo ind) := env.find? declNames[0] then
      let mut tos : Array (TSyntax ``matchAlt) := #[]
      let mut froms := #[]
      let mut to_froms := #[]
      let mut from_tos := #[]
      let mut i := 0

      for ctorName in ind.ctors do
        let c := mkIdent ctorName
        let n := Syntax.mkNumLit (toString i)

        tos      := tos.push      (← `(matchAltExpr| | $c => $n))
        from_tos := from_tos.push (← `(matchAltExpr| | $c => rfl))
        froms    := froms.push    (← `(matchAltExpr| | $n => $c))
        to_froms := to_froms.push (← `(matchAltExpr| | $n => rfl))

        i := i + 1

      let cmd ← `(instance : IsEnum $(mkIdent declNames[0]) where
                    size := $(quote ind.ctors.length)
                    toIdx $tos:matchAlt*
                    fromIdx $froms:matchAlt*
                    to_from_id $to_froms:matchAlt*
                    from_to_id $from_tos:matchAlt*)
      elabCommand cmd

      return true
  return false

initialize
  registerDerivingHandler ``IsEnum deriveIsEnum