From a39e490d1a3d08d96b1b7219f3824efe619a566a Mon Sep 17 00:00:00 2001 From: JJ Date: Sat, 31 Aug 2024 17:22:14 -0700 Subject: meow --- plt/lean.md | 142 ++++++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 99 insertions(+), 43 deletions(-) (limited to 'plt') diff --git a/plt/lean.md b/plt/lean.md index a7d0b86..a38e64d 100644 --- a/plt/lean.md +++ b/plt/lean.md @@ -13,12 +13,13 @@ I found it hard to get started with, however. This guide is an attempt at remedy - [Documentation](#documentation) - [Prelude](#prelude) -- Evaluation -- Assignment +- Basics +- [Assignment](#assignment) +- Functions - Data Types - - [Structural Types](#structural-types) + - [Structures](#structures) - [Products](#products) - - Inductive Types + - Inductives - [Sums](#sums) - [Booleans](#booleans) - [Numbers](#numbers) @@ -40,11 +41,12 @@ 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][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 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, and so these docs are as close as it gets. -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, indexable *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, indexable *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderful and very knowledgeable people: with channels for both 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, *[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]* @@ -70,6 +72,10 @@ Second: what is *in* the language, really? Is there a syntactic reference? The short answer is no, there is not a syntax reference, and if there existed one it wouldn't be very helpful. Lean has an extremely powerful metaprogramming system: and the majority of *syntax* in Lean is user-defined. However. To my best understanding, the syntactic forms are as follows: + +
+expand + - types: `:` - [`structure`] [`inductive`] `coinductive` [`class`] `instance` - `where` `instance` `extends` `deriving` @@ -110,9 +116,15 @@ However. To my best understanding, the syntactic forms are as follows: [`do`]: https://lean-lang.org/lean4/doc/do.html +
+ This list is unlikely to be comprehensive. The standard data types included in core Lean are the following: + +
+expand + - unit: [`Unit`] - booleans: [`Bool`] - numbers: [`Nat`] [`Int`] [`Fin n`] @@ -123,7 +135,7 @@ The standard data types included in core Lean are the following: - (see also: [`Batteries.Vector α n`]) - errors: [`Option α`] [`Except ε α`] - data: [`Prod α β`] [`Sum α β`] - - (see also: `structure` `inductive`) + - (see also: [`structure`] [`inductive`]) - types: [`Empty`] [`Nonempty`] [`Type`/`Prop`/`Type u`/`Sort u`] - proof: - [`And α β`] [`Or α β`] [`Iff α β`] [`True`] [`False`] @@ -166,17 +178,56 @@ The standard data types included in core Lean are the following: [`Equivalence`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Equivalence [`Exists`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Exists -The best way to find out what you're looking at is to use VS Code's right-click "Go to Declaration" feature. On a type, it'll drop you at its declaration. On a term, it'll drop you on its definition. On a *syntactic element*, it will either drop you into the core Lean codebase, or, more likely, onto a *macro syntax rule*. +
+ + +## Basics -(If you are not writing Lean in VS Code, by the way, you should be. Lean has *extremely* good tooling that is primarily based around VS Code. Emacs is the only other option but is much less maintained.) +Lean is a functional programming language. todo + +The best way to find out what you're looking at is to use VS Code's right-click "Go to Declaration" feature. On a type, it'll drop you at its declaration. On a term, it'll drop you on its definition. On a *syntactic element*, it will either drop you into the core Lean codebase, or, more likely, onto a *macro syntax rule*. -## Evaluation +(If you are not writing Lean in VS Code, you should be. Lean has *extremely* good tooling that is primarily based around VS Code. Emacs is the only other option but is much less maintained.) ## Assignment +There are several ways to declare variables and functions: +- `def` introduces a *named* definition. +- `let` defines a *local* binding. + - `let rec` declares a *local recursive* binding. + - `let mut` defines a *mutable* binding. +- `abbrev` defines a transparent alias. + +All of these may take parameters. + +```haskell +def hello := "Hello" +def world : String := + let world := "world" + let world := world.push '!' + world + +def inc (n : Nat) : Nat := n + 1 +def dec n := n - 1 + +abbrev Byte := UInt8 +``` + +The walrus operator `:=` is used for assignment, as `=` is used for *querying* equality. It follows the name of a `def`, `let`, or `abbrev` declaration. A type annotation can optionally precede `:=`. In most cases, they are not necessary - Lean has good type inference. The `←` operator is occasionally also used for assignment, in a similar fashion to `:=`. Its semantics are complex and covered in the section on monads. + +The primary distinction between `def` and `let` is that `let` allows *shadowing*: a future invocation of `let` may overwrite previous `let` bindings. `let` is thus useful for variables, while `def` is more useful for constants and functions that may be exported. `def` is additionally self-referential by default, though there are some asterisks, while `let` requires the use of `let rec`. The `let mut` declaration, it should be noted, is syntactic sugar over the State monad, which we will discuss later. + +The `abbrev` declaration creates a direct alias between the left and right hand sides of the declaration. Lean will gratuitously unfold these during overload resolution or when reducing or querying equality. + +All definitions may only be used after their declaration. A function thus cannot refer to a function declared after it, nor a structure to a not-yet declared structure. This prevents the declaration of mutually-entangled structures (and functions) and simplifies analysis. + +See also: [FPIL:Functions and Definitions](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/functions-and-definitions.html) + +## Functions + ## Data Types -### Structural Types +### Structures The `structure` type is analogous to structs in other languages. It behaves much as one would expect. @@ -191,17 +242,19 @@ let header : Header := { height := 1080 alpha := true } +``` + +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. +```haskell 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: @@ -219,16 +272,17 @@ structure Color where (r g b a : UInt8) structure Pixel extends Point, Color - -- implicit fields: - -- (x y : Int) - -- (r g b a : UInt8) + +let pixel : Pixel := { + x := 2000, y := 1000 + r := 255, g := 255, b := 255, a := 255 +} ``` 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 @@ -249,13 +303,13 @@ let image : Image := (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. +While products can be constructed with `Prod.mk a b` or `{ fst := a, snd := b }`, there is also 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 +### Inductives ### Sums @@ -290,9 +344,9 @@ if let {r, g, b} := a then ### Numbers -Lean provides a variety of representations of numbers. The main three are [`Nat`], [`Int`], and [`Fin n`]. +Lean provides a variety of representations of numbers. The main three are [`Nat`], [`Int`], & [`Fin`][`Fin n`]. -`Nat` is an arbitrary-sized number type. It is defined as the following: +[`Nat`] is an arbitrary-sized number type. It is defined as the following: ```haskell -- Zero is a natural number. -- The successor of a natural number is a natural number. @@ -301,7 +355,7 @@ inductive Nat where | 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. +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](https://gmplib.org/manual/). 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`. @@ -315,7 +369,7 @@ inductive Int where | 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`. +[`Fin n`] is a natural number guaranteed to be *smaller* than `n`. The underlying representation is `val : Nat` and a proof that `val < n`. ```haskell -- 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. @@ -344,13 +398,15 @@ The expected basic mathematical operations are defined on all numbers. Their sem - bitwise: `&&&`, `|||`, `^^^`, `~~~` - shifts: `<<<`, `>>>` -Numbers regularly need to be explicitly converted between different representations. This may be done via various `.toType` and `.ofType` methods. +Numbers regularly need to be explicitly converted between different representations. This may be done via various `.toType` and `.ofType` methods. More on conversion can be found in the Classes section. + +See also: [Manual:Naturals](https://lean-lang.org/lean4/doc/nat.html) ### Lists 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: +[`List α`] is the standard representation. It is represented as a linked list, and defined as follows: ```haskell inductive List (α : Type u) where | nil @@ -359,18 +415,18 @@ inductive List (α : Type u) where `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. As such, you usually want to use `Array`. +[`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", Lean will optimize all updates to be *destructive* - which provides comparable performance to mutable arrays in imperative programming languages. As such, **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. +However: currently `Arrays` are always represented as an array of *pointers* in memory, for ABI reasons. This is an obvious performance pitfall for small types 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`. +`Array` has different syntax for its constructor: `#[a, b, c]`. It also does not implement `List.cons a l` or `a :: l`. Instead, it uses `Array.push l a`, with elements added to the *end* of the array. -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. +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. It behaves much the same as `Array`, though without `push`. -All lists provide some postfix `foo[i]` syntax for accessing arbitrary array elements. -- `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. +All lists provide some postfix `list[i]` syntax for accessing arbitrary array elements. +- `list[i]` takes an `i : Fin n`, for `n < list.size`. If this cannot be proven it fails to compile. +- `list[i]?` returns an `Option α`. +- `list[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) @@ -378,7 +434,7 @@ See also: [FPIL:Polymorphism#Linked Lists](https://lean-lang.org/functional_prog 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 `''`. +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 `''`. They are ordered, and can be compared using `=`, `<`, `≤`, `>`, and `≥`. String manipulation can be inefficient. The [`Substring`] type provides an immutable *view* into some subslice of a `String`. @@ -417,11 +473,11 @@ inductive Except (ε : Type) (α : Type) where 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. -However: Lean is a purely functional language, as much as it does a good job at hiding it. In the default (pure) context, variable mutation is not allowed. Neither is IO, nor any sort of side effects. And `for`/`while`/`repeat` return only the Unit value, providing no information. +However: Lean is a purely functional language, as much as it does a good job at hiding it. In the default (pure) context, variable mutation is not allowed. Neither is IO, nor any sort of other side effects. And `for`/`while`/`repeat` may only return the Unit value. Iteration is thus *useless* in the pure context! We can iterate, for sure, but there may never be any *observable* changes. As such, Lean does not allow `for`/`while`/`repeat` within pure functions. This can be the cause of some strange type errors. Ensure you are only iterating in a monadic `do` context. -It should be noted that the `do` in `for/in/do` and `while/do` are part of their declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though. +(It should be noted that the `do` in `for/in/do` and `while/do` are part of their declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though.) #### implementing iterators: `ForIn` and `Stream` @@ -441,10 +497,10 @@ It is probably possible to do external iteration via the State monad. I would li 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. 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]. +The standard reference for type theorists is [Theorem Proving in Lean]. + +The standard reference for mathematicians is [Mathematics in Lean]. + +A guide for those new to mathematics entirely is [The Mechanics of Proof]. -- cgit v1.2.3-70-g09d2