11.3. 强制排序🔗

Lean精化器期望类型位于某些位置，但不一定能够提前确定类型的 universe。例如，定义标题中冒号后面的术语可能是命题或类型。普通强制转换机制不适用，因为它需要特定的预期类型，并且无法表示预期类型可以是 Coe 类中的 any Universe。

当在预期命题或类型的位置详细精化术语，但所精化术语的推断类型不是命题或类型时，Lean 尝试通过合成 CoeSort 的实例来从错误中恢复。如果找到实例，并且结果类型本身就是一种类型，则插入并展开强制转换。

并非精化器需要 Universe 的所有情况都需要 CoeSort。在某些情况下，特定的 Universe 可用作预期类型。在这些情况下，使用使用 CoeT 的普通强制插入。 CoeSort 的实例可用于合成 CoeOut 的实例，因此不需要单独的实例来支持此用例。一般来说，类型强制应实现为 CoeSort。

type class

CoeSort.{u, v} (α : Sort u) (β : outParam (Sort v)) :
  Sort (max (max 1 u) v)
CoeSort.{u, v} (α : Sort u)
  (β : outParam (Sort v)) :
  Sort (max (max 1 u) v)

CoeSort α β is a coercion to a sort. β must be a universe, and this is triggered when a : α appears in a place where a type is expected, like (x : a) or a → a. CoeSort instances apply to CoeOut as well.

Instance Constructor

CoeSort.mk.{u, v}

Methods

coe : α → β

Coerces a value of type α to β, which must be a universe.

syntaxExplicit Coercion to Sorts

term ::= ...
    | `↥ t` coerces `t` to a type. ↥ term

可以使用 ↥ 前缀运算符显式触发排序强制。

Sort Coercions

幺半群是一种配备有关联二元运算和单位元素的类型。虽然幺半群结构可以定义为类型类，但它也可以定义为将结构与类型“捆绑”的结构：

structure Monoid where
  Carrier : Type u
  op : Carrier → Carrier → Carrier
  id : Carrier
  op_assoc :
    ∀ (x y z : Carrier), op x (op y z) = op (op x y) z
  id_op_identity : ∀ (x : Carrier), op id x = x
  op_id_identity : ∀ (x : Carrier), op x id = x

类型 Monoid 不指示运营商：

def StringMonoid : Monoid where
  Carrier := String
  op := (· ++ ·)
  id := ""
  op_assoc := by⊢ ∀ (x y z : String), x ++ (y ++ z) = x ++ y ++ z introsx✝:Stringy✝:Stringz✝:String⊢ x✝ ++ (y✝ ++ z✝) = x✝ ++ y✝ ++ z✝; simp [String.append_assoc]All goals completed! 🐙
  id_op_identity := by⊢ ∀ (x : String), "" ++ x = x introsx✝:String⊢ "" ++ x✝ = x✝; simpAll goals completed! 🐙
  op_id_identity := by⊢ ∀ (x : String), x ++ "" = x introsx✝:String⊢ x✝ ++ "" = x✝; simpAll goals completed! 🐙

但是，当在 Lean 需要类型的位置使用幺半群时，可以实现应用 Monoid.Carrier 投影的 CoeSort 实例：

instance : CoeSort Monoid (Type u) where
  coe m := m.Carrier

example : StringMonoid := "hello"

Live ↪

Sort Coercions as Ordinary Coercions

归纳类型 NatOrBool 代表类型 Nat 和 Bool。它们可以强制转换为实际类型 Nat 和 Bool：

inductive NatOrBool where
  | nat | bool

@[coe]
abbrev NatOrBool.asType : NatOrBool → Type
  | .nat => Nat
  | .bool => Bool

instance : CoeSort NatOrBool Type where
  coe := NatOrBool.asType

open NatOrBool

当 nat 出现在冒号右侧时，使用 CoeSort 实例：

def x : nat := 5

当预期类型可用时，将使用普通的强制插入。在本例中，CoeSort 实例用于合成 CoeOut NatOrBool Type 实例，该实例与 Coe Type (Option Type) 实例链接以从类型错误中恢复。

def y : Option Type := bool

Live ↪