Lean 语言参考

11.4. 强制转换为函数类型🔗

预期类型通常不可用的另一种情况是函数应用术语中的函数位置。 依赖函数类型很常见；它们与 隐式 参数一起，导致信息从一个参数的精化流向其他参数的精化。 尝试从整个应用程序术语的预期类型和单独推断的参数类型来推断函数所需的类型通常会失败。 在这些情况下，Lean 使用 CoeFun 类型类将应用程序位置中的非函数强制为函数。 与 CoeSort 一样，CoeFun 实例在插入函数强制转换时不会与其他强制转换链接，但它们可以在普通强制插入期间用作 CoeOut 实例。

CoeFun 的第二个参数是输出参数，用于确定结果函数类型。 此输出参数是根据被强制转换的项计算函数类型的函数，而不是函数类型本身。 与 CoeDep 不同，在实例合成期间不考虑该术语本身；但是，它可以用于创建依值类型的强制转换，其中函数类型由术语确定。

🔗type class
CoeFun.{u, v} (α : Sort u) (γ : outParam (α → Sort v)) :
  Sort (max (max 1 u) v)
CoeFun.{u, v} (α : Sort u)
  (γ : outParam (α → Sort v)) :
  Sort (max (max 1 u) v)

CoeFun α (γ : α → Sort v) is a coercion to a function. γ a should be a (coercion-to-)function type, and this is triggered whenever an element f : α appears in an application like f x, which would not make sense since f does not have a function type. CoeFun instances apply to CoeOut as well.

Instance Constructor

CoeFun.mk.{u, v}

Methods

coe : (f : α) → γ f

Coerces a value f : α to type γ f, which should be either be a function type or another CoeFun type, in order to resolve a mistyped application f x.

syntaxExplicit Coercion to Functions
term ::= ...
    | `⇑ t` coerces `t` to a function. ⇑ term
Coercing Decorated Functions to Function Types

结构 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}>" #<asString ∘ succ>#eval asString.comp succ 
#<asString ∘ succ>

CoeFun 实例允许它们像普通函数一样应用：

instance : CoeFun (NamedFun α α'') (fun _ => α → α'') where coe | ⟨f, _⟩ => f [1, 2, 3, 4, 5, 6]#eval append [1, 2, 3] [4, 5, 6] 
[1, 2, 3, 4, 5, 6]
Live ↪
Dependent Coercion to Functions

有时，结果函数的类型取决于被强制转换的特定值。 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 可以用作函数：

"5 hello"#eval "" |> natWriter (5 : Nat) |> stringWriter " hello" 
"5 hello"
Live ↪
Coercing to Function Types

类型良好的解释器是一种编程语言的解释器，它使用索引族来排除运行时类型错误。 用解释语言编写的函数可以解释为 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

由于函数由一阶归纳类型表示，因此可以检查它们的代码：

Tm.lam (Tm.lam (Tm.rep (Tm.var 1) (Tm.var 0) (Tm.lam (Tm.lam (Tm.succ (Tm.var 0))))))#eval plus 
Tm.lam (Tm.lam (Tm.rep (Tm.var 1) (Tm.var 0) (Tm.lam (Tm.lam (Tm.succ (Tm.var 0))))))

同时，由于强制，它们可以像本机 Lean 函数一样应用：

8#eval plus 3 5 
8
Live ↪