Skip to content

Commit

Permalink
Inductive types (#25)
Browse files Browse the repository at this point in the history
  • Loading branch information
@david-christiansen
david-christiansen authored Aug 30, 2024
1 parent 22b7256 commit 17b8f21
Show file tree
Hide file tree
Showing 9 changed files with 2,527 additions and 657 deletions.
132 changes: 98 additions & 34 deletions Manual/Language.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ import VersoManual

import Manual.Meta
import Manual.Language.Files
import Manual.Language.InductiveTypes

open Verso.Genre Manual

Expand All @@ -15,14 +16,30 @@ set_option linter.unusedVariables false

# Types

::: TODO
Basic framework of the type theory goes here.

{deftech}[Canonical] type formers, definitional equality, types as first-class entities, large elimination
:::

## Functions

::: TODO
Write this section.

Topics:
* Dependent vs non-dependent {deftech}[function] types
* Eta equivalence
* Don't talk recursion (that goes in inductive types), but xref to it
* Syntax of anonymous functions with/without pattern matching
* Strictness
:::

## Propositions

Propositions are meaningful statements that admit proof. {index}[proposition]
{deftech}[Propositions] are meaningful statements that admit proof. {index}[proposition]
Nonsensical statements are not propositions, but false statements are.
All propositions are classified by `Prop`.
All propositions are classified by {lean}`Prop`.

Propositions have the following properties:

Expand All @@ -45,8 +62,8 @@ Propositions have the following properties:

## Universes

Types are classified by _universes_. {index}[universe]
Each universe has a {deftech (key:="universe level")}[_level_], {index subterm := "of universe"}[level] which is a natural number.
Types are classified by {deftech}_universes_. {index}[universe]
Each universe has a {deftech (key:="universe level")}_level_, {index subterm := "of universe"}[level] which is a natural number.
The {lean}`Sort` operator constructs a universe from a given level. {index}[`Sort`]
If the level of a universe is smaller than that of another, the universe itself is said to be smaller.
With the exception of propositions (described later in this chapter), types in a given universe may only quantify over types in smaller universes.
Expand All @@ -59,7 +76,7 @@ example : Sort 5 := Sort 4
example : Sort 2 := Sort 1
```

On the other hand, `Sort 3` is not an element of `Sort 5`:
On the other hand, {lean}`Sort 3` is not an element of {lean}`Sort 5`:
```lean (error := true) (name := sort3)
example : Sort 5 := Sort 3
```
Expand All @@ -73,7 +90,7 @@ but is expected to have type
Type 4 : Type 5
```

Similarly, because `Unit` is in `Sort 1`, it is not in `Sort 2`:
Similarly, because {lean}`Unit` is in {lean}`Sort 1`, it is not in {lean}`Sort 2`:
```lean
example : Sort 1 := Unit
```
Expand All @@ -93,7 +110,7 @@ but is expected to have type
Because propositions and data are used differently and are governed by different rules, the abbreviations {lean}`Type` and {lean}`Prop` are provided to make the distinction more convenient. {index}[`Type`] {index}[`Prop`]
`Type u` is an abbreviation for `Sort (u + 1)`, so {lean}`Type 0` is {lean}`Sort 1` and {lean}`Type 3` is {lean}`Sort 4`.
{lean}`Type 0` can also be abbreviated {lean}`Type`, so `Unit : Type` and `Type : Type 1`.
{lean}`Prop` is an abbreviation for `Sort 0`.
{lean}`Prop` is an abbreviation for {lean}`Sort 0`.

### Predicativity

Expand All @@ -102,20 +119,33 @@ A function type's universe is determined by the universes of its argument and re
The specific rules depend on whether the return type of the function is a proposition.

Predicates, which are functions that return propositions (that is, where the result type of the function is some type in `Prop`) may have argument types in any universe whatsoever, but the function type itself remains in `Prop`.
In other words, propositions feature {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] quantification, because propositions can themselves be statements about all propositions.
For example, proof irrelevance can be written as a proposition that quantifies over all propositions:
In other words, propositions feature {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] quantification, because propositions can themselves be statements about all propositions (and all other types).

:::example "Impredicativity"
Proof irrelevance can be written as a proposition that quantifies over all propositions:
```lean
example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2
```

A proposition may also quantify over all types, at any given level:
```lean
example : Prop := ∀ (α : Type), ∀ (x : α), x = x
example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x
```
:::

For universes at {tech key:="universe level"}[level] `1` and higher (that is, the `Type u` hierarchy), quantification is {deftech}[_predicative_]. {index}[predicative]{index subterm := "predicative"}[quantification]
For these universes, the universe of a function type is the least upper bound of the argument and return types' universes.

:::example "Universe levels of function types"
Both of these types are in {lean}`Type 2`:
```lean
example (α : Type 1) (β : Type 2) : Type 2 := α → β
example (α : Type 2) (β : Type 1) : Type 2 := α → β
```
:::

:::example "Predicativity of {lean}`Type`"
This example is not accepted, because `α`'s level is greater than `1`. In other words, the annotated universe is smaller than the function type's universe:
```lean error := true name:=toosmall
example (α : Type 2) (β : Type 1) : Type 1 := α → β
Expand All @@ -128,8 +158,12 @@ has type
but is expected to have type
Type 1 : Type 2
```
:::

Lean's universes are not {deftech}[cumulative];{index}[cumulativity] a type in `Type u` is not automatically also in `Type (u + 1)`.
Each type inhabits precisely one universe.

Lean's universes are not cumulative; a type in `Type u` is not automatically also in `Type (u + 1)`.
:::example "No cumulativity"
This example is not accepted because the annotated universe is larger than the function type's universe:
```lean error := true name:=toobig
example (α : Type 2) (β : Type 1) : Type 3 := α → β
Expand All @@ -142,23 +176,29 @@ has type
but is expected to have type
Type 3 : Type 4
```
:::

### Polymorphism

Lean supports _universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take {deftech}[universe parameters].
Lean supports {deftech}_universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take {deftech}[universe parameters].
These parameters can then be instantiated with universe levels when the constant is used.
Universe parameters are written in curly braces following a dot after a constant name.

:::example "Universe-polymorphic identity function"
When fully explicit, the identity function takes a universe parameter `u`. Its signature is:
```signature
id.{u} {α : Sort u} (x : α) : α
```
:::

Universe variables may additionally occur in universe level expressions, which provide specific universe levels in definitions.
Universe variables may additionally occur in {ref "level-expressions"}[universe level expressions], which provide specific universe levels in definitions.
When the polymorphic definition is instantiated with concrete levels, these universe level expressions are also evaluated to yield concrete levels.

In this example, a structure is in a universe that is one greater than the universe of the type it contains:
```lean (keep := true)
::::keepEnv
:::example "Universe level expressions"

In this example, {lean}`Codec` is in a universe that is one greater than the universe of the type it contains:
```lean
structure Codec.{u} : Type (u + 1) where
type : Type u
encode : Array UInt32 → type → Array UInt32
Expand All @@ -179,8 +219,13 @@ def Codec.char : Codec where
else
failure
```
:::
::::

Universe-polymorphic definitions in fact create a _schematic definition_ that can be instantiated at a variety of levels, and different instantiations of universes create incompatible values.

:::example "Universe polymorhism is not first-class"

This can be seen in the following example, in which `T` is a gratuitously-universe-polymorphic definition that always returns the constructor of the unit type.
Both instantiations of `T` have the same value, and both have the same type, but their differing universe instantiations make them incompatible:
```lean (error := true) (name := uniIncomp) (keep := false)
Expand All @@ -199,14 +244,13 @@ but is expected to have type
Eq.{1} T.{u} T.{v} : Prop
```

```lean (error := false) (name := uniIncomp) (keep := false)
```lean (error := false) (keep := false) (show := false)
-- check that the above statement stays true
abbrev T : Unit := (fun (α : Type) => ()) Unit

set_option pp.universes true

def test : T = T := rfl
```
:::

Auto-bound implicit arguments are as universe-polymorphic as possible.
Defining the identity function as follows:
Expand All @@ -217,6 +261,8 @@ results in the signature:
```signature
id'.{u} {α : Sort u} (x : α) : α
```

:::example "Universe monomorphism in auto-bound implicit"
On the other hand, because {name}`Nat` is in universe {lean}`Type 0`, this function automatically ends up with a concrete universe level for `α`, because `m` is applied to both {name}`Nat` and `α`, so both must have the same type and thus be in the same universe:
```lean
partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do
Expand All @@ -237,8 +283,12 @@ info: count.{u_1} {m : Type → Type u_1} {α : Type} [Monad m] (p : α → Bool
#guard_msgs in
#check count
```
:::

#### Level Expressions
%%%
tag := "level-expressions"
%%%

Levels that occur in a definition are not restricted to just variables and addition of constants.
More complex relationships between universes can be defined using level expressions.
Expand All @@ -256,37 +306,44 @@ The `imax` operation is defined as follows:

$$``\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}``

`imax` is used to implement impredicative quantification for {lean}`Prop`.
`imax` is used to implement {tech}[impredicative] quantification for {lean}`Prop`.
In particular, if `A : Sort u` and `B : Sort v`, then `(x : A) → B : Sort (imax u v)`.
If `B : Prop`, then the function type is itself a `Prop`; otherwise, the function type's level is the maximum of `u` and `v`.
If `B : Prop`, then the function type is itself a {lean}`Prop`; otherwise, the function type's level is the maximum of `u` and `v`.

#### Universe Variable Bindings

Universe-polymorphic definitions bind universe variables.
These bindings may be either explicit or implicit.
Explicit universe variable binding and instantiaion occurs as a suffix to the definition's name, as in the following declaration of `map`, which declares two universe parameters (`u` and `v`) and instantiates the polymorphic `List` with each in turn:
```lean (keep := false)
def map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List.{u} α → List.{v} β
| [] => []
| x :: xs => f x :: map f xs
```
Explicit universe variable binding and instantiation occurs as a suffix to the definition's name.
Universe parameters are defined or provided by suffixing the name of a constant with a period (`.`) followed by a comma-separated sequence of universe variables between curly braces.

Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters:
```lean (keep := false)
def map.{u} {α : Type u} {β : Type v} (f : α → β) : List α → List β
::::keepEnv
:::example "Universe-polymorphic `map`"
The following declaration of {lean}`map` declares two universe parameters (`u` and `v`) and instantiates the polymorphic {name}`List` with each in turn:
```lean
def map.{u, v} {α : Type u} {β : Type v}
(f : α → β) :
List.{u} α → List.{v} β
| [] => []
| x :: xs => f x :: map f xs
```
:::
::::

When the {TODO}[describe this option and add xref] `autoImplicit` option is set, it is not necessary to explicitly bind universe variables:
Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters.
When the {TODO}[describe this option and add xref] `autoImplicit` option is set to {lean}`true` (the default), it is not necessary to explicitly bind universe variables.
When it is set to {lean}`false`, then they must be added explicitly or declared using the `universe` command. {TODO}[xref]

::: example "Auto-implicits and universe polymorphism"
When `autoImplicit` is {lean}`true` (which is the default setting), this definition is accepted even though it does not bind its universe parameters:
```lean (keep := false)
set_option autoImplicit true
def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
| [] => []
| x :: xs => f x :: map f xs
```

Without this setting, the definition is rejected because `u` and `v` are not in scope:
When `autoImplicit` is {lean}`false`, the definition is rejected because `u` and `v` are not in scope:
```lean (error := true) (name := uv)
set_option autoImplicit false
def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
Expand All @@ -299,6 +356,7 @@ unknown universe level 'u'
```leanOutput uv
unknown universe level 'v'
```
:::

In addition to using `autoImplicit`, particular identifiers can be declared as universe variables in a particular {tech}[scope] using the `universe` command.

Expand All @@ -309,17 +367,21 @@ universe $x:ident $xs:ident*

Declares one or more universe variables for the extent of the current scope.

Just as the `variable` command causes a particular identifier to be treated as a parameter with a paricular type, the `universe` command causes the subsequent identifiers to be treated consistently as universe parameters, even if they are not mentioned in a signature or if the option `autoImplicit` is {lean}`false`.
Just as the `variable` command causes a particular identifier to be treated as a parameter with a particular type, the `universe` command causes the subsequent identifiers to be implicitly quantified as as universe parameters in declarations that mention them, even if the option `autoImplicit` is {lean}`false`.
:::

When `u` is declared to be a universe variable, it can be used as a parameter.
:::example "The `universe` command when `autoImplicit` is `false`"
```lean
set_option autoImplicit false
universe u
def id₃ (α : Type u) (a : α) := a
```
:::

Because automatic implicit arguments only insert parameters that are used in the declaration's {tech}[header], universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declared with `universe` even when `autoImplicit` is `true`.

:::example "Automatic universe parameters and the `universe` command"

Because automatic implicit arguments only insert parameters that are used in the declaration's {tech}[header], universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declaread with `universe` even when `autoImplicit` is `true`.
This definition with an explicit universe parameter is accepted:
```lean (keep := false)
def L.{u} := List (Type u)
Expand All @@ -338,12 +400,14 @@ universe u
def L := List (Type u)
```
The resulting definition of `L` is universe-polymorphic, with `u` inserted as a universe parameter.

Declarations in the scope of a `universe` command are not made polymorphic if the universe variables do not occur in them or in other automatically-inserted arguments.
```lean
universe u
def L := List (Type 0)
#check L
```
:::

#### Universe Unification

Expand All @@ -352,7 +416,7 @@ def L := List (Type 0)
* Lack of injectivity
:::

## Inductive Types
{include 2 Language.InductiveTypes}


# Organizational Features
Expand Down
2 changes: 1 addition & 1 deletion Manual/Language/Files.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ Such identifier components may contain any character at all, aside from `'»'`,
Some potential identifier components may be reserved keywords.
The specific set of reserved keywords depends on the set of active syntax extensions, which may depend on the set of imported modules and the currently-opened {TODO}[xref/deftech for namespace] namespaces; it is impossible to enumerate for Lean as a whole.
These keywords must also be quoted with guillemets to be used as identifier components in most syntactic contexts.
Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive datatypes, are _raw identifier_ contexts.{index (subterm:="raw")}[identifier]
Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive datatypes, are {deftech}_raw identifier_ contexts.{index (subterm:="raw")}[identifier]

Identifiers that contain one or more `'.'` characters, and thus consist of more than one identifier component, are called {deftech}[hierarchical identifiers].
Hierarchical identifiers are used to represent both module names and names in a namespace.
Expand Down
Loading

0 comments on commit 17b8f21

Please sign in to comment.