#synth
型クラス C
と型 T
があるとき、#synth C T
は T
が C
のインスタンスになっているかチェックします。もしインスタンスでなかった場合にはエラーになります。
型クラスとは
型クラスとは、複数の型に対して共通の機能や実装を提供するものです。具体例を見てみましょう。たとえば逆数は、複数の型に対して定義されています。
-- `⁻¹` で逆数を表すことができる
#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.
-/
#guard_msgs in #check (_ : α)⁻¹
一般の型に対して逆数は定義できないので、エラーになってしまいました。エラーメッセージで α
は Inv
のインスタンスではないと言われています。この Inv
が型クラスです。Inv
のインスタンスであるような型 T
に対しては、逆数関数 (·)⁻¹ : T → T
が定義できるというわけです。
インスタンスとは
例えば実数 ℝ
に対して逆数は定義できるだろうと予想されますが、実際 ℝ
は Inv
のインスタンスであることが確認できます。
/-- info: Real.instInv -/
#guard_msgs in #synth Inv Real
自然数 ℕ
に対しては逆数が定義されていないと予想されますが、実際 Inv
のインスタンスになっていません。
-- エラーになってしまう
/--
error: failed to synthesize
Inv ℕ
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in #synth Inv Nat
-- Inv のインスタンスになっていない
#check_failure (inferInstance : Inv Nat)
自分で無理やり ℕ
を Inv
のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に 1
になる定数関数としてみましょう。
instance : Inv Nat := ⟨fun _ => 1⟩
#synth Inv Nat
example : (1 : ℕ)⁻¹ = 1 := by rfl