另一个通常无法取得预期类型的情形，是函数应用项中的函数位置。
依赖函数类型很常见；它们与隐式参数一起，使信息从一个实参的精译流向其他实参的精译。
试图根据整个应用项的预期类型以及各实参独立推断出的类型来推导函数所需的类型，往往会失败。
在这些情形下，Lean 使用 CoeFun 类型类，将应用位置中的非函数强制转换为函数。
与 CoeSort 一样，插入函数强制转换时，CoeFun 实例不会与其他强制转换链接；但在普通的强制转换插入期间，它们可以用作 CoeOut 实例。
CoeFun 的第二个参数是一个输出参数，用于确定结果函数类型。
这个输出参数是根据被强制转换的项计算函数类型的函数，而不是函数类型本身。
与 CoeDep 不同，实例合成期间不会考虑项本身；不过，可以用它创建依赖类型的强制转换，使函数类型由该项确定。
term ::= ...
|
结构体 NamedFun α β 将一个从 α 到 β 的函数与一个名称配成一对。
structure NamedFun (α : Type u) (β : Type v) where
function : α → β
name : String
可以给已有函数命名：
def succ : NamedFun Nat Nat where
function n := n + 1
name := "succ"
def asString [ToString α] : NamedFun α String where
function := ToString.toString
name := "asString"
def append : NamedFun (List α) (List α → List α) where
function := (· ++ ·)
name := "append"
命名函数也可以组合：
def NamedFun.comp
(f : NamedFun β γ)
(g : NamedFun α β) :
NamedFun α γ where
function := f.function ∘ g.function
name := f.name ++ " ∘ " ++ g.name
与普通函数不同，命名函数可以合理地表示为字符串：
instance : ToString (NamedFun α α'') where
toString f := s!"#<{f.name}>"
#eval asString.comp succ
CoeFun 实例使它们可以像普通函数一样应用：
instance : CoeFun (NamedFun α α'') (fun _ => α → α'') where
coe | ⟨f, _⟩ => f
#eval append [1, 2, 3] [4, 5, 6]
有时，结果函数的类型取决于被强制转换的具体值。
Writer 表示将某个值的表示追加到字符串的一种方式：
structure Writer where
Writes : Type u
write : Writes → String → String
def natWriter : Writer where
Writes := Nat
write n out := out ++ toString n
def stringWriter : Writer where
Writes := String
write s out := out ++ s
由于内层函数所期待的参数类型取决于 Writer.Writes 字段，CoeFun 实例会提取该字段：
instance :
CoeFun Writer (·.Writes → String → String) where
coe w := w.write
有了这个实例，具体的 Writer 就可以用作函数：
#eval "" |> natWriter (5 : Nat) |> stringWriter " hello"
良类型解释器是一种编程语言解释器，它使用索引族排除运行时类型错误。 在被解释语言中编写的函数可以解释为 Lean 函数，同时也可以检查其底层源代码。
良类型解释器的第一步，是选出可以使用的 Lean 类型子集。
这些类型由代码的归纳类型 Ty 表示，并由一个函数将这些代码映射到实际类型。
inductive Ty where
| nat
| arr (dom cod : Ty)
abbrev Ty.interp : Ty → Type
| .nat => Nat
| .arr t t' => t.interp → t'.interp
语言本身表示为一个以变量上下文和结果类型为索引的索引族。 变量使用 de Bruijn 索引表示。
inductive Tm : List Ty → Ty → Type where
| zero : Tm Γ .nat
| succ (n : Tm Γ .nat) : Tm Γ .nat
| rep (n : Tm Γ .nat)
(start : Tm Γ t)
(f : Tm Γ (.arr .nat (.arr t t))) :
Tm Γ t
| lam (body : Tm (t :: Γ) t') : Tm Γ (.arr t t')
| app (f : Tm Γ (.arr t t')) (arg : Tm Γ t) : Tm Γ t'
| var (i : Fin Γ.length) : Tm Γ Γ[i]
deriving Repr
由于 Fin 的 OfNat 实例要求上界非零，因此将 Tm.var 与数值字面量一起使用可能不方便。
辅助函数 Tm.v 可在这些情况下避免类型标注。
def Tm.v
(i : Fin (Γ.length + 1)) :
Tm (t :: Γ) (t :: Γ)[i] :=
.var (Γ := t :: Γ) i
将两个自然数相加的函数使用 rep 运算重复应用后继 Tm.succ。
def plus : Tm [] (.arr .nat (.arr .nat .nat)) :=
.lam <| .lam <| .rep (.v 1) (.v 0) (.lam (.lam (.succ (.v 0))))
每个类型上下文都可以解释为一种运行时环境类型，为上下文中的每个变量提供值：
def Env : List Ty → Type
| [] => Unit
| t :: Γ => t.interp × Env Γ
def Env.empty : Env [] := ()
def Env.extend (ρ : Env Γ) (v : t.interp) : Env (t :: Γ) :=
(v, ρ)
def Env.get (i : Fin Γ.length) (ρ : Env Γ) : Γ[i].interp :=
match Γ, ρ, i with
| _::_, (v, _), ⟨0, _⟩ => v
| _::_, (_, ρ'), ⟨i+1, _⟩ => ρ'.get ⟨i, Γ:List Tyi✝:Fin Γ.lengthρ:Env Γhead✝:Tytail✝:List Tyfst✝:head✝.interpρ':Env tail✝i:NatisLt✝:i + 1 < (head✝ :: tail✝).length⊢ i < tail✝.length All goals completed! 🐙⟩
最后，解释器是关于项的递归函数：
def Tm.interp (ρ : Env α'') : Tm α'' t → t.interp
| .zero => 0
| .succ n => n.interp ρ + 1
| .rep n start f =>
let f' := f.interp ρ
(n.interp ρ).fold (fun n _ x => f' n x) (start.interp ρ)
| .lam body => fun x => body.interp (ρ.extend x)
| .app f arg => f.interp ρ (arg.interp ρ)
| .var i => ρ.get i
将 Tm 强制转换为函数，就是调用解释器。
instance : CoeFun (Tm [] α'') (fun _ => α''.interp) where
coe f := f.interp .empty
由于函数由一阶归纳类型表示，可以检查其代码：
#eval plus
与此同时，凭借强制转换，它们可以像原生 Lean 函数一样应用：
#eval plus 3 5