meow

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].