diff options
| -rw-r--r-- | plt/lean.md | 297 |
1 files changed, 271 insertions, 26 deletions
diff --git a/plt/lean.md b/plt/lean.md index 695d45c..9aae9fa 100644 --- a/plt/lean.md +++ b/plt/lean.md @@ -16,17 +16,20 @@ I found it hard to get started with, however. This guide is an attempt at remedy - Evaluation - Assignment - Data Types - - Structural Types + - [Structural Types](#structural-types) + - [Products](#products) - Inductive Types - - Booleans - - Numbers - - Lists + - [Sums](#sums) + - [Booleans](#booleans) + - [Numbers](#numbers) + - [Lists](#lists) + - [Strings](#strings) - Classes -- Coersion -- Errors -- [Iteration](#iteration) -- IO + - Coersion - Monads + - IO + - Errors + - [Iteration](#iteration) - Modules - Macros - Proof @@ -37,18 +40,28 @@ I found it hard to get started with, however. This guide is an attempt at remedy First: where is the documentation? -The primary source of documentation is the [Lean source code documentation](https://leanprover-community.github.io/mathlib4_docs/). Despite the URL, it covers more than just mathlib - also generating docs from the (heavily commented) standard library and compiler code base. Lean does not have a comprehensive reference manual, but these docs are as close as it gets. +The primary source of documentation is the [Lean source code documentation][Main Docs]. Despite the URL, it covers more than just mathlib - also generating docs from the (heavily commented) standard library and compiler code base. Lean does not have a comprehensive reference manual, but these docs are as close as it gets. -The secondary source of documentation is the [Lean Zulip](https://leanprover.zulipchat.com/). Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, <span title="Though, it doesn't seem to be indexed by Google.">indexable</span> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderfully nice and very knowledgeable people: with both channels for compiler development and new-to-Lean questions alike. +The secondary source of documentation is the [Lean Zulip]. Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, <span title="Though, it doesn't seem to be indexed by Google.">indexable</span> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderfully nice and very knowledgeable people: with both channels for compiler development and new-to-Lean questions alike. There is additionally the [official documentation page](https://lean-lang.org/documentation/) and the [unofficial documentation page](https://leanprover-community.github.io/learn.html), which together catalogue most all of the other learning resources available for Lean. -There are also several books written for Lean. Depending on what you want to do, [*Theorem Proving in Lean*](https://leanprover.github.io/theorem_proving_in_lean4/introduction.html) or [*Functional Programming in Lean*](https://leanprover.github.io/functional_programming_in_lean/introduction.html) are alternately recommended. There are a good deal more, which I have not read: -- [*Mathematics in Lean*](https://leanprover-community.github.io/mathematics_in_lean/) -- [*The Mechanics of Proof*](https://hrmacbeth.github.io/math2001/) -- [*The Hitchhiker's Guide to Logical Verification*](https://browncs1951x.github.io/static/files/hitchhikersguide.pdf) -- [*Metaprogramming in Lean*](https://leanprover-community.github.io/lean4-metaprogramming-book/) - -Finally, there is [the Lean manual](https://lean-lang.org/lean4/doc/). It is *very* much a work in progress, and contains plenty of blank pages: but, I've found some sections helpful on occasion. +There are also several books written for Lean. Depending on what you want to do, *[Functional Programming in Lean]* or *[Theorem Proving in Lean]* are alternately recommended. There are a good deal more, which I have not read: +- *[Mathematics in Lean]* +- *[The Mechanics of Proof]* +- *[The Hitchhiker's Guide to Logical Verification]* +- *[Metaprogramming in Lean]* + +Finally, there is [the Lean manual][Lean Manual]. It is *very* much a work in progress and contains plenty of blank pages. But, I've found some sections helpful on occasion. + +[Main Docs]: https://leanprover-community.github.io/mathlib4_docs/ +[Lean Zulip]: https://leanprover.zulipchat.com/ +[Theorem Proving in Lean]: https://leanprover.github.io/theorem_proving_in_lean4/introduction.html +[Functional Programming in Lean]: https://leanprover.github.io/functional_programming_in_lean/introduction.html +[Mathematics in Lean]: https://leanprover-community.github.io/mathematics_in_lean/ +[The Mechanics of Proof]: https://hrmacbeth.github.io/math2001/ +[The Hitchhiker's Guide to Logical Verification]: https://browncs1951x.github.io/static/files/hitchhikersguide.pdf +[Metaprogramming in Lean]: https://leanprover-community.github.io/lean4-metaprogramming-book/ +[Lean Manual]: https://lean-lang.org/lean4/doc/ ## Prelude @@ -68,7 +81,6 @@ However. To my best understanding, the syntactic forms are as follows: - assignment: `:=` - `def` `abbrev` - `let` `let rec` `let mut` - - `macro` `macro_rules` `notation` `syntax` - control flow: `if`/`then`/`else` `match`/`with` - iteration: - `for`/`in`/`do` `while`/`do` `repeat` @@ -81,6 +93,9 @@ However. To my best understanding, the syntactic forms are as follows: - `hiding` `renaming` `exposing` - `export` `private` `protected` ... - modifiers: `@[...]` `partial` `noncomputable` `nonrec` +- macros: + - `macro` `macro_rules` `notation` `syntax` + - `infix` `infixl` `infixr` `postfix` `prefix` - debugging: `assert!` `dbg_trace` - proof: - `axiom` `theorem` `lemma` @@ -101,7 +116,7 @@ The standard data types included in core Lean are the following: - unit: [`Unit`] - booleans: [`Bool`] - numbers: [`Nat`] [`Int`] [`Fin n`] - - [`USize`] [`UInt8`] [`UInt16`] [`UInt32`] [`UInt64`] [`BitVec`] + - [`USize`] [`UInt8`] [`UInt16`] [`UInt32`] [`UInt64`] [`BitVec w`] - strings: [`Char`] [`String`] [`Substring`] - lists: [`List α`] [`Array α`] [`Subarray`] - [`ByteArray`] [`FloatArray`] @@ -125,7 +140,7 @@ The standard data types included in core Lean are the following: [`UInt16`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt16 [`UInt32`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt32 [`UInt64`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt64 -[`BitVec`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/BitVec/Basic.html +[`BitVec w`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/BitVec/Basic.html [`Char`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Char [`String`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#String [`Substring`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Substring @@ -163,17 +178,243 @@ The best way to find out what you're looking at is to use VS Code's right-click ### Structural Types +The `structure` type is analogous to structs in other languages. It behaves much as one would expect. + +```lean +structure Header where + (width height : Nat) + alpha : Bool + linear := false + +let header : Header := { + width := 1920 + height := 1080 + alpha := true +} + +def increment_height (header : Header) : Header := + let {width, height, alpha, linear} := header + let height := height + 1 + {width, height, alpha, linear} +``` + +Structures may be declared with the `structure ... where` syntax. Just like functions, multiple fields of the same type may be grouped together, and default values are supported. An individual field with a default value may be omitted in the constructor. A field of a function may or may not be wrapped in parentheses, but parentheses are required for multiple fields of the same type. + +Structures may be constructed with braces. The braces are syntactic sugar for an underlying `Name.mk` constructor. Their fields take the form `field := value`, separated either by newlines or by commas. If `value` is a variable of the same name as `field`, the `field :=` portion may be omitted. The brace constructors are *structural*: the order in which fields are declared does not matter, only their name does. + +Structures may be destructured either by pattern matching or with dot notation for field access. Pattern matching may be done via `match` or inline via `let` with the `{}` syntax. + +They cannot be mutated: Lean is functional and so there is no explicit syntax for updating a field. `header.width ← ...` does nothing, even if `header` is declared to be mutable. Instead, the entire `header` structure must be updated at once. This can be a pain on large structures, so Lean provides the `with` keyword for succiently (re-)constructing a structure with only a few fields changed. The `increment_height` function above can thus be compactly declared as the following: +```lean +def increment_height (header : Header) : Header := + { header with height := header.height + 1 } +``` + +Structures may *extend* one another. A structure inherits all the fields of the structures it extends (which must not conflict), and can declare new fields. Default values may be redefined but fields may not be. As a type may not be referenced before its declaration, cyclic extensions cannot be formed. +```lean +structure Point where + (x y : Int) + +structure Color where + (r g b a : UInt8) + +structure Pixel extends Point, Color + -- implicit fields: + -- (x y : Int) + -- (r g b a : UInt8) +``` + +Structures may also parametrize over terms or other types. todo + +Be warned - the `where` in a `structure` declaration is mandatory. Leaving off the `where` will result in a (valid!) structure with *zero* fields, that is instead *parametrized* over what were intended to be the fields. This can lead to strange type errors. + + +See also: [FPIL:Structures](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/structures.html), [FPIL:Structures and Inheritance](https://leanprover.github.io/functional_programming_in_lean/functor-applicative-monad/inheritance.html), [Manual:Structures](https://lean-lang.org/lean4/doc/struct.html) + +### Products + +Sometimes, it is convenient to not need to bother with naming structures or their fields. Whether inline within the definition of a more complex type, or as the return type of a helper function, it can be the case that having explicit names is more trouble than it is worth. + +Lean provides a type for *anonymous structures*, that behave in a very similar fashion to *tuples* in other languages. This is called `Prod` on analogy with `Sum` (which we will see later) and is defined as follows: +```lean +structure Prod (α : Type) (β : Type) where + fst : α + snd : β + +abbrev Image := (Header × Array Pixel) +let image : Image := (header, #[]) + +#check (image.fst : Header) +``` + +Lean also provides the compact `α × β` notation as syntactic sugar for `Prod α β`. With Lean's rules around function application, tuples of arbitrary arity can be written `α × β × γ × ...`, which is equivalent to `α × (β × (γ × ...))` (and `Prod α Prod β Prod γ ...`). + +While products can be constructed with `Prod.mk a b` or `{ fst := a, snd := b }`, there is also provides tuple-like notation for constructing them: `(a, b, ...)`. This is overloaded to function for products of arbitrary arity. Similar to tuples elsewhere, the `.fst` and `.snd` destructors have aliases to `.1` and `.2`, respectively - however, there do not exist aliases for the rest of the natural numbers. + +The name `Prod` comes from type theory (and category theory more broadly). Structures are a special case of what is more generally called a "product": a vast generalization of the idea of taking a "pair" of something. The design of the `Prod` type aligns significantly closer to the specific formal notion of a "product type" in type theory than `structure` does, making it additionally quite useful for mathematicians. + +See also: [FPIL:Polymorphism#Prod](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/polymorphism.html#prod) + ### Inductive Types +### Sums + +Similarly to [products](#products), it is sometimes convenient to not need to bother with naming inductives or their variants. + +The `Sum` type provides for this. It is defined as follows: +```lean +inductive Sum (α : Type) (β : Type) where + | inl (val : α) + | inr (val : β) +``` + +Lean provides the compact `α ⊕ β` notation as syntactic sugar for `Sum α β`. This generalizes to sums of arbitrary length: `α ⊕ β ⊕ γ ⊕ ...`. There is no syntactic sugar for `Sum.inl` and `Sum.inr`: sums must be explicitly constructed. There is also no syntactic sugar for destructuring: `match` must be used. + +See also: [FPIL/Polymorphism#Sum](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#sum) + ### Booleans +Lean provides a `Bool` type, defined as an inductive data type: +```lean +inductive Bool where + | false + | true +``` + +The `true` and `false` terms are exported in the Prelude and do not need to be prefixed with `Bool`. Standard `if`/`else` destructors are also provided. `else if` is special cased in the parser to behave nicely. + +`if` is also overloaded to function with `let` to provide a compact alternative to a `match` statement. +```lean +let a := Chunk.rgb 1 2 3 +if let {r, g, b} := a then + IO.println s!"red: {r}, green: {g}, blue: {b}" + ### Numbers +Lean provides a variety of representations of numbers. The main three are [`Nat`], [`Int`], and [`Fin n`]. + +`Nat` is an arbitrary-sized number type. It is defined as the following: +```lean +-- Zero is a natural number. +-- The successor of a natural number is a natural number. +inductive Nat where + | zero + | succ (n : Nat) +``` + +Lean recognizes numeric literals (`0`, `1`, `2`...) as numeric constructors, equivalent to their `Nat.succ (Nat.succ ...)` counterparts. Special compiler support allows for representing `Nats` in a reasonable / efficient fashion: numbers smaller than `2^63` are stored directly, while numbers larger than `2^63 - 1` use an arbitrary precision BigInt library. + +It should be noted that Lean treats operations on `Nat` that would produce a negative number **as producing zero**. For example, `#check 4 - 5` prints `4 - 5 : Nat`, and `#eval 4 - 5` prints `0`. + +[`Int`] is an extension of `Nat` to also represent negative numbers. It is similarly special-cased by the compiler. Lean recognizes (..., `-2`, `-1`) as equivalent to their `Int.negSucc n` counterparts, and will also implicitly cast (`0`, `1`, `2`...) to `Int` as required. +```lean +-- A natural number is an integer. +-- The negation of the *successor* of a natural number is an integer. +-- (the above is enforced by compiler magic) +inductive Int where + | ofNat (n : Nat) -- [0 : ∞) + | negSucc (n : Nat) -- (-∞ : -1] +``` + +[`Fin n`] is a natural number guaranteed to be *smaller* than `n`: i.e. `i ∈ ℕ : 0 ≤ i < n`. The underlying representation is `val : Nat` and a proof that the `val < n`. +```lean +-- If i : Fin n, then i.val : Nat is the described number. +-- It can also be written as i.1 or just i when the target type is known. +-- If i : Fin n, then i.isLt is a proof that i.val < n. +structure Fin (n : Nat) where + val : Nat + isLt : LT.lt val n +``` + +Lean supports the following fixed-width integers: [`UInt8`], [`UInt16`], [`UInt32`], [`UInt64`], [`USize`]. They behave as one would expect. `USize` takes the size of a pointer on its appropriate platforms. Lean also supports *arbitrary* fixed-width integers with [`BitVec w`]. They are treated internally as `Fin (2 ^ w)`, and gain all the special support for math that `Fin n` and subsequently `Nat` has. + +Lean is good at typechecking numbers. For example, the following code compiles: +```lean +abbrev UInt6 := BitVec 6 +structure Pixel where + (r g b a : UInt8) + +def hash (pixel : Pixel) : UInt6 := + -- Lean recognizes the resulting value cannot be larger than 2^6 - 1 or 6 bits, via % 64. + (pixel.r.val * 3 + pixel.g.val * 5 + pixel.b.val * 7 + pixel.a.val * 11) % 64 +``` + +The expected basic mathematical operations are defined on all numbers. Their semantics differ depending on the specific numeric type. +- arithmetic: `+`, `-`, `*`, `/`, `%`, `∣` +- comparison: `<`, `>`, `<=`/`≤`, `>=`/`≥` +- bitwise: `&&&`, `|||`, `^^^`, `~~~` +- shifts: `<<<` and `>>>` + +Numbers regularly need to be explicitly converted between different representations. This may be done via various `.toType` and `.ofType` methods. + ### Lists -## Errors +Lean provides for several representations of list-like data structures. + +[`List α`] is the standard representation. It is represented as a linked list, and defined as the following: +```lean +inductive List (α : Type u) where + | nil + | cons (head : α) (tail : List α) +``` + +`List.nil` or more commonly `[]` represents the empty list. `List.cons a l` or `a :: l` (for some `a : α`, `l : List α`) are used for list concatenation. `[a, b, c, ...]` syntax can also be used for construction of lists. Various functions and classes are defined for and on lists. + +[`Array α`] is isomorphic to `List α`. It is represented as a dynamic array. `Arrays` are significantly more performant than `Lists`: not only are they more efficient at everything except insertation and deletion, but so long as arrays are used "linearly", all updates will be *destructive* - which provides comparable performance to mutable arrays in imperative programming languages. + +You usually want to use `Array`. However: currently `Arrays` are represented as an array of *pointers* in memory, for ABI reasons. This is an obvious performance pitfall and liable to change in the (near) future. But for now, Lean provides special [`ByteArray`] / [`FloatArray`] types that are treated like `Array UInt8` and `Array Float` respectively, but represented as real unboxed byte/float arrays. + +`Array` has a different syntax for its constructor: `#[a, b, c]`. It does overload `a :: l`. + +The [`Batteries.Vector α n`] type is not in `Std`, but worth a mention. It is a *statically sized array*: represented under the hood by `Array`, but guaranteed to not change size throughout its existence. + +All lists provide postfix `foo[i]` syntax for accessing arbitrary array elements. There are three variations: +- `foo[i]` takes an `i : Fin n`, where `n < foo.size`. If this cannot be proven it fails to compile. +- `foo[i]?` returns an `Option α`. +- `foo[i]!` returns an `α` or panics. + +See also: [FPIL:Polymorphism#Linked Lists](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#linked-lists), [Manual:Arrays](https://lean-lang.org/lean4/doc/array.html) + +### Strings + +The [`String`] type represents a UTF-8 encoded string. It is treated as a `List Char`, but represented as a packed `ByteArray`. Strings are constructed via `""`. + +The [`Char`] type represents a "Unicode scalar value": that is, a codepoint. The underlying value is represented (presumably) in UTF-32 as a `UInt32`. Chars are constructed via `''`. + +String manipulation can be inefficient. The [`Substring`] type provides an immutable *view* into some subslice of a `String`. + +## Classes + +### Coersion -## Iteration + +## Monads + +The [Functional Programming in Lean] book contains extensive information on monads in Lean: [FPIL:Monads](https://leanprover.github.io/functional_programming_in_lean/monads.html), [FPIL:Functors, Applicative Functors, and Monads](https://leanprover.github.io/functional_programming_in_lean/functor-applicative-monad.html), [FPIL:Monad Transformers](https://leanprover.github.io/functional_programming_in_lean/monad-transformers.html). + +Those interested in theory and the intricate details may look there. I intend to present a purely-workable overview of the language features implemented *atop* monads. + +### IO + +### Errors + +Lean encodes errors as monads. The [`Option α`] type is by far the most used. + +An `Option α` is the following type: +```lean +inductive Option (α : Type) where + | none + | some (val : α) +``` + +There are other forms of errors. The [`Except ε α`] type allows for encoding a specific error type: +```lean +inductive Except (ε : Type) (α : Type) where + | error (err : ε) + | ok (val : α) +``` + +### Iteration Lean has three main syntactic constructs for iteration: `for`, `while`, and `repeat`. They all function pretty much as you would expect and ultimately desugar to lambdas and (tail) recursion. @@ -195,12 +436,16 @@ Lean also has an external iteration typeclass, called `Stream`, but it is not us It is perhaps possible to do external iteration via the State monad. I would like to try this out. -## IO - -## Monads - ## Modules ## Macros +The standard reference is [Metaprogramming in Lean](https://leanprover-community.github.io/lean4-metaprogramming-book/). + +I will make no attempt to describe Lean's system in detail: but I do plan to provide a high-level overview. + ## Proof + +A text for type theorists is [Theorem Proving in Lean]. +A text for mathematicians is [Mathematics in Lean]. +A text for those new to mathematics is [The Mechanics of Proof]. |