CoeFun

CoeFun クラスのインスタンスを与えると、関数ではない項を関数型に強制することができます。

/-- 加法的な関数の全体 -/
structure AdditiveFunction : Type where
  /-- 関数部分 -/
  toFun : Nat → Nat

  /-- 加法を保つ -/
  additive : ∀ x y, toFun (x + y) = toFun x + toFun y

/-- 恒等写像 -/
def identity : AdditiveFunction := ⟨id, by intro _ _; rfl⟩

-- `identity` の型は `AdditiveFunction` であって、関数ではないのでこれはエラーになる
#check_failure (identity 1)

-- 関数に変換してからならOK
#check (identity.toFun 1)

-- `CoeFun` を使って関数への変換を自動化する
local instance : CoeFun AdditiveFunction (fun _ => Nat → Nat) where
  coe f := f.toFun

-- まるで関数のように使えるようになる
#check (identity 1)

上記の例ではどんな t : AdditiveFunction も同じ型 Nat → Nat に強制していますが、実際には依存関数型に強制することができます。

Coe との違い

上記の例を、Coe を使って再現しようとして下記のようにしても上手くいかないことに注意して下さい。

-- `Coe` で `Nat → Nat` への変換を自動化しようとしている例
local instance : Coe AdditiveFunction (Nat → Nat) where
  coe f := f.toFun

-- `Nat → Nat` への型強制が呼び出されず、エラーになってしまう
-- これは、期待されている型が `Nat → Nat` ではなく、単に `Nat → ?_` であるため。
/--
warning: function expected at
  identity
term has type
  AdditiveFunction
-/
#guard_msgs in
  #check_failure (identity 1)

-- 期待される型を明記すればエラーにならない
#check ((identity : Nat → Nat) 1)