DerivingHandler

Lean.Elab.DerivingHandler は、型クラスのインスタンスの自動生成を行うための関数の型で、Array Name → CommandElabM Bool という型と等しいものです。

import Lean

open Lean Elab Command

example : DerivingHandler = (Array Name → CommandElabM Bool) := by
  rfl

deriving ハンドラの登録

deriving コマンドを使用したときに、対応する DerivingHandler 型の関数が呼び出されます。

簡単な例として、任意の型から Unit への自明な関数を提供する ToUnit という型クラスを考えてみましょう。この型クラスが与える変換は自明なので、どんな型に対しても実装方法は「わかりきって」おり自動生成できそうです。

/-- `Unit`への変換方法を与える自明な型クラス -/
class ToUnit (α : Type) where
  toUnit : α → Unit

/-- `Nat`における `ToUnit` のインスタンス -/
instance : ToUnit Nat where
  toUnit _ := ()

/-- `String`における `ToUnit` のインスタンス -/
instance : ToUnit String where
  toUnit _ := ()

#guard ToUnit.toUnit 42 = ()
#guard ToUnit.toUnit "hello" = ()

この型クラスに対して deriving コマンドが使えるようにするには、まず以下のように記述したファイルを作成し、deriving ハンドラを登録します。

import Lean
import LeanByExample.Type.DerivingHandler.ToUnit

open Lean Elab Command

/-- `ToUnit` のためのインスタンス自動導出関数 -/
def deriveToUnitInstance (declNames : Array Name) : CommandElabM Bool := do
  for declName in declNames do
    let term := mkCIdent declName
    let cmd ← `(command| instance : ToUnit $term := ⟨fun _ => ()⟩)
    elabCommand cmd
  return true

initialize
  registerDerivingHandler ``ToUnit deriveToUnitInstance

そうすると、このファイルを import することで以下のように使用できるようになります。

import LeanByExample.Type.DerivingHandler.Lib

-- 最初はインスタンスがない
#check_failure ToUnit.toUnit true

-- `deriving` コマンドを使用
deriving instance ToUnit for Bool, Int, Char

-- インスタンスが生成された！
#guard ToUnit.toUnit true = ()
#guard ToUnit.toUnit (42 : Int) = ()
#guard ToUnit.toUnit 'a' = ()