doc: documentation for Init.Coe
This commit is contained in:
Mario Carneiro
Leonardo de Moura
parent
0d27c5c5cd
commit
b0db7deeef
4 changed files with 188 additions and 15 deletions
|
|
@ -1,45 +1,207 @@
|
|||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
Authors: Leonardo de Moura, Mario Carneiro
|
||||
-/
|
||||
prelude
|
||||
import Init.Prelude
|
||||
set_option linter.missingDocs true -- keep it documented
|
||||
|
||||
/-!
|
||||
# Coercion
|
||||
|
||||
Lean uses a somewhat elaborate system of typeclasses to drive the coercion system.
|
||||
Here a *coercion* means an invisible function that is automatically inserted
|
||||
to fix what would otherwise be a type error. For example, if we have:
|
||||
```
|
||||
def f (x : Nat) : Int := x
|
||||
```
|
||||
then this is clearly not type correct as is, because `x` has type `Nat` but
|
||||
type `Int` is expected, and normally you will get an error message saying exactly that.
|
||||
But before it shows that message, it will attempt to synthesize an instance of
|
||||
`CoeT Nat x Int`, which will end up going through all the other typeclasses defined
|
||||
below, to discover that there is an instance of `Coe Nat Int` defined.
|
||||
|
||||
This instance is defined as:
|
||||
```
|
||||
instance : Coe Nat Int := ⟨Int.ofNat⟩
|
||||
```
|
||||
so Lean will elaborate the original function `f` as if it said:
|
||||
```
|
||||
def f (x : Nat) : Int := Int.ofNat x
|
||||
```
|
||||
which is not a type error anymore.
|
||||
|
||||
You can also use the `↑` operator to explicitly indicate a coercion. Using `↑x`
|
||||
instead of `x` in the example will result in the same output.
|
||||
Because there are many polymorphic functions in Lean, it is often ambiguous where
|
||||
the coercion can go. For example:
|
||||
```
|
||||
def f (x y : Nat) : Int := x + y
|
||||
```
|
||||
This could be either `↑x + ↑y` where `+` is the addition on `Int`, or `↑(x + y)`
|
||||
where `+` is addition on `Nat`, or even `x + y` using a heterogeneous addition
|
||||
with the type `Nat → Nat → Int`. You can use the `↑` operator to disambiguate
|
||||
between these possibilities, but generally Lean will elaborate working from the
|
||||
"outside in", meaning that it will first look at the expression `_ + _ : Int`
|
||||
and assign the `+` to be the one for `Int`, and then need to insert coercions
|
||||
for the subterms `↑x : Int` and `↑y : Int`, resulting in the `↑x + ↑y` version.
|
||||
|
||||
## Important typeclasses
|
||||
|
||||
* `Coe α β` is the most basic class, and the usual one you will want to use
|
||||
when implementing a coercion for your own types.
|
||||
|
||||
* `CoeDep α (x : α) β` allows `β` to depend not only on `α` but on the value
|
||||
`x : α` itself. This is useful when the coercion function is dependent.
|
||||
An example of a dependent coercion is the instance for `Prop → Bool`, because
|
||||
it only holds for `Decidable` propositions. It is defined as:
|
||||
```
|
||||
instance (p : Prop) [Decidable p] : CoeDep Prop p Bool := ...
|
||||
```
|
||||
|
||||
* `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. This is automatically turned into `CoeFun.coe f x`.
|
||||
|
||||
* `CoeSort α β` is a coercion to a sort. `β` must be a universe, and if
|
||||
`a : α` appears in a place where a type is expected, like `(x : a)` or `a → a`,
|
||||
then it will be turned into `(x : CoeSort.coe a)`.
|
||||
|
||||
* `CoeHead` is like `Coe`, but while `Coe` can be transitively chained in the
|
||||
`CoeT` class, `CoeHead` can only appear once and only at the start of such a
|
||||
chain. This is useful when the transitive instances are not well behaved.
|
||||
|
||||
* `CoeTail` is similar: it can only appear at the end of a chain of coercions.
|
||||
|
||||
* `CoeT α (x : α) β` itself is the combination of all the aforementioned classes
|
||||
(except `CoeSort` and `CoeFun` which have different triggers). You can
|
||||
implement `CoeT` if you do not want this coercion to be transitively composed
|
||||
with any other coercions.
|
||||
|
||||
Note that unlike most operators like `+`, `↑` is always eagerly unfolded at
|
||||
parse time into its definition. So if we look at the definition of `f` from
|
||||
before, we see no trace of the `CoeT.coe` function:
|
||||
```
|
||||
def f (x : Nat) : Int := x
|
||||
#print f
|
||||
-- def f : Nat → Int :=
|
||||
-- fun (x : Nat) => Int.ofNat x
|
||||
```
|
||||
-/
|
||||
|
||||
universe u v w w'
|
||||
|
||||
/--
|
||||
`Coe α β` is the typeclass for coercions from `α` to `β`. It can be transitively
|
||||
chained with other `Coe` instances, and coercion is automatically used when
|
||||
`x` has type `α` but it is used in a context where `β` is expected.
|
||||
You can use the `↑x` operator to explicitly trigger coercion.
|
||||
-/
|
||||
class Coe (α : Sort u) (β : Sort v) where
|
||||
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
|
||||
or by double type ascription `((x : α) : β)`. -/
|
||||
coe : α → β
|
||||
|
||||
/-- Auxiliary class that contains the transitive closure of `Coe`. -/
|
||||
/--
|
||||
Auxiliary class that contains the transitive closure of `Coe`.
|
||||
Users should generally not implement this directly.
|
||||
-/
|
||||
class CoeTC (α : Sort u) (β : Sort v) where
|
||||
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
|
||||
or by double type ascription `((x : α) : β)`. -/
|
||||
coe : α → β
|
||||
|
||||
/-- Expensive coercion that can only appear at the beginning of a sequence of coercions. -/
|
||||
/--
|
||||
`CoeHead α β` is for coercions that can only appear at the beginning of a
|
||||
sequence of coercions. That is, `β` can be further coerced via `Coe β γ` and
|
||||
`CoeTail γ δ` instances but `α` will only be the inferred type of the input.
|
||||
-/
|
||||
class CoeHead (α : Sort u) (β : Sort v) where
|
||||
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
|
||||
or by double type ascription `((x : α) : β)`. -/
|
||||
coe : α → β
|
||||
|
||||
/-- Expensive coercion that can only appear at the end of a sequence of coercions. -/
|
||||
/--
|
||||
`CoeTail α β` is for coercions that can only appear at the end of a
|
||||
sequence of coercions. That is, `α` can be further coerced via `Coe σ α` and
|
||||
`CoeHead τ σ` instances but `β` will only be the expected type of the expression.
|
||||
-/
|
||||
class CoeTail (α : Sort u) (β : Sort v) where
|
||||
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
|
||||
or by double type ascription `((x : α) : β)`. -/
|
||||
coe : α → β
|
||||
|
||||
/-- Auxiliary class that contains `CoeHead` + `CoeTC` + `CoeTail`. -/
|
||||
/--
|
||||
Auxiliary class that contains `CoeHead` + `CoeTC` + `CoeTail`.
|
||||
|
||||
A `CoeHTCT` chain has the "grammar" `(CoeHead)? (Coe)* (CoeTail)?`, except that
|
||||
the empty sequence is not allowed.
|
||||
-/
|
||||
class CoeHTCT (α : Sort u) (β : Sort v) where
|
||||
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
|
||||
or by double type ascription `((x : α) : β)`. -/
|
||||
coe : α → β
|
||||
|
||||
/--
|
||||
`CoeDep α (x : α) β` is a typeclass for dependent coercions, that is, the type `β`
|
||||
can depend on `x` (or rather, the value of `x` is available to typeclass search
|
||||
so an instance that relates `β` to `x` is allowed).
|
||||
|
||||
Dependent coercions do not participate in the transitive chaining process of
|
||||
regular coercions: they must exactly match the type mismatch on both sides.
|
||||
-/
|
||||
class CoeDep (α : Sort u) (_ : α) (β : Sort v) where
|
||||
/-- The resulting value of type `β`. The input `x : α` is a parameter to
|
||||
the type class, so the value of type `β` may possibly depend on additional
|
||||
typeclasses on `x`. -/
|
||||
coe : β
|
||||
|
||||
/-- Combines CoeHead, CoeTC, CoeTail, CoeDep -/
|
||||
/--
|
||||
`CoeT` is the core typeclass which is invoked by Lean to resolve a type error.
|
||||
It can also be triggered explicitly with the notation `↑x` or by double type
|
||||
ascription `((x : α) : β)`.
|
||||
|
||||
A `CoeT` chain has the "grammar" `(CoeHead)? (Coe)* (CoeTail)? | CoeDep`,
|
||||
except that the empty sequence is not allowed (identity coercions don't need
|
||||
the coercion system at all).
|
||||
-/
|
||||
class CoeT (α : Sort u) (_ : α) (β : Sort v) where
|
||||
/-- The resulting value of type `β`. The input `x : α` is a parameter to
|
||||
the type class, so the value of type `β` may possibly depend on additional
|
||||
typeclasses on `x`. -/
|
||||
coe : β
|
||||
|
||||
class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where
|
||||
coe : (a : α) → γ a
|
||||
|
||||
/--
|
||||
`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. This is automatically turned into `CoeFun.coe f x`.
|
||||
-/
|
||||
class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where
|
||||
/-- 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`. -/
|
||||
coe : (f : α) → γ f
|
||||
|
||||
/--
|
||||
`CoeSort α β` is a coercion to a sort. `β` must be a universe, and if
|
||||
`a : α` appears in a place where a type is expected, like `(x : a)` or `a → a`,
|
||||
then it will be turned into `(x : CoeSort.coe a)`.
|
||||
-/
|
||||
class CoeSort (α : Sort u) (β : outParam (Sort v)) where
|
||||
/-- Coerces a value of type `α` to `β`, which must be a universe. -/
|
||||
coe : α → β
|
||||
|
||||
/--
|
||||
`↑x` represents a coercion, which converts `x` of type `α` to type `β`, using
|
||||
typeclasses to resolve a suitable conversion function. You can often leave the
|
||||
`↑` off entirely, since coercion is triggered implicitly whenever there is a
|
||||
type error, but in ambiguous cases it can be useful to use `↑` to disambiguate
|
||||
between e.g. `↑x + ↑y` and `↑(x + y)`.
|
||||
-/
|
||||
syntax:1024 (name := coeNotation) "↑" term:1024 : term
|
||||
|
||||
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [Coe β δ] [CoeTC α β] : CoeTC α δ where
|
||||
|
|
@ -100,13 +262,24 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead (Subtype p) α whe
|
|||
|
||||
/-! # Coe bridge -/
|
||||
|
||||
-- Helper definition used by the elaborator. It is not meant to be used directly by users
|
||||
@[inline] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
|
||||
/--
|
||||
Helper definition used by the elaborator. It is not meant to be used directly by users.
|
||||
|
||||
This is used for coercions between monads, in the case where we want to apply
|
||||
a monad lift and a coercion on the result type at the same time.
|
||||
-/
|
||||
@[inline] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
|
||||
[MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
|
||||
let a ← liftM x
|
||||
pure (CoeT.coe a)
|
||||
|
||||
-- Helper definition used by the elaborator. It is not meant to be used directly by users
|
||||
@[inline] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
|
||||
/--
|
||||
Helper definition used by the elaborator. It is not meant to be used directly by users.
|
||||
|
||||
This is used for coercing the result type under a monad.
|
||||
-/
|
||||
@[inline] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
|
||||
[∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
|
||||
let a ← x
|
||||
pure (CoeT.coe a)
|
||||
|
||||
|
|
|
|||
|
|
@ -1425,7 +1425,7 @@ private def tryCoeSort (α : Expr) (a : Expr) : TermElabM Expr := do
|
|||
if (← synthesizeCoeInstMVarCore mvarId) then
|
||||
let result ← expandCoe <| mkAppN (Lean.mkConst ``CoeSort.coe [u, v]) #[α, β, mvar, a]
|
||||
unless (← isType result) do
|
||||
throwError "failed to coerse{indentExpr a}\nto a type, after applying `CoeSort.coe`, result is still not a type{indentExpr result}\nthis is often due to incorrect `CoeSort` instances, the synthesized value for{indentExpr coeSortInstType}\nwas{indentExpr mvar}"
|
||||
throwError "failed to coerce{indentExpr a}\nto a type, after applying `CoeSort.coe`, result is still not a type{indentExpr result}\nthis is often due to incorrect `CoeSort` instances, the synthesized value for{indentExpr coeSortInstType}\nwas{indentExpr mvar}"
|
||||
return result
|
||||
else
|
||||
throwError "type expected"
|
||||
|
|
|
|||
|
|
@ -264,7 +264,7 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
|
|||
@[builtinTermParser] def noindex := leading_parser "no_index " >> termParser maxPrec
|
||||
|
||||
@[builtinTermParser] def binrel := leading_parser "binrel% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
|
||||
/-- Similar to `binrel`, but coerse `Prop` arguments into `Bool`. -/
|
||||
/-- Similar to `binrel`, but coerce `Prop` arguments into `Bool`. -/
|
||||
@[builtinTermParser] def binrel_no_prop := leading_parser "binrel_no_prop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
|
||||
@[builtinTermParser] def binop := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
|
||||
@[builtinTermParser] def binop_lazy := leading_parser "binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
621.lean:4:45-4:47: error: type expected
|
||||
failed to coerse
|
||||
failed to coerce
|
||||
xs
|
||||
to a type, after applying `CoeSort.coe`, result is still not a type
|
||||
xs.val
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue