#synth

型クラス C と型 T があるとき、#synth C TTC のインスタンスになっているかチェックします。もしインスタンスでなかった場合にはエラーになります。

型クラスとは

型クラスとは、複数の型に対して共通の機能や実装を提供するものです。具体例を見てみましょう。たとえば逆数は、複数の型に対して定義されています。

-- `⁻¹` で逆数を表すことができる #check (1 : ℚ)⁻¹ -- 実数として見ても同じ #check (1 : ℝ)⁻¹

逆数をとる関数 fun x => x⁻¹ の定義域はどうなっているのでしょうか?定義域を一般の型 α に拡張してみて、どうなるか見てみましょう。

variable (α : Type) /- error: failed to synthesize Inv α Additional diagnostic information may be available using the `set_option diagnostics true` command. -/ #check (_ : α)⁻¹

一般の型に対して逆数は定義できないので、エラーになってしまいました。エラーメッセージで αInv のインスタンスではないと言われています。この Inv が型クラスです。Inv のインスタンスであるような型 T に対しては、逆数関数 (·)⁻¹ : T → T が定義できるというわけです。

インスタンスとは

例えば実数 に対して逆数は定義できるだろうと予想されますが、実際 Inv のインスタンスであることが確認できます。

/- info: Real.instInv -/ #synth Inv Real

自然数 に対しては逆数が定義されていないと予想されますが、実際 Inv のインスタンスになっていません。

-- エラーになってしまう /- error: failed to synthesize Inv ℕ Additional diagnostic information may be available using the `set_option diagnostics true` command. -/ #synth Inv Nat -- Inv のインスタンスになっていない #check_failure (inferInstance : Inv Nat)

自分で無理やり Inv のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に 1 になる定数関数としてみましょう。

instance : Inv Nat := ⟨fun _ => 1#synth Inv Nat example : (1 : ℕ)⁻¹ = 1 := by rfl