From 5d58fa56d2b619d89854844b16c0fe6e449a3299 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 20 Oct 2025 14:17:33 +0200 Subject: [PATCH] chore: add tags to all sections that are probably permanent --- book/.verso/verso-xref-manifest.json | 3 +- .../DependentTypes/IndexedFamilies.lean | 7 ++ .../IndicesParametersUniverses.lean | 3 + book/FPLean/DependentTypes/Pitfalls.lean | 18 +++++ book/FPLean/DependentTypes/Summary.lean | 15 ++++ book/FPLean/DependentTypes/TypedQueries.lean | 59 +++++++++++++++ .../DependentTypes/UniversePattern.lean | 12 +++ .../FunctorApplicativeMonad/Alternative.lean | 12 +++ .../FunctorApplicativeMonad/Applicative.lean | 9 +++ .../ApplicativeContract.lean | 9 +++ .../FunctorApplicativeMonad/Complete.lean | 16 ++++ .../FunctorApplicativeMonad/Inheritance.lean | 12 +++ .../FunctorApplicativeMonad/Summary.lean | 15 ++++ .../FunctorApplicativeMonad/Universes.lean | 19 +++++ book/FPLean/GettingToKnow/Conveniences.lean | 33 +++++++- .../GettingToKnow/DatatypesPatterns.lean | 3 + book/FPLean/GettingToKnow/Evaluating.lean | 6 ++ .../GettingToKnow/FunctionsDefinitions.lean | 12 +++ book/FPLean/GettingToKnow/Polymorphism.lean | 30 ++++++++ book/FPLean/GettingToKnow/Structures.lean | 6 ++ book/FPLean/GettingToKnow/Summary.lean | 19 ++++- book/FPLean/GettingToKnow/Types.lean | 4 +- book/FPLean/HelloWorld/Cat.lean | 20 ++++- book/FPLean/HelloWorld/Conveniences.lean | 9 +++ book/FPLean/HelloWorld/RunningAProgram.lean | 15 +++- book/FPLean/HelloWorld/StartingAProject.lean | 13 ++++ book/FPLean/HelloWorld/StepByStep.lean | 19 +++++ book/FPLean/HelloWorld/Summary.lean | 15 ++++ book/FPLean/Intro.lean | 75 +++++++++++++++++-- .../MonadTransformers/Conveniences.lean | 12 +++ book/FPLean/MonadTransformers/Do.lean | 30 ++++++++ book/FPLean/MonadTransformers/Order.lean | 9 +++ book/FPLean/MonadTransformers/ReaderIO.lean | 18 +++++ book/FPLean/MonadTransformers/Summary.lean | 15 ++++ .../MonadTransformers/Transformers.lean | 39 ++++++++++ book/FPLean/Monads.lean | 19 +++++ book/FPLean/Monads/Arithmetic.lean | 28 ++++++- book/FPLean/Monads/Class.lean | 21 ++++++ book/FPLean/Monads/Conveniences.lean | 9 +++ book/FPLean/Monads/Do.lean | 6 ++ book/FPLean/Monads/IO.lean | 3 + book/FPLean/Monads/Summary.lean | 18 +++++ book/FPLean/NextSteps.lean | 15 ++++ .../ProgramsProofs/ArraysTermination.lean | 15 ++++ book/FPLean/ProgramsProofs/Fin.lean | 6 ++ book/FPLean/ProgramsProofs/Inequalities.lean | 26 +++++++ book/FPLean/ProgramsProofs/InsertionSort.lean | 28 ++++++- book/FPLean/ProgramsProofs/SpecialTypes.lean | 6 ++ book/FPLean/ProgramsProofs/Summary.lean | 21 ++++++ book/FPLean/ProgramsProofs/TailRecursion.lean | 12 +++ .../ProgramsProofs/TailRecursionProofs.lean | 28 +++++++ book/FPLean/PropsProofsIndexing.lean | 18 +++++ book/FPLean/TacticsInductionProofs.lean | 22 ++++++ book/FPLean/TypeClasses/Coercions.lean | 30 ++++++++ book/FPLean/TypeClasses/Conveniences.lean | 10 ++- book/FPLean/TypeClasses/Indexing.lean | 7 ++ book/FPLean/TypeClasses/OutParams.lean | 12 +++ book/FPLean/TypeClasses/Polymorphism.lean | 20 ++++- book/FPLean/TypeClasses/Pos.lean | 18 +++++ book/FPLean/TypeClasses/StandardClasses.lean | 27 +++++++ book/FPLean/TypeClasses/Summary.lean | 21 ++++++ book/lakefile.lean | 1 + 62 files changed, 1040 insertions(+), 18 deletions(-) diff --git a/book/.verso/verso-xref-manifest.json b/book/.verso/verso-xref-manifest.json index f6a54d9..d927854 100644 --- a/book/.verso/verso-xref-manifest.json +++ b/book/.verso/verso-xref-manifest.json @@ -1,8 +1,7 @@ {"version": 0, "sources": {"manual": - {"updated": "2025-10-16:12:58:47.024355000", - "updateFrequency": "manual", + {"updateFrequency": "manual", "shortName": "ref", "root": "https://lean-lang.org/doc/reference/4.23.0/", "longName": "Lean Language Reference"}}, diff --git a/book/FPLean/DependentTypes/IndexedFamilies.lean b/book/FPLean/DependentTypes/IndexedFamilies.lean index f7e3bdd..e3ea454 100644 --- a/book/FPLean/DependentTypes/IndexedFamilies.lean +++ b/book/FPLean/DependentTypes/IndexedFamilies.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.DependentTypes" #doc (Manual) "Indexed Families" => +%%% +tag := "indexed-families" +%%% Polymorphic inductive types take type arguments. For instance, {moduleName}`List` takes an argument that determines the type of the entries in the list, and {moduleName}`Except` takes arguments that determine the types of the exceptions or values. @@ -291,6 +294,10 @@ def Vect.zip : (n : Nat) → Vect α n → Vect β n → Vect (α × β) n ``` # Exercises +%%% +tag := "indexed-families-exercises" +%%% + Getting a feel for programming with dependent types requires experience, and the exercises in this section are very important. For each exercise, try to see which mistakes the type checker can catch, and which ones it can't, by experimenting with the code as you go. diff --git a/book/FPLean/DependentTypes/IndicesParametersUniverses.lean b/book/FPLean/DependentTypes/IndicesParametersUniverses.lean index c0152c0..2f53aa8 100644 --- a/book/FPLean/DependentTypes/IndicesParametersUniverses.lean +++ b/book/FPLean/DependentTypes/IndicesParametersUniverses.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.DependentTypes.IndicesParameters" #doc (Manual) "Indices, Parameters, and Universe Levels" => +%%% +tag := "indices-parameters-universe-levels" +%%% The distinction between indices and parameters of an inductive type is more than just a way to describe arguments to the type that either vary or do not between the constructors. Whether an argument to an inductive type is a parameter or an index also matters when it comes time to determine the relationships between their universe levels. diff --git a/book/FPLean/DependentTypes/Pitfalls.lean b/book/FPLean/DependentTypes/Pitfalls.lean index 4211c27..33a745a 100644 --- a/book/FPLean/DependentTypes/Pitfalls.lean +++ b/book/FPLean/DependentTypes/Pitfalls.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.DependentTypes.Pitfalls" #doc (Manual) "Pitfalls of Programming with Dependent Types" => +%%% +tag := "dependent-type-pitfalls" +%%% The flexibility of dependent types allows more useful programs to be accepted by a type checker, because the language of types is expressive enough to describe variations that less-expressive type systems cannot. At the same time, the ability of dependent types to express very fine-grained specifications allows more buggy programs to be rejected by a type checker. @@ -72,6 +75,9 @@ Behind the scenes, pattern matching on the first {anchorName appendL1}`Vect` imp Here, {lit}`n✝` represents the {anchorName moreNames}`Nat` that is one less than the argument {anchorName appendL1}`n`. # Definitional Equality +%%% +tag := "definitional-equality" +%%% In the definition of {anchorName appendL3}`plusL`, there is a pattern case {anchorTerm plusL}`0, k => k`. This applies in the length used in the first placeholder, so another way to write the underscore's type {anchorTerm moreNames}`Vect α (Nat.plusL 0 k)` is {anchorTerm moreNames}`Vect α k`. @@ -230,6 +236,9 @@ Exposing the internals of a function in a type means that refactoring the expose In particular, the fact that {anchorName appendL}`plusL` is used in the type of {anchorName appendL}`appendL` means that the definition of {anchorName appendL}`plusL` cannot be replaced by the otherwise-equivalent {anchorName plusR}`plusR`. # Getting Stuck on Addition +%%% +tag := "stuck-addition" +%%% What happens if append is defined with {anchorName appendR}`plusR` instead? Beginning in the same way, with explicit lengths and placeholder underscores in each case, reveals the following useful error messages: @@ -301,6 +310,9 @@ Getting it unstuck requires {ref "equality-and-ordering"}[propositional equality ::: # Propositional Equality +%%% +tag := "propositional-equality" +%%% Propositional equality is the mathematical statement that two expressions are equal. While definitional equality is a kind of ambient fact that Lean automatically checks when required, statements of propositional equality require explicit proofs. @@ -476,6 +488,9 @@ def appendR : Vect α n → Vect α k → Vect α (n.plusR k) ``` # Pros and Cons +%%% +tag := "dependent-types-pros-and-cons" +%%% Indexed families have an important property: pattern matching on them affects definitional equality. For example, in the {anchorName Vect}`nil` case in a {kw}`match` expression on a {anchorTerm Vect}`Vect`, the length simply _becomes_ {anchorTerm moreNames}`0`. @@ -509,6 +524,9 @@ Fluency in their use is an important part of knowing when to use them. # Exercises +%%% +tag := "dependent-type-pitfalls-exercises" +%%% * Using a recursive function in the style of {anchorName plusR_succ_left}`plusR_succ_left`, prove that for all {anchorName moreNames}`Nat`s {anchorName exercises}`n` and {anchorName exercises}`k`, {anchorTerm exercises}`n.plusR k = n + k`. * Write a function on {anchorName moreNames}`Vect` for which {anchorName plusR}`plusR` is more natural than {anchorName plusL}`plusL`, where {anchorName plusL}`plusL` would require proofs to be used in the definition. diff --git a/book/FPLean/DependentTypes/Summary.lean b/book/FPLean/DependentTypes/Summary.lean index b939668..6bcc9a1 100644 --- a/book/FPLean/DependentTypes/Summary.lean +++ b/book/FPLean/DependentTypes/Summary.lean @@ -10,8 +10,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.DependentTypes" #doc (Manual) "Summary" => +%%% +tag := "dependent-types-summary" +%%% # Dependent Types +%%% +tag := none +%%% Dependent types, where types contain non-type code such as function calls and ordinary data constructors, lead to a massive increase in the expressive power of a type system. The ability to _compute_ a type from the _value_ of an argument means that the return type of a function can vary based on which argument is provided. @@ -28,6 +34,9 @@ In these cases, pattern-matching gets “stuck” and does not proceed until or Type-level computation can be seen as a kind of partial evaluation, where only the parts of the program that are sufficiently known need to be evaluated and other parts are left alone. # The Universe Pattern +%%% +tag := none +%%% A common pattern when working with dependent types is to section off some subset of the type system. For example, a database query library might be able to return varying-length strings, fixed-length strings, or numbers in certain ranges, but it will never return a function, a user-defined datatype, or an {anchorName otherEx}`IO` action. @@ -43,6 +52,9 @@ Defining a custom universe has a number of advantages over using the types direc # Indexed Families +%%% +tag := none +%%% Datatypes can take two separate kinds of arguments: _parameters_ are identical in each constructor of the datatype, while _indices_ may vary between constructors. For a given choice of index, only some constructors of the datatype are available. @@ -65,6 +77,9 @@ Thirdly, running complicated code on large values during type checking can lead Avoiding these slowdowns for complicated programs can require specialized techniques. # Definitional and Propositional Equality +%%% +tag := none +%%% Lean's type checker must, from time to time, check whether two types should be considered interchangeable. Because types can contain arbitrary programs, it must therefore be able to check arbitrary programs for equality. diff --git a/book/FPLean/DependentTypes/TypedQueries.lean b/book/FPLean/DependentTypes/TypedQueries.lean index 6aaf132..8f21a27 100644 --- a/book/FPLean/DependentTypes/TypedQueries.lean +++ b/book/FPLean/DependentTypes/TypedQueries.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.DependentTypes.DB" #doc (Manual) "Worked Example: Typed Queries" => +%%% +tag := "typed-queries" +%%% Indexed families are very useful when building an API that is supposed to resemble some other language. They can be used to write a library of HTML constructors that don't permit generating invalid HTML, to encode the specific rules of a configuration file format, or to model complicated business constraints. @@ -20,6 +23,10 @@ It is not a realistic system, however—databases are represented as linked list However, it is large enough to demonstrate useful principles and techniques. # A Universe of Data +%%% +tag := "typed-query-data-universe" +%%% + In this relational algebra, the base data that can be held in columns can have types {anchorName DBType}`Int`, {anchorName DBType}`String`, and {anchorName DBType}`Bool` and are described by the universe {anchorName DBType}`DBType`: ```anchor DBType @@ -97,6 +104,9 @@ instance {t : DBType} : Repr t.asType where ``` # Schemas and Tables +%%% +tag := "schemas" +%%% A schema describes the name and type of each column in a database: @@ -163,6 +173,9 @@ def waterfallDiary : Table waterfall := [ ``` ## Recursion and Universes, Revisited +%%% +tag := "recursion-universes-revisited" +%%% The convenient structuring of rows as tuples comes at a cost: the fact that {anchorName Row}`Row` treats its two base cases separately means that functions that use {anchorName Row}`Row` in their types and are defined recursively over the codes (that, is the schema) need to make the same distinctions. One example of a case where this matters is an equality check that uses recursion over the schema to define a function that checks rows for equality. @@ -262,6 +275,9 @@ In the second role, the constructors are used like {anchorName Naturals}`Nat`s t Programming with indexed families often requires the ability to switch fluently between both perspectives. ## Subschemas +%%% +tag := "subschemas" +%%% One important operation in relational algebra is to _project_ a table or row into a smaller schema. Every column not present in the smaller schema is forgotten. @@ -416,6 +432,9 @@ def Subschema.reflexive : (s : Schema) → Subschema s s ## Projecting Rows +%%% +tag := "projecting-rows" +%%% Given evidence that {anchorName RowProj}`s'` is a subschema of {anchorName RowProj}`s`, a row in {anchorName RowProj}`s` can be projected into a row in {anchorName RowProj}`s'`. This is done using the evidence that {anchorName RowProj}`s'` is a subschema of {anchorName RowProj}`s`, which explains where each column of {anchorName RowProj}`s'` is found in {anchorName RowProj}`s`. @@ -433,6 +452,9 @@ def Row.project (row : Row s) : (s' : Schema) → Subschema s' s → Row s' # Conditions and Selection +%%% +tag := "conditions-and-selection" +%%% Projection removes unwanted columns from a table, but queries must also be able to remove unwanted rows. This operation is called _selection_. @@ -515,6 +537,9 @@ false ``` # Queries +%%% +tag := "typed-query-language" +%%% The query language is based on relational algebra. In addition to tables, it includes the following operators: @@ -572,11 +597,17 @@ def Schema.renameColumn : (s : Schema) → HasCol s n t → String → Schema ``` # Executing Queries +%%% +tag := "executing-queries" +%%% Executing queries requires a number of helper functions. The result of a query is a table; this means that each operation in the query language requires a corresponding implementation that works with tables. ## Cartesian Product +%%% +tag := "executing-cartesian-product" +%%% Taking the Cartesian product of two tables is done by appending each row from the first table to each row from the second. First off, due to the structure of {anchorName Row}`Row`, adding a single column to a row requires pattern matching on its schema in order to determine whether the result will be a bare value or a tuple. @@ -635,6 +666,9 @@ def Table.cartesianProduct (table1 : Table s1) (table2 : Table s2) : ## Difference +%%% +tag := "executing-difference" +%%% Removing undesired rows from a table can be done using {anchorName misc}`List.filter`, which takes a list and a function that returns a {anchorName misc}`Bool`. A new list is returned that contains only the entries for which the function returns {anchorName misc}`true`. @@ -656,6 +690,9 @@ def List.without [BEq α] (source banned : List α) : List α := This will be used with the {anchorName BEqDBType}`BEq` instance for {anchorName Row}`Row` when interpreting queries. ## Renaming Columns +%%% +tag := "executing-renaming-columns" +%%% Renaming a column in a row is done with a recursive function that traverses the row until the column in question is found, at which point the column with the new name gets the same value as the column with the old name: ```anchor renameRow @@ -672,6 +709,9 @@ One difficulty in programming with indexed families is that when performance mat It takes a very careful, often brittle, design to eliminate these kinds of “re-indexing” functions. ## Prefixing Column Names +%%% +tag := "executing-prefixing-column-names" +%%% Adding a prefix to column names is very similar to renaming a column. Instead of proceeding to a desired column and then returning, {anchorName prefixRow}`prefixRow` must process all columns: @@ -688,6 +728,9 @@ This can be used with {anchorName misc}`List.map` in order to add a prefix to al Once again, this function only exists to change the type of a value. ## Putting the Pieces Together +%%% +tag := "query-exec-runner" +%%% With all of these helpers defined, executing a query requires only a short recursive function: @@ -758,6 +801,10 @@ Because the example data includes only waterfalls in the USA, executing the quer ``` ## Errors You May Meet +%%% +tag := "typed-queries-error-messages" +%%% + Many potential errors are ruled out by the definition of {anchorName Query}`Query`. For instance, forgetting the added qualifier in {anchorTerm Query2}`"mountain.location"` yields a compile-time error that highlights the column reference {anchorTerm QueryOops1}`c! "location"`: @@ -804,12 +851,21 @@ Unfortunately, it is beyond the scope of this book to provide a description of i An indexed family such as {anchorName Query}`Query` is probably best as the core of a typed database interaction library, rather than its user interface. # Exercises +%%% +tag := "typed-query-exercises" +%%% ## Dates +%%% +tag := none +%%% Define a structure to represent dates. Add it to the {anchorName DBExpr}`DBType` universe and update the rest of the code accordingly. Provide the extra {anchorName DBExpr}`DBExpr` constructors that seem to be necessary. ## Nullable Types +%%% +tag := none +%%% Add support for nullable columns to the query language by representing database types with the following structure: ```anchor nullable @@ -827,6 +883,9 @@ abbrev NDBType.asType (t : NDBType) : Type := Use this type in place of {anchorName DBExpr}`DBType` in {anchorName Schema}`Column` and {anchorName DBExpr}`DBExpr`, and look up SQL's rules for {lit}`NULL` and comparison operators to determine the types of {anchorName DBExpr}`DBExpr`'s constructors. ## Experimenting with Tactics +%%% +tag := none +%%% What is the result of asking Lean to find values of the following types using {kw}`by repeat constructor`? Explain why each gives the result that it does. diff --git a/book/FPLean/DependentTypes/UniversePattern.lean b/book/FPLean/DependentTypes/UniversePattern.lean index 865c2df..d376020 100644 --- a/book/FPLean/DependentTypes/UniversePattern.lean +++ b/book/FPLean/DependentTypes/UniversePattern.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.DependentTypes.Finite" #doc (Manual) "The Universe Design Pattern" => +%%% +tag := "universe-pattern" +%%% In Lean, types such as {anchorTerm sundries}`Type`, {anchorTerm sundries}`Type 3`, and {anchorTerm sundries}`Prop` that classify other types are known as universes. However, the term _universe_ is also used for a design pattern in which a datatype is used to represent a subset of Lean's types, and a function converts the datatype's constructors into actual types. @@ -90,6 +93,9 @@ Hint: Additional diagnostic information may be available using the `set_option d The {anchorName beqNoCases}`t` in the error message stands for an unknown value of type {anchorName beqNoCases}`NestedPairs`. # Type Classes vs Universes +%%% +tag := "type-classes-vs-universe-pattern" +%%% Type classes allow an open-ended collection of types to be used with an API as long as they have implementations of the necessary interfaces. In most cases, this is preferable. @@ -104,6 +110,9 @@ This is useful in a few situations: Type classes are useful in many of the same situations as interfaces in Java or C#, while a universe à la Tarski can be useful in cases where a sealed class might be used, but where an ordinary inductive datatype is not usable. # A Universe of Finite Types +%%% +tag := "finite-type-universe" +%%% Restricting the types that can be used with an API to a predetermined collection can enable operations that would be impossible for an open-ended API. For example, functions can't normally be compared for equality. @@ -350,6 +359,9 @@ Nested exponentials grow quickly, and there are many higher-order functions. # Exercises +%%% +tag := "universe-exercises" +%%% * Write a function that converts any value from a type coded for by {anchorName Finite}`Finite` into a string. Functions should be represented as their tables. * Add the empty type {anchorName sundries}`Empty` to {anchorName Finite}`Finite` and {anchorName FiniteBeq}`Finite.beq`. diff --git a/book/FPLean/FunctorApplicativeMonad/Alternative.lean b/book/FPLean/FunctorApplicativeMonad/Alternative.lean index 786d29d..ffe290f 100644 --- a/book/FPLean/FunctorApplicativeMonad/Alternative.lean +++ b/book/FPLean/FunctorApplicativeMonad/Alternative.lean @@ -16,6 +16,9 @@ tag := "alternative" # Recovery from Failure +%%% +tag := "alternative-recovery" +%%% {anchorName Validate}`Validate` can also be used in situations where there is more than one way for input to be acceptable. For the input form {anchorName RawInput}`RawInput`, an alternative set of business rules that implement conventions from a legacy system might be the following: @@ -219,6 +222,9 @@ Validate.errors # The {lit}`Alternative` Class +%%% +tag := "Alternative" +%%% Many types support a notion of failure and recovery. The {anchorName AlternativeMany}`Many` monad from the section on {ref "nondeterministic-search"}[evaluating arithmetic expressions in a variety of monads] is one such type, as is {anchorName AlternativeOption}`Option`. @@ -292,8 +298,14 @@ Running it on {anchorTerm evenDivisors20}`20` yields the expected results: # Exercises +%%% +tag := "Alternative-exercises" +%%% ## Improve Validation Friendliness +%%% +tag := none +%%% The errors returned from {anchorName Validate}`Validate` programs that use {anchorTerm OrElseSugar}`<|>` can be difficult to read, because inclusion in the list of errors simply means that the error can be reached through _some_ code path. A more structured error report can be used to guide the user through the process more accurately: diff --git a/book/FPLean/FunctorApplicativeMonad/Applicative.lean b/book/FPLean/FunctorApplicativeMonad/Applicative.lean index 27fdbf7..6d240c8 100644 --- a/book/FPLean/FunctorApplicativeMonad/Applicative.lean +++ b/book/FPLean/FunctorApplicativeMonad/Applicative.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.FunctorApplicativeMonad" #doc (Manual) "Applicative Functors" => +%%% +tag := "applicative" +%%% An _applicative functor_ is a functor that has two additional operations available: {anchorName ApplicativeOption}`pure` and {anchorName ApplicativeOption}`seq`. {anchorName ApplicativeOption}`pure` is the same operator used in {anchorName ApplicativeLaws}`Monad`, because {anchorName ApplicativeLaws}`Monad` in fact inherits from {anchorName ApplicativeOption}`Applicative`. @@ -134,6 +137,9 @@ Because {anchorName Pairpure2 (show := pure)}`Pair.pure` would need to work for After all, a caller could choose {anchorName Pairpure2}`α` to be {anchorName ApplicativePair}`Empty`, which has no values at all. # A Non-Monadic Applicative +%%% +tag := "validate" +%%% When validating user input to a form, it's generally considered to be best to provide many errors at once, rather than one error at a time. This allows the user to have an overview of what is needed to please the computer, rather than feeling badgered as they correct the errors field by field. @@ -152,6 +158,9 @@ Like the {anchorName ApplicativeExcept}`Except` monad, {anchorName Validate}`Val Unlike {anchorName ApplicativeExcept}`Except`, it allows multiple errors to be accumulated, without a risk of forgetting to check whether the list is empty. ## User Input +%%% +tag := "user-input" +%%% As an example of user input, take the following structure: ```anchor RawInput diff --git a/book/FPLean/FunctorApplicativeMonad/ApplicativeContract.lean b/book/FPLean/FunctorApplicativeMonad/ApplicativeContract.lean index 1d67230..b1806d9 100644 --- a/book/FPLean/FunctorApplicativeMonad/ApplicativeContract.lean +++ b/book/FPLean/FunctorApplicativeMonad/ApplicativeContract.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.FunctorApplicativeMonad" #doc (Manual) "The Applicative Contract" => +%%% +tag := "applicative-laws" +%%% Just like {anchorName ApplicativeLaws}`Functor`, {anchorName ApplicativeLaws}`Monad`, and types that implement {anchorName SizedCreature}`BEq` and {anchorName MonstrousAssistantMore}`Hashable`, {anchorName ApplicativeLaws}`Applicative` has a set of rules that all instances should adhere to. @@ -61,6 +64,9 @@ In the fourth case, assume that {anchorName ApplicativeLaws}`u` is {anchorTerm O # All Applicatives are Functors +%%% +tag := "applicatives-are-functors" +%%% The two operators for {anchorName ApplicativeMap}`Applicative` are enough to define {anchorName ApplicativeMap}`map`: @@ -86,6 +92,9 @@ class Applicative (f : Type → Type) extends Functor f where ``` # All Monads are Applicative Functors +%%% +tag :="monads-are-applicative" +%%% An instance of {anchorName MonadExtends}`Monad` already requires an implementation of {anchorName MonadSeq}`pure`. Together with {anchorName MonadExtends}`bind`, this is enough to define {anchorName MonadSeq}`seq`: diff --git a/book/FPLean/FunctorApplicativeMonad/Complete.lean b/book/FPLean/FunctorApplicativeMonad/Complete.lean index 6756964..23f98e3 100644 --- a/book/FPLean/FunctorApplicativeMonad/Complete.lean +++ b/book/FPLean/FunctorApplicativeMonad/Complete.lean @@ -10,11 +10,18 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.FunctorApplicativeMonad.ActualDefs" #doc (Manual) "The Complete Definitions" => +%%% +tag := "complete-definitions" +%%% Now that all the relevant language features have been presented, this section describes the complete, honest definitions of {anchorName HonestFunctor}`Functor`, {anchorName Applicative}`Applicative`, and {anchorName Monad}`Monad` as they occur in the Lean standard library. For the sake of understanding, no details are omitted. # Functor +%%% +tag := "complete-functor-definition" +%%% + The complete definition of the {anchorName Applicative}`Functor` class makes use of universe polymorphism and a default method implementation: @@ -66,6 +73,9 @@ Similarly, other arguments to the function have a type built by applying {anchor All the type classes in this section share this property. # Applicative +%%% +tag := "complete-applicative-definition" +%%% The {anchorName Applicative}`Applicative` type class is actually built from a number of smaller classes that each contain some of the relevant methods. The first are {anchorName Applicative}`Pure` and {anchorName Applicative}`Seq`, which contain {anchorName Applicative}`pure` and {anchorName Seq}`seq` respectively: @@ -153,6 +163,9 @@ In other words, {anchorTerm unfoldMapConstSeqRight}`(fun _ x => x) <$> a` preser From the perspective of effects, the side effects of {anchorName unfoldMapConstSeqRight}`a` occur, but the values are thrown out when it is used with {anchorName Seq}`seq`. # Monad +%%% +tag := "complete-monad-definition" +%%% Just as the constituent operations of {anchorName Applicative}`Applicative` are split into their own type classes, {anchorName Bind}`Bind` has its own class as well: @@ -176,6 +189,9 @@ From the perspective of API boundaries, any type with a {anchorName Monad}`Monad # Exercises +%%% +tag := "complete-functor-applicative-monad-exercises" +%%% 1. Understand the default implementations of {anchorName HonestFunctor}`map`, {anchorName Seq}`seq`, {anchorName SeqLeft}`seqLeft`, and {anchorName SeqRight}`seqRight` in {anchorName Monad}`Monad` by working through examples such as {anchorName mapConstOption}`Option` and {anchorName ApplicativeExcept (module:=Examples.FunctorApplicativeMonad)}`Except`. In other words, substitute their definitions for {anchorName Bind}`bind` and {anchorName Pure}`pure` into the default definitions, and simplify them to recover the versions {anchorName HonestFunctor}`map`, {anchorName Seq}`seq`, {anchorName SeqLeft}`seqLeft`, and {anchorName SeqRight}`seqRight` that would be written by hand. 2. On paper or in a text file, prove to yourself that the default implementations of {anchorName HonestFunctor}`map` and {anchorName Seq}`seq` satisfy the contracts for {anchorName Applicative}`Functor` and {anchorName Applicative}`Applicative`. In this argument, you're allowed to use the rules from the {anchorName Monad}`Monad` contract as well as ordinary expression evaluation. diff --git a/book/FPLean/FunctorApplicativeMonad/Inheritance.lean b/book/FPLean/FunctorApplicativeMonad/Inheritance.lean index 89327e6..9940f57 100644 --- a/book/FPLean/FunctorApplicativeMonad/Inheritance.lean +++ b/book/FPLean/FunctorApplicativeMonad/Inheritance.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.FunctorApplicativeMonad" #doc (Manual) "Structures and Inheritance" => +%%% +tag := "structure-inheritance" +%%% In order to understand the full definitions of {anchorName ApplicativeLaws}`Functor`, {anchorName ApplicativeLaws}`Applicative`, and {anchorName ApplicativeLaws}`Monad`, another Lean feature is necessary: structure inheritance. Structure inheritance allows one structure type to provide the interface of another, along with additional fields. @@ -140,6 +143,9 @@ in the application ``` # Multiple Inheritance +%%% +tag := "multiple-structure-inheritance" +%%% A helper is a mythical creature that can provide assistance when given the correct payment: @@ -202,6 +208,9 @@ This function constructs a {anchorName Helper}`Helper` from the fields of {ancho The {lit}`@[reducible]` attribute has the same effect as writing {kw}`abbrev`. ## Default Declarations +%%% +tag := "inheritance-defaults" +%%% When one structure inherits from another, default field definitions can be used to instantiate the parent structure's fields based on the child structure's fields. If more size specificity is required than whether a creature is large or not, a dedicated datatype describing sizes can be used together with inheritance, yielding a structure in which the {anchorName MythicalCreature}`large` field is computed from the contents of the {anchorName SizedCreature}`size` field: @@ -253,6 +262,9 @@ example : SizesMatch huldre := by ## Type Class Inheritance +%%% +tag := "type-class-inheritance" +%%% Behind the scenes, type classes are structures. Defining a new type class defines a new structure, and defining an instance creates a value of that structure type. diff --git a/book/FPLean/FunctorApplicativeMonad/Summary.lean b/book/FPLean/FunctorApplicativeMonad/Summary.lean index c5d519f..0f50969 100644 --- a/book/FPLean/FunctorApplicativeMonad/Summary.lean +++ b/book/FPLean/FunctorApplicativeMonad/Summary.lean @@ -10,8 +10,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.FunctorApplicativeMonad.ActualDefs" #doc (Manual) "Summary" => +%%% +tag := "structure-applicative-monad-summary" +%%% # Type Classes and Structures +%%% +tag := none +%%% Behind the scenes, type classes are represented by structures. Defining a class defines a structure, and additionally creates an empty table of instances. @@ -20,6 +26,9 @@ Instance search consists of constructing an instance by consulting the instance Both structures and classes may provide default values for fields (which are default implementations of methods). # Structures and Inheritance +%%% +tag := none +%%% Structures may inherit from other structures. Behind the scenes, a structure that inherits from another structure contains an instance of the original structure as a field. @@ -31,6 +40,9 @@ Because type classes are just structures with some additional automation applied Together with default methods, this can be used to create a fine-grained hierarchy of interfaces that nonetheless does not impose a large burden on clients, because the small classes that the large classes inherit from can be automatically implemented. # Applicative Functors +%%% +tag := none +%%% An applicative functor is a functor with two additional operations: * {anchorName Applicative}`pure`, which is the same operator as that for {anchorName Monad}`Monad` @@ -51,6 +63,9 @@ Programs that are written against these interfaces expect that the additional ru The default implementations of {anchorName HonestFunctor}`Functor`'s methods in terms of {anchorName Applicative}`Applicative`'s, and of {anchorName Applicative}`Applicative`'s in terms of {anchorName Monad}`Monad`'s, will obey these rules. # Universes +%%% +tag := none +%%% To allow Lean to be used as both a programming language and a theorem prover, some restrictions on the language are necessary. This includes restrictions on recursive functions that ensure that they all either terminate or are marked as {kw}`partial` and written to return types that are not uninhabited. diff --git a/book/FPLean/FunctorApplicativeMonad/Universes.lean b/book/FPLean/FunctorApplicativeMonad/Universes.lean index 5d994e4..0ba803f 100644 --- a/book/FPLean/FunctorApplicativeMonad/Universes.lean +++ b/book/FPLean/FunctorApplicativeMonad/Universes.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Universes" #doc (Manual) "Universes" => +%%% +tag := "universe-levels" +%%% In the interests of simplicity, this book has thus far papered over an important feature of Lean: _universes_. A universe is a type that classifies other types. @@ -71,6 +74,9 @@ Even though {anchorTerm SomeTypes}`Nat` is in {anchorTerm SomeTypes}`Type`, this Similarly, even though {anchorTerm SomeTypes}`Type` is in {anchorTerm SomeTypes}`Type 1`, the function type {anchorTerm FunTypePropType}`Type → 2 + 2 = 4` is still in {anchorTerm FunTypePropType}`Prop`. # User Defined Types +%%% +tag := "inductive-type-universes" +%%% Structures and inductive datatypes can be declared to inhabit particular universes. Lean then checks whether each datatype avoids paradoxes by being in a universe that's large enough to prevent it from containing its own type. @@ -120,6 +126,9 @@ Generally speaking, it's easiest to start with the datatype in the same universe Then, if Lean rejects the definition, increase its level by one, which will usually go through. # Universe Polymorphism +%%% +tag := "universe-polymorphism" +%%% Defining a datatype in a specific universe can lead to code duplication. Placing {anchorName MyList1}`MyList` in {anchorTerm MyList1Type}`Type → Type` means that it can't be used for an actual list of types. @@ -225,6 +234,9 @@ In positions where Lean expects a universe level, any of the following are allow * A level increase, written with {anchorTerm someTrueProps}`+ 1` ## Writing Universe-Polymorphic Definitions +%%% +tag := none +%%% Until now, every datatype defined in this book has been in {anchorTerm SomeTypes}`Type`, the smallest universe of data. When presenting polymorphic datatypes from the Lean standard library, such as {anchorName SomeTypes}`List` and {anchorName SumMax}`Sum`, this book created non-universe-polymorphic versions of them. @@ -238,6 +250,10 @@ Finally, it's a good idea to put the new type in as small of a universe as possi Non-polymorphic types, such as {anchorTerm SomeTypes}`Nat` and {anchorName SomeTypes}`String`, can be placed directly in {anchorTerm Type0Type}`Type 0`. ## {anchorTerm PropType}`Prop` and Polymorphism +%%% +tag := none +%%% + Just as {anchorTerm SomeTypes}`Type`, {anchorTerm SomeTypes}`Type 1`, and so on describe types that classify programs and data, {anchorTerm PropType}`Prop` classifies logical propositions. A type in {anchorTerm PropType}`Prop` describes what counts as convincing evidence for the truth of a statement. @@ -273,6 +289,9 @@ The universe level {lit}`imax u v` is {lit}`0` when {anchorTerm sorts}`v` is {li Together with {anchorTerm sorts}`Sort`, this allows the special rule for functions that return {anchorTerm PropType}`Prop`s to be used when writing code that should be as portable as possible between {anchorTerm PropType}`Prop` and {anchorTerm SomeTypes}`Type` universes. # Polymorphism in Practice +%%% +tag := none +%%% In the remainder of the book, definitions of polymorphic datatypes, structures, and classes will use universe polymorphism in order to be consistent with the Lean standard library. This will enable the complete presentation of the {moduleName}`Functor`, {anchorName next}`Applicative`, and {anchorName next}`Monad` classes to be completely consistent with their actual definitions. diff --git a/book/FPLean/GettingToKnow/Conveniences.lean b/book/FPLean/GettingToKnow/Conveniences.lean index 2fb64b4..fb252e0 100644 --- a/book/FPLean/GettingToKnow/Conveniences.lean +++ b/book/FPLean/GettingToKnow/Conveniences.lean @@ -11,10 +11,16 @@ set_option verso.exampleModule "Examples.Intro" #doc (Manual) "Additional Conveniences" => +%%% +tag := "getting-to-know-conveniences" +%%% Lean contains a number of convenience features that make programs much more concise. # Automatic Implicit Parameters +%%% +tag := "automatic-implicit-parameters" +%%% :::paragraph When writing polymorphic functions in Lean, it is typically not necessary to list all the implicit parameters. @@ -43,6 +49,9 @@ This can greatly simplify highly polymorphic definitions that take many implicit ::: # Pattern-Matching Definitions +%%% +tag := "pattern-matching-definitions" +%%% When defining functions with {kw}`def`, it is quite common to name an argument and then immediately use it with pattern matching. For instance, in {anchorName lengthImpAuto}`length`, the argument {anchorName lengthImpAuto}`xs` is used only in {kw}`match`. @@ -107,6 +116,9 @@ This function is called {anchorTerm fragments}`Option.getD` in the standard libr ::: # Local Definitions +%%% +tag := "local-definitions" +%%% It is often useful to name intermediate steps in a computation. In many cases, intermediate values represent useful concepts all on their own, and naming them explicitly can make the program easier to read. @@ -182,6 +194,9 @@ When it reaches the end of the input list, {anchorName reverse}`soFar` contains ::: # Type Inference +%%% +tag := "type-inference" +%%% :::paragraph In many situations, Lean can automatically determine an expression's type. @@ -380,6 +395,9 @@ def sameLength (xs : List α) (ys : List β) : Bool := ::: # Natural Number Patterns +%%% +tag := "natural-number-patterns" +%%% :::paragraph @@ -448,6 +466,9 @@ This restriction enables Lean to transform all uses of the {anchorTerm halveFlip ::: # Anonymous Functions +%%% +tag := "anonymous-functions" +%%% :::paragraph @@ -563,7 +584,9 @@ while {anchor applyCdot}`#eval (· * 2) 5` results in: ::: # Namespaces - +%%% +tag := "namespaces" +%%% Each name in Lean occurs in a _namespace_, which is a collection of names. Names are placed in namespaces using {lit}`.`, so {anchorName fragments}`List.map` is the name {anchorName fragments}`map` in the {lit}`List` namespace. @@ -657,7 +680,10 @@ To do this, simply omit the {kw}`in` from a top-level usage of {kw}`open`. ::: -# if let +# {lit}`if let` +%%% +tag := "if-let" +%%% :::paragraph When consuming values that have a sum type, it is often the case that only a single constructor is of interest. @@ -699,6 +725,9 @@ In some contexts, using {kw}`if let` instead of {kw}`match` can make code easier ::: # Positional Structure Arguments +%%% +tag := "positional-structure-arguments" +%%% The {ref "structures"}[section on structures] presents two ways of constructing structures: 1. The constructor can be called directly, as in {anchorTerm pointCtor}`Point.mk 1 2`. diff --git a/book/FPLean/GettingToKnow/DatatypesPatterns.lean b/book/FPLean/GettingToKnow/DatatypesPatterns.lean index 007a812..8ece6c1 100644 --- a/book/FPLean/GettingToKnow/DatatypesPatterns.lean +++ b/book/FPLean/GettingToKnow/DatatypesPatterns.lean @@ -114,6 +114,9 @@ Just like C# and Java, this encoding ends up with more types than in Lean, becau It also illustrates that Lean constructors correspond to objects in JavaScript or TypeScript that include a tag that identifies the contents. # Pattern Matching +%%% +tag := "pattern-matching" +%%% In many languages, these kinds of data are consumed by first using an instance-of operator to check which subclass has been received and then reading the values of the fields that are available in the given subclass. The instance-of check determines which code to run, ensuring that the data needed by this code is available, while the fields themselves provide the data. diff --git a/book/FPLean/GettingToKnow/Evaluating.lean b/book/FPLean/GettingToKnow/Evaluating.lean index 0a2c96d..169df31 100644 --- a/book/FPLean/GettingToKnow/Evaluating.lean +++ b/book/FPLean/GettingToKnow/Evaluating.lean @@ -143,6 +143,9 @@ String.append "it is " "no" # Messages You May Meet +%%% +tag := "evaluating-messages" +%%% :::paragraph Asking Lean to evaluate a function application that is missing an argument will lead to an error message. @@ -166,6 +169,9 @@ Lean cannot display functions to users, and thus returns an error when asked to # Exercises +%%% +tag := "evaluating-exercises" +%%% What are the values of the following expressions? Work them out by hand, then enter them into Lean to check your work. diff --git a/book/FPLean/GettingToKnow/FunctionsDefinitions.lean b/book/FPLean/GettingToKnow/FunctionsDefinitions.lean index 7523b63..0d12aea 100644 --- a/book/FPLean/GettingToKnow/FunctionsDefinitions.lean +++ b/book/FPLean/GettingToKnow/FunctionsDefinitions.lean @@ -11,6 +11,9 @@ set_option verso.exampleModule "Examples.Intro" #doc (Manual) "Functions and Definitions" => +%%% +tag := "functions-and-definitions" +%%% :::paragraph In Lean, definitions are introduced using the {kw}`def` keyword. @@ -57,6 +60,9 @@ In Lean, functions are defined using the same {kw}`def` keyword as other values. Nonetheless, definitions such as {anchorTerm helloNameVal}`hello` introduce names that refer _directly_ to their values, rather than to zero-argument functions that return equivalent results each time they are called. # Defining Functions +%%% +tag := "defining-functions" +%%% :::paragraph There are a variety of ways to define functions in Lean. The simplest is to place the function's arguments before the definition's type, separated by spaces. For instance, a function that adds one to its argument can be written: @@ -124,12 +130,18 @@ Using a function that returns a function to implement multiple-argument function Function arrows associate to the right, which means that {anchorTerm currying}`Nat → Nat → Nat` should be parenthesized {anchorTerm currying}`Nat → (Nat → Nat)`. ## Exercises +%%% +tag := "function-definition-exercises" +%%% * Define the function {anchorName joinStringsWithEx}`joinStringsWith` with type {anchorTerm joinStringsWith}`String → String → String → String` that creates a new string by placing its first argument between its second and third arguments. {anchorEvalStep joinStringsWithEx 0}`joinStringsWith ", " "one" "and another"` should evaluate to {anchorEvalStep joinStringsWithEx 1}`"one, and another"`. * What is the type of {anchorTerm joinStringsWith}`joinStringsWith ": "`? Check your answer with Lean. * Define a function {anchorName volume}`volume` with type {anchorTerm volume}`Nat → Nat → Nat → Nat` that computes the volume of a rectangular prism with the given height, width, and depth. # Defining Types +%%% +tag := "defining-types" +%%% Most typed programming languages have some means of defining aliases for types, such as C's {c}`typedef`. In Lean, however, types are a first-class part of the language—they are expressions like any other. diff --git a/book/FPLean/GettingToKnow/Polymorphism.lean b/book/FPLean/GettingToKnow/Polymorphism.lean index 493df71..800d7e6 100644 --- a/book/FPLean/GettingToKnow/Polymorphism.lean +++ b/book/FPLean/GettingToKnow/Polymorphism.lean @@ -180,6 +180,9 @@ Evaluation can occur both in the expression and its type: ::: # Linked Lists +%%% +tag := "linked-lists" +%%% :::paragraph Lean's standard library includes a canonical linked list datatype, called {anchorName fragments}`List`, and special syntax that makes it more convenient to use. @@ -276,6 +279,9 @@ def length (α : Type) (xs : List α) : Nat := ::: # Implicit Arguments +%%% +tag := "implicit-parameters" +%%% :::paragraph Both {anchorName replaceX}`replaceX` and {anchorName length1}`length` are somewhat bureaucratic to use, because the type argument is typically uniquely determined by the later values. @@ -353,10 +359,16 @@ List.length : List Int → Nat ::: # More Built-In Datatypes +%%% +tag := "more-built-in-types" +%%% In addition to lists, Lean's standard library contains a number of other structures and inductive datatypes that can be used in a variety of contexts. ## {lit}`Option` +%%% +tag := "Option" +%%% Not every list has a first entry—some lists are empty. Many operations on collections may fail to find what they are looking for. For instance, a function that finds the first entry in a list may not find any such entry. @@ -537,6 +549,9 @@ In other words, all products of more than two types, and their corresponding con ## {anchorName Sum}`Sum` +%%% +tag := "Sum" +%%% The {anchorName Sum}`Sum` datatype is a generic way of allowing a choice between values of two different types. For instance, a {anchorTerm fragments}`Sum String Int` is either a {anchorName fragments}`String` or an {anchorName fragments}`Int`. @@ -594,6 +609,9 @@ As expected, {anchor dogCount}`#eval howManyDogs animals` yields {anchorInfo dog ::: ## {anchorName Unit}`Unit` +%%% +tag := "Unit" +%%% :::paragraph {anchorName Unit}`Unit` is a type with just one argumentless constructor, called {anchorName Unit}`unit`. @@ -633,6 +651,9 @@ By being an intentionally uninteresting value, {anchorName ArithExprEx}`Unit` al Unit's constructor can be written as empty parentheses: {anchorTerm unitParens}`() : Unit`. ## {lit}`Empty` +%%% +tag := "Empty" +%%% The {anchorName fragments}`Empty` datatype has no constructors whatsoever. Thus, it indicates unreachable code, because no series of calls can ever terminate with a value at type {anchorName fragments}`Empty`. @@ -645,6 +666,9 @@ Using {anchorName fragments}`Empty` as one of the type arguments to {anchorName This can allow generic code to be used in contexts that have additional restrictions. ## Naming: Sums, Products, and Units +%%% +tag := "sum-products-units" +%%% Generally speaking, types that offer multiple constructors are called _sum types_, while types whose single constructor takes multiple arguments are called {deftech}_product types_. These terms are related to sums and products used in ordinary arithmetic. @@ -655,6 +679,9 @@ The product {anchorTerm fragments}`Bool × Unit` has the two values {anchorTerm Similarly, $`2 \times 1 = 2`, and $`2 + 1 = 3`. # Messages You May Meet +%%% +tag := "polymorphism-messages" +%%% :::paragraph Not all definable structures or inductive types can have the type {anchorTerm Prod}`Type`. @@ -858,6 +885,9 @@ def allFirewood : List Firewood := [ ::: # Exercises +%%% +tag := "polymorphism-exercises" +%%% * Write a function to find the last entry in a list. It should return an {anchorName fragments}`Option`. * Write a function that finds the first entry in a list that satisfies a given predicate. Start the definition with {anchorTerm List.findFirst?Ex}`def List.findFirst? {α : Type} (xs : List α) (predicate : α → Bool) : Option α := …`. diff --git a/book/FPLean/GettingToKnow/Structures.lean b/book/FPLean/GettingToKnow/Structures.lean index 1d6fae3..f9fb0e4 100644 --- a/book/FPLean/GettingToKnow/Structures.lean +++ b/book/FPLean/GettingToKnow/Structures.lean @@ -224,6 +224,9 @@ To make programs more concise, Lean also allows the structure type annotation in # Updating Structures +%%% +tag := "updating-structures" +%%% Imagine a function {anchorName zeroXBad}`zeroX` that replaces the {anchorName zeroXBad}`x` field of a {anchorName zeroXBad}`Point` with {anchorTerm zeroX}`0`. In most programming language communities, this sentence would mean that the memory location pointed to by {anchorName Point}`x` was to be overwritten with a new value. @@ -413,6 +416,9 @@ In this case, {lit}`TARGET` represents {anchorName fourAndThree}`fourAndThree`, This is because the target of the accessor notation is used as the first argument in which the type matches, not necessarily the first argument. # Exercises +%%% +tag := "structure-exercises" +%%% * Define a structure named {anchorName RectangularPrism}`RectangularPrism` that contains the height, width, and depth of a rectangular prism, each as a {anchorName RectangularPrism}`Float`. * Define a function named {anchorTerm RectangularPrism}`volume : RectangularPrism → Float` that computes the volume of a rectangular prism. diff --git a/book/FPLean/GettingToKnow/Summary.lean b/book/FPLean/GettingToKnow/Summary.lean index 50f5e9e..708aac7 100644 --- a/book/FPLean/GettingToKnow/Summary.lean +++ b/book/FPLean/GettingToKnow/Summary.lean @@ -11,8 +11,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Intro" #doc (Manual) "Summary" => +%%% +tag := "getting-to-know-summary" +%%% # Evaluating Expressions +%%% +tag := none +%%% In Lean, computation occurs when expressions are evaluated. This follows the usual rules of mathematical expressions: sub-expressions are replaced by their values following the usual order of operations, until the entire expression has become a value. @@ -23,6 +29,9 @@ Similarly to mathematics but unlike most programming languages, Lean variables a Variables' values may come from global definitions with {kw}`def`, local definitions with {kw}`let`, as named arguments to functions, or from pattern matching. # Functions +%%% +tag := none +%%% Functions in Lean are first-class values, meaning that they can be passed as arguments to other functions, saved in variables, and used like any other value. Every Lean function takes exactly one argument. @@ -38,6 +47,9 @@ There are three primary ways of creating functions: 3. Functions can be defined using {kw}`def` or {kw}`let` by adding an argument list or by using pattern-matching notation. # Types +%%% +tag := none +%%% Lean checks that every expression has a type. Types, such as {anchorName fragments}`Int`, {anchorName fragments}`Point`, {anchorTerm fragments}`{α : Type} → Nat → α → List α`, and {anchorTerm fragments}`Option (String ⊕ (Nat × String))`, describe the values that may eventually be found for an expression. @@ -62,6 +74,9 @@ Because types are first class in Lean, polymorphism does not require any special Naming an argument in a function type allows later types to mention that name, and when the function is applied to an argument, the type of the resulting term is found by replacing the argument's name with the actual value it was applied to. # Structures and Inductive Types +%%% +tag := none +%%% Brand new datatypes can be introduced to Lean using the {kw}`structure` or {kw}`inductive` features. These new types are not considered to be equivalent to any other type, even if their definitions are otherwise identical. @@ -73,8 +88,10 @@ Datatypes defined with {kw}`structure` are provided with one accessor function f Both structures and inductive datatypes may be consumed with pattern matching, which exposes the values stored inside of constructors using a subset of the syntax used to call said constructors. Pattern matching means that knowing how to create a value implies knowing how to consume it. - # Recursion +%%% +tag := none +%%% A definition is recursive when the name being defined is used in the definition itself. Because Lean is an interactive theorem prover in addition to being a programming language, there are certain restrictions placed on recursive definitions. diff --git a/book/FPLean/GettingToKnow/Types.lean b/book/FPLean/GettingToKnow/Types.lean index 2104f39..81a4035 100644 --- a/book/FPLean/GettingToKnow/Types.lean +++ b/book/FPLean/GettingToKnow/Types.lean @@ -13,7 +13,9 @@ set_option verso.exampleModule "Examples.Intro" #doc (Manual) "Types" => - +%%% +tag := "getting-to-know-types" +%%% Types classify programs based on the values that they can compute. Types serve a number of roles in a program: diff --git a/book/FPLean/HelloWorld/Cat.lean b/book/FPLean/HelloWorld/Cat.lean index e0df920..41f2984 100644 --- a/book/FPLean/HelloWorld/Cat.lean +++ b/book/FPLean/HelloWorld/Cat.lean @@ -14,6 +14,9 @@ set_option verso.exampleModule "FelineLib" example_module Examples.Cat #doc (Manual) "Worked Example: {lit}`cat`" => +%%% +tag := "example-cat" +%%% The standard Unix utility {lit}`cat` takes a number of command-line options, followed by zero or more input files. If no files are provided, or if one of them is a dash ({lit}`-`), then it takes the standard input as the corresponding input instead of reading a file. @@ -29,7 +32,10 @@ To get the most benefit from this section, follow along yourself. It's OK to copy-paste the code examples, but it's even better to type them in by hand. This makes it easier to learn the mechanical process of typing in code, recovering from mistakes, and interpreting feedback from the compiler. -# Getting started +# Getting Started +%%% +tag := "example-cat-start" +%%% The first step in implementing {lit}`feline` is to create a package and decide how to organize the code. In this case, because the program is so simple, all the code will be placed in {lit}`Main.lean`. @@ -58,6 +64,9 @@ Ensure that the code can be built by running {command feline1 "feline/1"}`lake b # Concatenating Streams +%%% +tag := "example-cat-streams" +%%% Now that the basic skeleton of the program has been built, it's time to actually enter the code. A proper implementation of {lit}`cat` can be used with infinite IO streams, such as {lit}`/dev/random`, which means that it can't read its input into memory before outputting it. @@ -191,6 +200,9 @@ Each recursive call is provided with the tail of the input list, and all Lean li Thus, {anchorName process}`process` does not introduce any non-termination. ## Main +%%% +tag := "example-cat-main" +%%% The final step is to write the {anchorName main}`main` action. Unlike prior examples, {anchorName main}`main` in {lit}`feline` is a function. @@ -209,6 +221,9 @@ def main (args : List String) : IO UInt32 := ``` # Meow! +%%% +tag := "example-cat-running" +%%% :::paragraph To check whether {lit}`feline` works, the first step is to build it with {command feline2 "feline/2"}`lake build`. @@ -257,6 +272,9 @@ and curl up! # Exercise +%%% +tag := "example-cat-exercise" +%%% Extend {lit}`feline` with support for usage information. The extended version should accept a command-line argument {lit}`--help` that causes documentation about the available command-line options to be written to standard output. diff --git a/book/FPLean/HelloWorld/Conveniences.lean b/book/FPLean/HelloWorld/Conveniences.lean index bf0e392..688c5c9 100644 --- a/book/FPLean/HelloWorld/Conveniences.lean +++ b/book/FPLean/HelloWorld/Conveniences.lean @@ -12,6 +12,9 @@ set_option verso.exampleModule "FelineLib" #doc (Manual) "Additional Conveniences" => +%%% +tag := "hello-world-conveniences" +%%% # Nested Actions %%% @@ -128,6 +131,9 @@ invalid use of `(<- ...)`, must be nested inside a 'do' expression # Flexible Layouts for {lit}`do` +%%% +tag := "do-layout-syntax" +%%% In Lean, {moduleTerm (module := Examples.Cat)}`do` expressions are whitespace-sensitive. Each {moduleName (module := Examples.Cat)}`IO` action or local binding in the {moduleTerm (module := Examples.Cat)}`do` is expected to start on its own line, and they should all have the same indentation. @@ -174,6 +180,9 @@ def main : IO Unit := do Idiomatic Lean code uses curly braces with {moduleTerm (module := Examples.Cat)}`do` very rarely. # Running {lit}`IO` Actions With {kw}`#eval` +%%% +tag := "eval-io" +%%% Lean's {moduleTerm (module := Examples.Cat)}`#eval` command can be used to execute {moduleName (module := Examples.Cat)}`IO` actions, rather than just evaluating them. Normally, adding a {moduleTerm (module := Examples.Cat)}`#eval` command to a Lean file causes Lean to evaluate the provided expression, convert the resulting value to a string, and provide that string as a tooltip and in the info window. diff --git a/book/FPLean/HelloWorld/RunningAProgram.lean b/book/FPLean/HelloWorld/RunningAProgram.lean index b0e882b..eb95bea 100644 --- a/book/FPLean/HelloWorld/RunningAProgram.lean +++ b/book/FPLean/HelloWorld/RunningAProgram.lean @@ -38,6 +38,9 @@ The program displays {commandOut hello}`lean --run Hello.lean` and exits. # Anatomy of a Greeting +%%% +tag := "hello-world-parts" +%%% When Lean is invoked with the {lit}`--run` option, it invokes the program's {lit}`main` definition. In programs that do not take command-line arguments, {moduleName (module := Hello)}`main` should have type {moduleTerm}`IO Unit`. @@ -61,6 +64,9 @@ If it did return something interesting, then that would be indicated by the {mod # Functional Programming vs Effects +%%% +tag := "fp-effects" +%%% Lean's model of computation is based on the evaluation of mathematical expressions, in which variables are given exactly one value that does not change over time. The result of evaluating an expression does not change, and evaluating the same expression again will always yield the same result. @@ -96,6 +102,10 @@ From the external perspective of the program's user, there is a layer of side ef # Real-World Functional Programming +%%% +tag := "fp-world-passing" +%%% + The other useful way to think about side effects in Lean is by considering {moduleTerm}`IO` actions to be functions that take the entire world as an argument and return a value paired with a new world. In this case, reading a line of text from standard input _is_ a pure function, because a different world is provided as an argument each time. @@ -117,6 +127,9 @@ But real programs typically consist of a sequence of effects, rather than just o To enable programs to use multiple effects, there is a sub-language of Lean called {kw}`do` notation that allows these primitive {moduleTerm}`IO` actions to be safely composed into a larger, useful program. # Combining {anchorName all}`IO` Actions +%%% +tag := "combining-io-actions" +%%% Most useful programs accept input in addition to producing output. Furthermore, they may take decisions based on input, using the input data as part of a computation. @@ -134,8 +147,6 @@ def main : IO Unit := do stdout.putStrLn s!"Hello, {name}!" ``` - - In this program, the {anchorName all}`main` action consists of a {kw}`do` block. This block contains a sequence of _statements_, which can be both local variables (introduced using {kw}`let`) and actions that are to be executed. Just as SQL can be thought of as a special-purpose language for interacting with databases, the {kw}`do` syntax can be thought of as a special-purpose sub-language within Lean that is dedicated to modeling imperative programs. diff --git a/book/FPLean/HelloWorld/StartingAProject.lean b/book/FPLean/HelloWorld/StartingAProject.lean index 9425441..f5eaecd 100644 --- a/book/FPLean/HelloWorld/StartingAProject.lean +++ b/book/FPLean/HelloWorld/StartingAProject.lean @@ -11,6 +11,9 @@ set_option verso.exampleProject "../examples/second-lake/greeting" set_option verso.exampleModule "Main" #doc (Manual) "Starting a Project" => +%%% +tag := "starting-a-project" +%%% As a program written in Lean becomes more serious, an ahead-of-time compiler-based workflow that results in an executable becomes more attractive. Like other languages, Lean has tools for building multiple-file packages and managing dependencies. @@ -19,6 +22,10 @@ Lake is typically configured using a TOML file that declaratively specifies depe For advanced use cases, Lake can also be configured in Lean itself. # First steps +%%% +tag := "lake-new" +%%% + To get started with a project that uses Lake, use the command {command lake "first-lake"}`lake new greeting` in a directory that does not already contain a file or directory called {lit}`greeting`. This creates a directory called {lit}`greeting` that contains the following files: @@ -65,6 +72,9 @@ Running {command lake "first-lake/greeting"}`lake exe greeting` also results in # Lakefiles +%%% +tag := "lakefiles" +%%% A {lit}`lakefile.toml` describes a _package_, which is a coherent collection of Lean code for distribution, analogous to an {lit}`npm` or {lit}`nuget` package or a Rust crate. A package may contain any number of libraries or executables. @@ -101,6 +111,9 @@ By default, {lit}`lake build` builds those targets that are specified in the {li To build a target that is not a default target, specify the target's name as an argument after {lit}`lake build`. # Libraries and Imports +%%% +tag := "libraries-and-imports" +%%% A Lean library consists of a hierarchically organized collection of source files from which names can be imported, called _modules_. By default, a library has a single root file that matches its name. diff --git a/book/FPLean/HelloWorld/StepByStep.lean b/book/FPLean/HelloWorld/StepByStep.lean index e78d0b8..5018484 100644 --- a/book/FPLean/HelloWorld/StepByStep.lean +++ b/book/FPLean/HelloWorld/StepByStep.lean @@ -15,6 +15,9 @@ example_module Examples.HelloWorld #doc (Manual) "Step By Step" => +%%% +tag := "step-by-step" +%%% :::paragraph A {moduleTerm}`do` block can be executed one line at a time. @@ -31,6 +34,9 @@ Start with the program from the prior section: ::: # Standard IO +%%% +tag := "stdio" +%%% :::paragraph The first line is {anchor line1}`let stdin ← IO.getStdin`, while the remainder is: @@ -55,6 +61,9 @@ Next, this action is executed, actually returning the standard output. Finally, this value is associated with the name {anchorTerm line2}`stdout` for the remainder of the {moduleTerm}`do` block. # Asking a Question +%%% +tag := "asking-a-question" +%%% :::paragraph Now that {anchorTerm line1}`stdin` and {anchorTerm line2}`stdout` have been found, the remainder of the block consists of a question and an answer: @@ -122,6 +131,9 @@ In the current line of the program, whitespace characters (including the newline ::: # Greeting the User +%%% +tag := "greeting" +%%% :::paragraph All that remains to be executed in the {moduleTerm}`do` block is a single statement: @@ -135,6 +147,10 @@ Because this statement is an expression, it is evaluated to yield an {moduleTerm Once the expression has been evaluated, the resulting {moduleTerm}`IO` action is executed, resulting in the greeting. # {lit}`IO` Actions as Values +%%% +tag := "actions-as-values" +%%% + In the above description, it can be difficult to see why the distinction between evaluating expressions and executing {moduleTerm}`IO` actions is necessary. After all, each action is executed immediately after it is produced. @@ -290,6 +306,9 @@ The final step, {moduleTerm (module := Examples.HelloWorld)}`pure ()`, does not ::: # Exercise +%%% +tag := "step-by-step-exercise" +%%% :::paragraph Step through the execution of the following program on a piece of paper: diff --git a/book/FPLean/HelloWorld/Summary.lean b/book/FPLean/HelloWorld/Summary.lean index 31e6bb6..7772df2 100644 --- a/book/FPLean/HelloWorld/Summary.lean +++ b/book/FPLean/HelloWorld/Summary.lean @@ -13,8 +13,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.HelloWorld" #doc (Manual) "Summary" => +%%% +tag := "hello-world-summary" +%%% # Evaluation vs Execution +%%% +tag := none +%%% Side effects are aspects of program execution that go beyond the evaluation of mathematical expressions, such as reading files, throwing exceptions, or triggering industrial machinery. While most languages allow side effects to occur during evaluation, Lean does not. @@ -35,6 +41,9 @@ An {moduleName}`IO` action {anchorName MainTypes}`main` is executed when the pro # {lit}`do` Notation +%%% +tag := none +%%% The Lean standard library provides a number of basic {moduleName}`IO` actions that represent effects such as reading from and writing to files and interacting with standard input and standard output. These base {moduleName}`IO` actions are composed into larger {moduleName}`IO` actions using {kw}`do` notation, which is a built-in domain-specific language for writing descriptions of programs with side effects. @@ -52,6 +61,9 @@ This unique name then replaces the origin site of the nested action. # Compiling and Running Programs +%%% +tag := none +%%% A Lean program that consists of a single file with a {moduleName}`main` definition can be run using {lit}`lean --run FILE`. While this can be a nice way to get started with a simple program, most programs will eventually graduate to a multiple-file project that should be compiled before running. @@ -63,6 +75,9 @@ Lake package configuration is another domain-specific language. Use {lit}`lake build` to build a project. # Partiality +%%% +tag := none +%%% One consequence of following the mathematical model of expression evaluation is that every expression must have a value. This rules out both incomplete pattern matches that fail to cover all constructors of a datatype and programs that can fall into an infinite loop. diff --git a/book/FPLean/Intro.lean b/book/FPLean/Intro.lean index d284aff..1151384 100644 --- a/book/FPLean/Intro.lean +++ b/book/FPLean/Intro.lean @@ -46,6 +46,9 @@ These are worth doing, in order to cement your understanding of the section. It is also useful to explore Lean as you read the book, finding creative new ways to use what you have learned. # Getting Lean +%%% +tag := "getting-lean" +%%% Before writing and running programs written in Lean, you'll need to set up Lean on your own computer. The Lean tooling consists of the following: @@ -59,6 +62,9 @@ The Lean tooling consists of the following: Please refer to the [Lean manual](https://lean-lang.org/lean4/doc/quickstart.html) for up-to-date instructions for installing Lean. # Typographical Conventions +%%% +tag := "typographical-conventions" +%%% Code examples that are provided to Lean as _input_ are formatted like this: @@ -97,6 +103,9 @@ declaration uses 'sorry' ``` # Unicode +%%% +tag := "unicode" +%%% Idiomatic Lean code makes use of a variety of Unicode characters that are not part of ASCII. @@ -112,86 +121,139 @@ In Emacs, use {lit}`C-c C-k` with point on the character in question. # Release history %%% +tag := "release-history" number := false htmlSplit := .never %%% ## October, 2025 +%%% +tag := none +%%% The book has been updated to the latest stable Lean release (version 4.23.0), and now describes functional induction and the {tactic}`grind` tactic. ## August, 2025 +%%% +tag := none +%%% This is a maintenance release to resolve an issue with copy-pasting code from the book. ## July, 2025 +%%% +tag := none +%%% The book has been updated for version 4.21 of Lean. ## June, 2025 +%%% +tag := none +%%% The book has been reformatted with Verso. ## April, 2025 +%%% +tag := none +%%% The book has been extensively updated and now describes Lean version 4.18. ## January, 2024 +%%% +tag := none +%%% This is a minor bugfix release that fixes a regression in an example program. ## October, 2023 +%%% +tag := none +%%% In this first maintenance release, a number of smaller issues were fixed and the text was brought up to date with the latest release of Lean. ## May, 2023 +%%% +tag := none +%%% The book is now complete! Compared to the April pre-release, many small details have been improved and minor mistakes have been fixed. ## April, 2023 +%%% +tag := none +%%% This release adds an interlude on writing proofs with tactics as well as a final chapter that combines discussion of performance and cost models with proofs of termination and program equivalence. This is the last release prior to the final release. ## March, 2023 +%%% +tag := none +%%% This release adds a chapter on programming with dependent types and indexed families. ## January, 2023 +%%% +tag := none +%%% This release adds a chapter on monad transformers that includes a description of the imperative features that are available in {kw}`do`-notation. ## December, 2022 +%%% +tag := none +%%% This release adds a chapter on applicative functors that additionally describes structures and type classes in more detail. This is accompanied with improvements to the description of monads. The December 2022 release was delayed until January 2023 due to winter holidays. ## November, 2022 +%%% +tag := none +%%% This release adds a chapter on programming with monads. Additionally, the example of using JSON in the coercions section has been updated to include the complete code. ## October, 2022 - +%%% +tag := none +%%% This release completes the chapter on type classes. In addition, a short interlude introducing propositions, proofs, and tactics has been added just before the chapter on type classes, because a small amount of familiarity with the concepts helps to understand some of the standard library type classes. ## September, 2022 - +%%% +tag := none +%%% This release adds the first half of a chapter on type classes, which are Lean's mechanism for overloading operators and an important means of organizing code and structuring libraries. Additionally, the second chapter has been updated to account for changes in Lean's stream API. ## August, 2022 - +%%% +tag := none +%%% This third public release adds a second chapter, which describes compiling and running programs along with Lean's model for side effects. ## July, 2022 - +%%% +tag := none +%%% The second public release completes the first chapter. ## June, 2022 - +%%% +tag := none +%%% This was the first public release, consisting of an introduction and part of the first chapter. # About the Author +%%% +tag := "about-the-author" +%%% David Thrane Christiansen has been using functional languages for twenty years, and dependent types for ten. Together with Daniel P. Friedman, he wrote [_The Little Typer_](https://thelittletyper.com/), an introduction to the key ideas of dependent type theory. @@ -201,6 +263,9 @@ Since leaving academia, he has worked as a software developer at Galois in Portl At the time of writing, he is employed at the [Lean Focused Research Organization](https://lean-fro.org) working full-time on Lean. # License +%%% +tag := "license" +%%% {creativeCommons} diff --git a/book/FPLean/MonadTransformers/Conveniences.lean b/book/FPLean/MonadTransformers/Conveniences.lean index 694b1af..a816e97 100644 --- a/book/FPLean/MonadTransformers/Conveniences.lean +++ b/book/FPLean/MonadTransformers/Conveniences.lean @@ -10,8 +10,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.MonadTransformers.Conveniences" #doc (Manual) "Additional Conveniences" => +%%% +tag := "monad-transformer-conveniences" +%%% # Pipe Operators +%%% +tag := "pipe-operators" +%%% Functions are normally written before their arguments. When reading a program from left to right, this promotes a view in which the function's _output_ is paramount—the function has a goal to achieve (that is, a value to compute), and it receives arguments to support it in this process. @@ -66,6 +72,9 @@ As a final convenience, Lean provides the “pipeline dot” operator, which gro With “pipeline dot”, the example can be rewritten to {anchorTerm listReverseDropReversePipe}`[1, 2, 3] |>.reverse |>.drop 1 |>.reverse`. # Infinite Loops +%%% +tag := "infinite-loops" +%%% Within a {kw}`do`-block, the {kw}`repeat` keyword introduces an infinite loop. For example, a program that spams the string {anchorTerm spam}`"Spam!"` can use it: @@ -103,6 +112,9 @@ Instead, {kw}`repeat` makes use of a type whose {anchorTerm names}`ForM` instanc Partiality does not “infect” calling functions. # While Loops +%%% +tag := "while-loops" +%%% When programming with local mutability, {kw}`while` loops can be a convenient alternative to {kw}`repeat` with an {kw}`if`-guarded {kw}`break`: diff --git a/book/FPLean/MonadTransformers/Do.lean b/book/FPLean/MonadTransformers/Do.lean index 9da126e..be76daa 100644 --- a/book/FPLean/MonadTransformers/Do.lean +++ b/book/FPLean/MonadTransformers/Do.lean @@ -11,11 +11,17 @@ set_option verso.exampleModule "Examples.MonadTransformers.Do" #doc (Manual) "More do Features" => +%%% +tag := "more-do-features" +%%% Lean's {kw}`do`-notation provides a syntax for writing programs with monads that resembles imperative programming languages. In addition to providing a convenient syntax for programs with monads, {kw}`do`-notation provides syntax for using certain monad transformers. # Single-Branched {kw}`if` +%%% +tag := "single-branched-if" +%%% When working in a monad, a common pattern is to carry out a side effect only if some condition is true. For instance, {anchorName countLettersModify (module := Examples.MonadTransformers.Defs)}`countLetters` contains a check for vowels or consonants, and letters that are neither have no effect on the state. @@ -85,6 +91,9 @@ They simply replace the missing branch with {anchorTerm count}`pure ()`. The remaining extensions in this section, however, require Lean to automatically rewrite the {kw}`do`-block to add a local transformer on top of the monad that the {kw}`do`-block is written in. # Early Return +%%% +tag := "early-return" +%%% The standard library contains a function {anchorName findHuh}`List.find?` that returns the first entry in a list that satisfies some check. A simple implementation that doesn't make use of the fact that {anchorName findHuh}`Option` is a monad loops over the list using a recursive function, with an {kw}`if` to stop the loop when the desired entry is found: @@ -219,6 +228,9 @@ def greet (name : String) : String := the expression {anchorTerm greetDavid}`greet "David"` evaluates to {anchorTerm greetDavid}`"Hello, David"`, not just {anchorTerm greetDavid}`"David"`. # Loops +%%% +tag := "loops" +%%% Just as every program with mutable state can be rewritten to a program that passes the state as arguments, every loop can be rewritten as a recursive function. From one perspective, {anchorName findHuh}`List.find?` is most clear as a recursive function. @@ -229,6 +241,9 @@ After all, the program consults the entries in order until a satisfactory one is If the loop terminates without having returned, the answer is {anchorName findHuhSimple}`none`. ## Looping with ForM +%%% +tag := "looping-with-forM" +%%% Lean includes a type class that describes looping over a container type in some monad. This class is called {anchorName ForM}`ForM`: @@ -379,6 +394,9 @@ Ok ``` ## Stopping Iteration +%%% +tag := "break" +%%% Terminating a loop early is difficult to do with {anchorName ForM}`ForM`. Writing a function that iterates over the {anchorName AllLessThan}`Nat`s in an {anchorName AllLessThan}`AllLessThan` only until {anchorTerm OptionTcountToThree}`3` is reached requires a means of stopping the loop partway through. @@ -555,6 +573,9 @@ def printArray [ToString α] (xs : Array α) : IO Unit := do In this example, {anchorName printArray}`h` is evidence that {lit}`i ∈ [0:xs.size]`, and the tactic that checks whether {anchorTerm printArray}`xs[i]` is safe is able to transform this into evidence that {lit}`i < xs.size`. # Mutable Variables +%%% +tag := "let-mut" +%%% In addition to early {kw}`return`, {kw}`else`-less {kw}`if`, and {kw}`for` loops, Lean supports local mutable variables within a {kw}`do` block. Behind the scenes, these mutable variables desugar to code that's equivalent to {anchorName twoStateT}`StateT`, rather than being implemented by true mutable variables. @@ -634,6 +655,9 @@ yields the following error on the attempted mutation of {anchorName nonLocalMut} This is because the recursive function is written in the identity monad, and only the monad of the {kw}`do`-block in which the variable is introduced is transformed with {anchorName twoStateT}`StateT`. # What counts as a {kw}`do` block? +%%% +tag := "do-block-boundaries" +%%% Many features of {kw}`do`-notation apply only to a single {kw}`do`-block. Early return terminates the current block, and mutable variables can only be mutated in the block that they are defined in. @@ -748,6 +772,9 @@ example : Id Unit := do # Imperative or Functional Programming? +%%% +tag := none +%%% The imperative features provided by Lean's {kw}`do`-notation allow many programs to very closely resemble their counterparts in languages like Rust, Java, or C#. This resemblance is very convenient when translating an imperative algorithm into Lean, and some tasks are just most naturally thought of imperatively. @@ -756,6 +783,9 @@ Monads and monad transformers allow functional versus imperative programming to # Exercises +%%% +tag := "monad-transformer-do-exercises" +%%% * Rewrite {lit}`doug` to use {kw}`for` instead of the {anchorName doList (module:=DirTree)}`doList` function. * Are there other opportunities to use the features introduced in this section to improve the code? If so, use them! diff --git a/book/FPLean/MonadTransformers/Order.lean b/book/FPLean/MonadTransformers/Order.lean index 979c6df..b637e41 100644 --- a/book/FPLean/MonadTransformers/Order.lean +++ b/book/FPLean/MonadTransformers/Order.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.MonadTransformers.Defs" #doc (Manual) "Ordering Monad Transformers" => +%%% +tag := "monad-transformer-order" +%%% When composing a monad from a stack of monad transformers, it's important to be aware that the order in which the monad transformers are layered matters. Different orderings of the same set of transformers result in different monads. @@ -129,6 +132,9 @@ When an exception is thrown in {anchorName M1eval}`M1`, there is no final state. When an exception is thrown in {anchorName M2eval}`M2`, it is accompanied by a state. # Commuting Monads +%%% +tag := "commuting-monads" +%%% In the jargon of functional programming, two monad transformers are said to _commute_ if they can be re-ordered without the meaning of the program changing. The fact that the result of the program can differ when {anchorName SomeMonads}`StateT` and {anchorName SomeMonads}`ExceptT` are reordered means that state and exceptions do not commute. @@ -148,6 +154,9 @@ With great expressive power comes the responsibility to check that what's being # Exercises +%%% +tag := "monad-transformer-order-exercises" +%%% * Check that {anchorName m}`ReaderT` and {anchorName SomeMonads}`StateT` commute by expanding their definitions and reasoning about the resulting types. * Do {anchorName m}`ReaderT` and {anchorName SomeMonads}`ExceptT` commute? Check your answer by expanding their definitions and reasoning about the resulting types. diff --git a/book/FPLean/MonadTransformers/ReaderIO.lean b/book/FPLean/MonadTransformers/ReaderIO.lean index 748a019..345d28f 100644 --- a/book/FPLean/MonadTransformers/ReaderIO.lean +++ b/book/FPLean/MonadTransformers/ReaderIO.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "DirTree" #doc (Manual) "Combining IO and Reader" => +%%% +tag := "io-reader" +%%% One case where a reader monad can be useful is when there is some notion of the “current configuration” of the application that is passed through many recursive calls. An example of such a program is {lit}`tree`, which recursively prints the files in the current directory and its subdirectories, indicating their tree structure using characters. @@ -190,6 +193,9 @@ def doList [Applicative f] : List α → (α → f Unit) → f Unit # Using a Custom Monad +%%% +tag := "reader-io-custom-monad" +%%% While this implementation of {lit}`doug` works, manually passing the configuration around is verbose and error-prone. The type system will not catch it if the wrong configuration is passed downwards, for instance. @@ -303,6 +309,9 @@ Monad transformers consist of: 3. An operator to “lift” an action from the inner monad to the transformed monad, akin to {anchorName runIO}`runIO` # Adding a Reader to Any Monad +%%% +tag := "ReaderT" +%%% Adding a reader effect to {anchorName ConfigIO}`IO` was accomplished in {anchorName ConfigIO}`ConfigIO` by wrapping {anchorTerm ConfigIO}`IO α` in a function type. The Lean standard library contains a function that can do this to _any_ polymorphic type, called {anchorName MyReaderT}`ReaderT`: @@ -439,13 +448,22 @@ Finally, using a set of type classes included in the standard library, polymorph Just as some functions work in any monad, others can work in any monad that provides a certain type of state, or a certain type of exceptions, without having to specifically describe the _way_ in which a particular concrete monad provides the state or exceptions. # Exercises +%%% +tag := "reader-io-exercises" +%%% ## Controlling the Display of Dotfiles +%%% +tag := none +%%% Files whose names begin with a dot character ({lit}`'.'`) typically represent files that should usually be hidden, such as source-control metadata and configuration files. Modify {lit}`doug` with an option to show or hide filenames that begin with a dot. This option should be controlled with a {lit}`-a` command-line option. ## Starting Directory as Argument +%%% +tag := none +%%% Modify {lit}`doug` so that it takes a starting directory as an additional command-line argument. diff --git a/book/FPLean/MonadTransformers/Summary.lean b/book/FPLean/MonadTransformers/Summary.lean index 3c382a2..40397c9 100644 --- a/book/FPLean/MonadTransformers/Summary.lean +++ b/book/FPLean/MonadTransformers/Summary.lean @@ -10,8 +10,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.MonadTransformers" #doc (Manual) "Summary" => +%%% +tag := "monad-transformer-summary" +%%% # Combining Monads +%%% +tag := none +%%% When writing a monad from scratch, there are design patterns that tend to describe the ways that each effect is added to the monad. Reader effects are added by having the monad's type be a function from the reader's environment, state effects are added by including a function from the initial state to the value paired with the final state, failure or exceptions are added by including a sum type in the return type, and logging or other output is added by including a product type in the return type. @@ -26,6 +32,9 @@ At a minimum, a monad transformer should provide the following instances: Monad transformers may be implemented as polymorphic structures or inductive datatypes, but they are most often implemented as functions from the underlying monad type to the enhanced monad type. # Type Classes for Effects +%%% +tag := none +%%% A common design pattern is to implement a particular effect by defining a monad that has the effect, a monad transformer that adds it to another monad, and a type class that provides a generic interface to the effect. This allows programs to be written that merely specify which effects they need, so the caller can provide any monad that has the right effects. @@ -35,12 +44,18 @@ The output parameter is most useful for simple programs that use each kind of ef Thus, both versions are typically provided, with the ordinary-parameter version of the type class having a name that ends in {lit}`-Of`. # Monad Transformers Don't Commute +%%% +tag := none +%%% It is important to note that changing the order of transformers in a monad can change the meaning of programs that use the monad. For instance, re-ordering {anchorName Summary}`StateT` and {anchorTerm Summary}`ExceptT` can result either in programs that lose state modifications when exceptions are thrown or programs that keep changes. While most imperative languages provide only the latter, the increased flexibility provided by monad transformers demands thought and attention to choose the correct variety for the task at hand. # {kw}`do`-Notation for Monad Transformers +%%% +tag := none +%%% Lean's {kw}`do`-blocks support early return, in which the block is terminated with some value, locally mutable variables, {kw}`for`-loops with {kw}`break` and {kw}`continue`, and single-branched {kw}`if`-statements. While this may seem to be introducing imperative features that would get in the way of using Lean to write proofs, it is in fact nothing more than a more convenient syntax for certain common uses of monad transformers. diff --git a/book/FPLean/MonadTransformers/Transformers.lean b/book/FPLean/MonadTransformers/Transformers.lean index b2ec43b..a1a025e 100644 --- a/book/FPLean/MonadTransformers/Transformers.lean +++ b/book/FPLean/MonadTransformers/Transformers.lean @@ -28,6 +28,9 @@ The type classes are a way for programs to express their requirements, and monad # Failure with {lit}`OptionT` +%%% +tag := "OptionT" +%%% Failure, represented by the {anchorName OptionExcept}`Option` monad, and exceptions, represented by the {anchorName M1eval}`Except` monad, both have corresponding transformers. In the case of {anchorName OptionTdef}`Option`, failure can be added to a monad by having it contain values of type {anchorTerm OptionTdef}`Option α` where it would otherwise contain values of type {anchorName OptionTdef}`α`. @@ -81,6 +84,9 @@ def interact : IO Unit := do ``` ## The Monad Instance +%%% +tag := "OptionT-monad-instance" +%%% Writing the monad instance reveals a difficulty. Based on the types, {anchorName MonadExceptT}`pure` should use {anchorName MonadMissingUni}`pure` from the underlying monad {anchorName firstMonadOptionT}`m` together with {anchorName firstMonadOptionT}`some`. @@ -210,6 +216,9 @@ The final rule states that {anchorTerm OptionTThirdLaw}`bind (bind v f) g` is t It can be checked in the same way, by expanding the definitions of {anchorName OptionTThirdLaw}`bind` and {anchorName OptionTSecondLaw}`pure` and then delegating to the underlying monad {anchorName OptionTFirstLaw}`m`. ## An {lit}`Alternative` Instance +%%% +tag := "OptionT-Alternative-instance" +%%% One convenient way to use {anchorName OptionTdef}`OptionT` is through the {anchorName AlternativeOptionT}`Alternative` type class. Successful return is already indicated by {anchorName AlternativeOptionT}`pure`, and the {anchorName AlternativeOptionT}`failure` and {anchorName AlternativeOptionT}`orElse` methods of {anchorName AlternativeOptionT}`Alternative` provide a way to write a program that returns the first successful result from a number of subprograms: @@ -225,6 +234,9 @@ instance [Monad m] : Alternative (OptionT m) where ## Lifting +%%% +tag := "OptionT-lifting" +%%% Lifting an action from {anchorName LiftOptionT}`m` to {anchorTerm LiftOptionT}`OptionT m` only requires wrapping {anchorName LiftOptionT}`some` around the result of the computation: @@ -236,6 +248,9 @@ instance [Monad m] : MonadLift m (OptionT m) where # Exceptions +%%% +tag := "exceptions" +%%% The monad transformer version of {anchorName ExceptT}`Except` is very similar to the monad transformer version of {anchorName m}`Option`. Adding exceptions of type {anchorName ExceptT}`ε` to some monadic action of type {anchorTerm ExceptT}`m`{lit}` `{anchorTerm ExceptT}`α` can be accomplished by adding exceptions to {anchorName MonadExcept}`α`, yielding type {anchorTerm ExceptT}`m (Except ε α)`: @@ -311,6 +326,9 @@ instance [Monad m] : MonadLift m (ExceptT ε m) where ``` ## Type Classes for Exceptions +%%% +tag := "exceptions-type-classes" +%%% Exception handling fundamentally consists of two operations: the ability to throw exceptions, and the ability to recover from them. Thus far, this has been accomplished using the constructors of {anchorName m}`Except` and pattern matching, respectively. @@ -384,6 +402,9 @@ In addition to {anchorName m}`Except` and {anchorName ExceptT}`ExceptT`, there a For example, failure due to {anchorName m}`Option` can be seen as throwing an exception that contains no data whatsoever, so there is an instance of {anchorTerm OptionExcept}`MonadExcept Unit Option` that allows {kw}`try`{lit}` ...`{kw}`catch`{lit}` ...` syntax to be used with {anchorName m}`Option`. # State +%%% +tag := "state-monad" +%%% A simulation of mutable state is added to a monad by having monadic actions accept a starting state as an argument and return a final state together with their result. The bind operator for a state monad provides the final state of one action as an argument to the next action, threading the state through the program. @@ -496,6 +517,9 @@ class MonadState (σ : outParam (Type u)) (m : Type u → Type v) : While it would be possible to provide a default implementation of {anchorName MonadState}`modifyGet` in terms of {anchorName MonadState}`get` and {anchorName MonadState}`set`, it would not admit the optimizations that make {anchorName MonadState}`modifyGet` useful in the first place, rendering the method useless. # {lit}`Of` Classes and {lit}`The` Functions +%%% +tag := "of-and-the" +%%% Thus far, each monad type class that takes extra information, like the type of exceptions for {anchorName MonadExcept}`MonadExcept` or the type of the state for {anchorName MonadState}`MonadState`, has this type of extra information as an output parameter. For simple programs, this is generally convenient, because a monad that combines one use each of {anchorName MonadStateT}`StateT`, {anchorName m}`ReaderT`, and {anchorName ExceptT}`ExceptT` has only a single state type, environment type, and exception type. @@ -534,6 +558,9 @@ In other words, implementing the {lit}`Of` version yields implementations of bot It's generally a good idea to implement the {lit}`Of` version, and then start writing programs using the non-{lit}`Of` versions of the class, transitioning to the {lit}`Of` version if the output parameter becomes inconvenient. # Transformers and {lit}`Id` +%%% +tag := "transformers-and-Id" +%%% The identity monad {anchorName various}`Id` is the monad that has no effects whatsoever, to be used in contexts that expect a monad for some reason but where none is actually necessary. Another use of {anchorName various}`Id` is to serve as the bottom of a stack of monad transformers. @@ -541,17 +568,29 @@ For instance, {anchorTerm StateTDoubleB}`StateT σ Id` works just like {anchorTe # Exercises +%%% +tag := "monad-transformer-exercises" +%%% ## Monad Contract +%%% +tag := none +%%% Using pencil and paper, check that the rules of the monad transformer contract are satisfied for each monad transformer in this section. ## Logging Transformer +%%% +tag := none +%%% Define a monad transformer version of {anchorName WithLog (module:=Examples.Monads)}`WithLog`. Also define the corresponding type class {lit}`MonadWithLog`, and write a program that combines logging and exceptions. ## Counting Files +%%% +tag := none +%%% Modify {lit}`doug`'s monad with {anchorName MonadStateT}`StateT` such that it counts the number of directories and files seen. At the end of execution, it should display a report like: diff --git a/book/FPLean/Monads.lean b/book/FPLean/Monads.lean index a30e742..b753927 100644 --- a/book/FPLean/Monads.lean +++ b/book/FPLean/Monads.lean @@ -18,6 +18,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Monads" #doc (Manual) "Monads" => +%%% +tag := "monads" +%%% In C# and Kotlin, the {CSharp}`?.` operator is a way to look up a property or call a method on a potentially-null value. If the receiver is {CSharp}`null`, the whole expression is null. @@ -30,6 +33,9 @@ At the same time, logging is easiest to accomplish by having a dedicated logging Chained null checks and exceptions typically require language designers to anticipate this use case, while logging frameworks typically make use of side effects to decouple code that logs from the accumulation of the logs. # One API, Many Applications +%%% +tag := "monad-api-examples" +%%% All these features and more can be implemented in library code as instances of a common API called {moduleName}`Monad`. Lean provides dedicated syntax that makes this API convenient to use, but can also get in the way of understanding what is going on behind the scenes. @@ -37,6 +43,9 @@ This chapter begins with the nitty-gritty presentation of manually nesting null Please suspend your disbelief in the meantime. ## Checking for {lit}`none`: Don't Repeat Yourself +%%% +tag := "example-option-monad" +%%% :::paragraph In Lean, pattern matching can be used to chain checks for null. @@ -137,6 +146,10 @@ Improving the syntax used to write {anchorName firstThirdandThenExpl}`andThen` c ::: ### Infix Operators +%%% +tag := "defining-infix-operators" +%%% + In Lean, infix operators can be declared using the {kw}`infix`, {kw}`infixl`, and {kw}`infixr` commands, which create (respectively) non-associative, left-associative, and right-associative operators. When used multiple times in a row, a {deftech}_left associative_ operator stacks up the opening parentheses on the left side of the expression. @@ -183,6 +196,9 @@ def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) := ::: ## Propagating Error Messages +%%% +tag := "example-except-monad" +%%% Pure functional languages such as Lean have no built-in exception mechanism for error handling, because throwing or catching an exception is outside of the step-by-step evaluation model for expressions. However, functional programs certainly need to handle errors. @@ -634,6 +650,9 @@ Because {anchorName State}`State` simulates only a single local variable, {ancho ::: ## Monads: A Functional Design Pattern +%%% +tag := "monad-as-design-pattern" +%%% Each of these examples has consisted of: * A polymorphic type, such as {anchorName first}`Option`, {anchorTerm okExcept}`Except ε`, {anchorTerm save}`WithLog α`, or {anchorTerm andThenState}`State σ` diff --git a/book/FPLean/Monads/Arithmetic.lean b/book/FPLean/Monads/Arithmetic.lean index a7bef58..664ab50 100644 --- a/book/FPLean/Monads/Arithmetic.lean +++ b/book/FPLean/Monads/Arithmetic.lean @@ -10,7 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Monads.Class" #doc (Manual) "Example: Arithmetic in Monads" => - +%%% +tag := "monads-arithmetic-example" +%%% Monads are a way of encoding programs with side effects into a language that does not have them. It would be easy to read this as a sort of admission that pure functional programs are missing something important, requiring programmers to jump through hoops just to write a normal program. @@ -21,6 +23,9 @@ However, while using the {moduleName}`Monad` API does impose a syntactic cost on One example of a program that can make sense in a variety of monads is an evaluator for arithmetic expressions. # Arithmetic Expressions +%%% +tag := "monads-arithmetic-example-expr" +%%% :::paragraph An arithmetic expression is either a literal integer or a primitive binary operator applied to two expressions. The operators are addition, subtraction, multiplication, and division: @@ -61,6 +66,9 @@ def fourteenDivided : Expr Arith := ::: # Evaluating Expressions +%%% +tag := "monads-arithmetic-example-eval" +%%% :::paragraph Because expressions include division, and division by zero is undefined, evaluation might fail. @@ -207,6 +215,9 @@ In this refactored code, the fact that the two code paths differ only in their t ::: # Further Effects +%%% +tag := "monads-arithmetic-example-effects" +%%% Failure and exceptions are not the only kinds of effects that can be interesting when working with an evaluator. While division's only side effect is failure, adding other primitive operators to the expressions make it possible to express other effects. @@ -256,6 +267,9 @@ def evaluateM [Monad m] ``` ## No Effects +%%% +tag := "monads-arithmetic-example-no-effects" +%%% The type {anchorName applyEmpty}`Empty` has no constructors, and thus no values, like the {Kotlin}`Nothing` type in Scala or Kotlin. In Scala and Kotlin, {Kotlin}`Nothing` can represent computations that never return a result, such as functions that crash the program, throw exceptions, or always fall into infinite loops. @@ -798,13 +812,22 @@ Similarly, Scheme and Racket's parameter objects are an effect that exactly corr The Kotlin idiom of context objects can solve a similar problem, but they are fundamentally a means of passing function arguments automatically, so this idiom is more like the encoding as a reader monad than it is an effect in the language. ## Exercises +%%% +tag := "monads-arithmetic-example-exercises" +%%% ### Checking Contracts +%%% +tag := none +%%% Check the monad contract for {anchorTerm StateMonad}`State σ` and {anchorTerm MonadOptionExcept}`Except ε`. ### Readers with Failure +%%% +tag := none +%%% Adapt the reader monad example so that it can also indicate failure when the custom operator is not defined, rather than just returning zero. In other words, given these definitions: @@ -820,6 +843,9 @@ do the following: 4. Define suitable {anchorName evaluateM}`applyPrim` operators and test them with {anchorName evaluateM}`evaluateM` on some example expressions ### A Tracing Evaluator +%%% +tag := "monads-arithmetic-example-exercise-trace" +%%% The {anchorName MonadWriter}`WithLog` type can be used with the evaluator to add optional tracing of some operations. In particular, the type {anchorName ToTrace}`ToTrace` can serve as a signal to trace a given operator: diff --git a/book/FPLean/Monads/Class.lean b/book/FPLean/Monads/Class.lean index 83e8df9..46e2ff0 100644 --- a/book/FPLean/Monads/Class.lean +++ b/book/FPLean/Monads/Class.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Monads.Class" #doc (Manual) "The Monad Type Class" => +%%% +tag := "monad-type-class" +%%% :::paragraph Rather than having to import an operator like {lit}`ok` or {lit}`andThen` for each type that is a monad, the Lean standard library contains a type class that allow them to be overloaded, so that the same operators can be used for _any_ monad. @@ -119,6 +122,9 @@ The fact that {anchorName firstThirdFifthSeventhMonad}`m` must have a {anchorNam ::: # General Monad Operations +%%% +tag := "monad-class-polymorphism" +%%% :::paragraph Because many different types are monads, functions that are polymorphic over _any_ monad are very powerful. @@ -210,6 +216,9 @@ Using this function with {anchorName mapMsaveIfEven}`mapM` results in a log cont # The Identity Monad +%%% +tag := "Id-monad" +%%% Monads encode programs with effects, such as failure, exceptions, or logging, into explicit representations as data and functions. Sometimes, however, an API will be written to use a monad for flexibility, but the API's client may not require any encoded effects. @@ -259,6 +268,9 @@ typeclass instance problem is stuck, it is often due to metavariables ::: # The Monad Contract +%%% +tag := "monad-contract" +%%% Just as every pair of instances of {anchorName MonadContract}`BEq` and {anchorName MonadContract}`Hashable` should ensure that any two equal values have the same hash, there is a contract that each instance of {anchorName MonadContract}`Monad` should obey. First, {anchorName MonadContract}`pure` should be a left identity of {anchorName MonadContract}`bind`. @@ -271,8 +283,14 @@ Because {anchorName MonadContract}`pure` has no effects, sequencing its effects The associative property of {anchorName MonadContract}`bind` basically says that the sequencing bookkeeping itself doesn't matter, so long as the order in which things are happening is preserved. # Exercises +%%% +tag := "monad-class-exercises" +%%% ## Mapping on a Tree +%%% +tag := none +%%% :::paragraph Define a function {anchorName ex1}`BinTree.mapM`. @@ -284,6 +302,9 @@ def BinTree.mapM [Monad m] (f : α → m β) : BinTree α → m (BinTree β) ::: ## The Option Monad Contract +%%% +tag := none +%%% :::paragraph First, write a convincing argument that the {anchorName badOptionMonad}`Monad` instance for {anchorName badOptionMonad}`Option` satisfies the monad contract. diff --git a/book/FPLean/Monads/Conveniences.lean b/book/FPLean/Monads/Conveniences.lean index e4e8226..1c6d8bd 100644 --- a/book/FPLean/Monads/Conveniences.lean +++ b/book/FPLean/Monads/Conveniences.lean @@ -10,8 +10,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Monads.Conveniences" #doc (Manual) "Additional Conveniences" => +%%% +tag := "monads-conveniences" +%%% # Shared Argument Types +%%% +tag := "shared-argument-types" +%%% When defining a function that takes multiple arguments that have the same type, both can be written before the same colon. For example, @@ -71,6 +77,9 @@ BinTree.empty : BinTree Nat ``` # Or-Patterns +%%% +tag := "or-patterns" +%%% In contexts that allow multiple patterns, such as {kw}`match`-expressions, multiple patterns may share their result expressions. The datatype {anchorName Weekday}`Weekday` that represents days of the week: diff --git a/book/FPLean/Monads/Do.lean b/book/FPLean/Monads/Do.lean index e1a5314..bd3c1a5 100644 --- a/book/FPLean/Monads/Do.lean +++ b/book/FPLean/Monads/Do.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Monads.Do" #doc (Manual) "{kw}`do`-Notation for Monads" => +%%% +tag := "monad-do-notation" +%%% While APIs based on monads are very powerful, the explicit use of {lit}`>>=` with anonymous functions is still somewhat noisy. Just as infix operators are used instead of explicit calls to {anchorName names}`HAdd.hAdd`, Lean provides a syntax for monads called _{kw}`do`-notation_ that can make programs that use monads easier to read and write. @@ -182,6 +185,9 @@ def number (t : BinTree α) : BinTree (Nat × α) := # Exercises +%%% +tag := "monad-do-notation-exercises" +%%% * Rewrite {anchorName evaluateM (module:=Examples.Monads.Class)}`evaluateM`, its helpers, and the different specific use cases using {kw}`do`-notation instead of explicit calls to {lit}`>>=`. * Rewrite {anchorName firstThirdFifthSeventhDo}`firstThirdFifthSeventh` using nested actions. diff --git a/book/FPLean/Monads/IO.lean b/book/FPLean/Monads/IO.lean index 0860a39..e05ca97 100644 --- a/book/FPLean/Monads/IO.lean +++ b/book/FPLean/Monads/IO.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Monads.IO" #doc (Manual) "The IO Monad" => +%%% +tag := "io-monad" +%%% {anchorName names}`IO` as a monad can be understood from two perspectives, which were described in the section on {ref "running-a-program"}[running programs]. Each can help to understand the meanings of {anchorName names}`pure` and {anchorName names}`bind` for {anchorName names}`IO`. diff --git a/book/FPLean/Monads/Summary.lean b/book/FPLean/Monads/Summary.lean index ee40533..a39bb46 100644 --- a/book/FPLean/Monads/Summary.lean +++ b/book/FPLean/Monads/Summary.lean @@ -10,8 +10,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.Monads.Class" #doc (Manual) "Summary" => +%%% +tag := "monads-summary" +%%% # Encoding Side Effects +%%% +tag := none +%%% Lean is a pure functional language. This means that it does not include side effects such as mutable variables, logging, or exceptions. @@ -24,6 +30,9 @@ Functional programming does not mean that programs can't use effects, it simply A Lean type signature describes not only the types of arguments that a function expects and the type of result that it returns, but also which effects it may use. # The Monad Type Class +%%% +tag := none +%%% It's possible to write purely functional programs in languages that allow effects anywhere. For example, {python}`2 + 3` is a valid Python program that has no effects at all. @@ -35,6 +44,9 @@ It has two methods: {anchorName FakeMonad}`pure` represents programs that have n The contract for {anchorName FakeMonad}`Monad` instances ensures that {anchorName FakeMonad}`bind` and {anchorName FakeMonad}`pure` actually capture pure computation and sequencing. # {kw}`do`-Notation for Monads +%%% +tag := none +%%% Rather than being limited to {moduleName}`IO`, {kw}`do`-notation works for any monad. It allows programs that use monads to be written in a style that is reminiscent of statement-oriented languages, with statements sequenced after one another. @@ -42,6 +54,9 @@ Additionally, {kw}`do`-notation enables a number of additional convenient shorth A program written with {kw}`do` is translated to applications of {lit}`>>=` behind the scenes. # Custom Monads +%%% +tag := none +%%% Different languages provide different sets of side effects. While most languages feature mutable variables and file I/O, not all have features like exceptions. @@ -50,6 +65,9 @@ An advantage to encoding effects with monads is that programs are not limited to Because Lean is designed to make programming with any monad convenient, programmers are free to choose exactly the set of side effects that make sense for any given application. # The {lit}`IO` Monad +%%% +tag := none +%%% Programs that can affect the real world are written as {moduleName}`IO` actions in Lean. {moduleName}`IO` is one monad among many. diff --git a/book/FPLean/NextSteps.lean b/book/FPLean/NextSteps.lean index fda2f85..b53d583 100644 --- a/book/FPLean/NextSteps.lean +++ b/book/FPLean/NextSteps.lean @@ -17,6 +17,9 @@ Using dependently-typed functional languages like Lean is a deep topic, and much Depending on your interests, the following resources might be useful for learning Lean 4. # Learning Lean +%%% +tag := "learning-lean" +%%% Lean 4 itself is described in the following resources: @@ -30,21 +33,33 @@ However, the best way to continue learning Lean is to start reading and writing Additionally, the [Lean Zulip](https://leanprover.zulipchat.com/) is an excellent place to meet other Lean users, ask for help, and help others. # Mathematics in Lean +%%% +tag := none +%%% A wide selection of learning resources for mathematicians are available at [the community site](https://leanprover-community.github.io/learn.html). # Using Dependent Types in Computer Science +%%% +tag := none +%%% Rocq is a language that has a lot in common with Lean. For computer scientists, the [Software Foundations](https://softwarefoundations.cis.upenn.edu/) series of interactive textbooks provides an excellent introduction to applications of Rocq in computer science. The fundamental ideas of Lean and Rocq are very similar, and skills are readily transferable between the systems. # Programming with Dependent Types +%%% +tag := none +%%% For programmers who are interested in learning to use indexed families and dependent types to structure programs, Edwin Brady's [_Type Driven Development with Idris_](https://www.manning.com/books/type-driven-development-with-idris) provides an excellent introduction. Like Rocq, Idris is a close cousin of Lean, though it lacks tactics. # Understanding Dependent Types +%%% +tag := none +%%% [_The Little Typer_](https://thelittletyper.com/) is a book for programmers who haven't formally studied logic or the theory of programming languages, but who want to build an understanding of the core ideas of dependent type theory. While all of the above resources aim to be as practical as possible, _The Little Typer_ presents an approach to dependent type theory where the very basics are built up from scratch, using only concepts from programming. diff --git a/book/FPLean/ProgramsProofs/ArraysTermination.lean b/book/FPLean/ProgramsProofs/ArraysTermination.lean index 0fe8790..255046e 100644 --- a/book/FPLean/ProgramsProofs/ArraysTermination.lean +++ b/book/FPLean/ProgramsProofs/ArraysTermination.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.ProgramsProofs.Arrays" #doc (Manual) "Arrays and Termination" => +%%% +tag := "array-termination" +%%% To write efficient code, it is important to select appropriate data structures. Linked lists have their place: in some applications, the ability to share the tails of lists is very important. @@ -23,6 +26,9 @@ Making effective use of arrays requires knowing how to prove to Lean that an arr Both of these are expressed using an inequality proposition, rather than propositional equality. # Inequality +%%% +tag := "inequality" +%%% Because different types have different notions of ordering, inequality is governed by two type classes, called {anchorName ordSugarClasses (module := Examples.Classes)}`LE` and {anchorName ordSugarClasses (module := Examples.Classes)}`LT`. The table in the section on {ref "equality-and-ordering"}[standard type classes] describes how these classes relate to the syntax: @@ -75,6 +81,9 @@ instance : LE Nat where Defining {anchorName LENat}`Nat.le` requires a feature of Lean that has not yet been presented: it is an inductively-defined relation. ## Inductively-Defined Propositions, Predicates, and Relations +%%% +tag := "inductive-props" +%%% {anchorName LENat}`Nat.le` is an _inductively-defined relation_. Just as {kw}`inductive` can be used to create new datatypes, it can be used to create new propositions. @@ -236,6 +245,9 @@ theorem four_is_not_three : ¬ IsThree 4 := by Just as a pattern match on a {anchorTerm otherEx (module:=Examples.DependentTypes)}`Vect String 2` doesn't need to include a case for {anchorName otherEx (module:=Examples.DependentTypes)}`Vect.nil`, a proof by cases over {anchorTerm fourNotThreeDone}`IsThree 4` doesn't need to include a case for {anchorName IsThree}`isThree`. ## Inequality of Natural Numbers +%%% +tag := "inequality-of-natural-numbers" +%%% The definition of {anchorName NatLe}`Nat.le` has a parameter and an index: @@ -395,6 +407,9 @@ Sometimes, creativity can be required in order to figure out just why a function # Exercises +%%% +tag := "array-termination-exercises" +%%% * Implement a {anchorTerm ForMArr}`ForM m (Array α)` instance on arrays using a tail-recursive accumulator-passing function and a {kw}`termination_by` clause. * Reimplement {anchorName ArrayMap}`Array.map`, {anchorName ArrayFind}`Array.find`, and the {anchorName ForMArr}`ForM` instance using {kw}`for`{lit}` ... `{kw}`in`{lit}` ...` loops in the identity monad and compare the resulting code. diff --git a/book/FPLean/ProgramsProofs/Fin.lean b/book/FPLean/ProgramsProofs/Fin.lean index 800a180..48e3793 100644 --- a/book/FPLean/ProgramsProofs/Fin.lean +++ b/book/FPLean/ProgramsProofs/Fin.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.ProgramsProofs.Fin" #doc (Manual) "Bounded Numbers" => +%%% +tag := "Fin" +%%% The {anchorTerm sundries}`GetElem` instance for {anchorName sundries}`Array` and {anchorName sundries}`Nat` requires a proof that the provided {anchorName sundries}`Nat` is smaller than the array. In practice, these proofs often end up being passed to functions along with the indices. @@ -53,6 +56,9 @@ def Array.find (arr : Array α) (p : α → Bool) : Option (Fin arr.size × α) ``` # Exercise +%%% +tag := "Fin-exercises" +%%% Write a function {anchorTerm exercise}`Fin.next? : Fin n → Option (Fin n)` that returns the next largest {anchorName nextThreeFin}`Fin` when it would be in bounds, or {anchorName ArrayFindHelper}`none` if not. Check that diff --git a/book/FPLean/ProgramsProofs/Inequalities.lean b/book/FPLean/ProgramsProofs/Inequalities.lean index 747dab6..b11cf0d 100644 --- a/book/FPLean/ProgramsProofs/Inequalities.lean +++ b/book/FPLean/ProgramsProofs/Inequalities.lean @@ -10,12 +10,19 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.ProgramsProofs.Inequalities" #doc (Manual) "More Inequalities" => +%%% +tag := "more-inequalities" +%%% Lean's built-in proof automation is sufficient to check that {anchorName ArrayMapHelperOk (module:=Examples.ProgramsProofs.Arrays)}`arrayMapHelper` and {anchorName ArrayFindHelper (module:=Examples.ProgramsProofs.Arrays)}`findHelper` terminate. All that was needed was to provide an expression whose value decreases with each recursive call. However, Lean's built-in automation is not magic, and it often needs some help. # Merge Sort +%%% +tag := "merge-sort" +%%% + One example of a function whose termination proof is non-trivial is merge sort on {moduleName}`List`. Merge sort consists of two phases: first, a list is split in half. @@ -123,6 +130,9 @@ halves : List α × List α := splitList xs ``` # Splitting a List Makes it Shorter +%%% +tag := "splitting-shortens" +%%% It will also be necessary to prove that {lit}`(splitList xs).snd.length < xs.length`. Because {anchorName splitList}`splitList` alternates between adding entries to the two lists, it is easiest to prove both statements at once, so the structure of the proof can follow the algorithm used to implement {anchorName splitList}`splitList`. @@ -295,6 +305,9 @@ The {anchorTerm splitList_shorter_le}`right` goal resembles the {lit}`right✝` It's time to prove that the inequality holds. ## Adding One to the Greater Side +%%% +tag := "le-succ-of-le" +%%% The inequality needed to prove {anchorName splitList_shorter_le}`splitList_shorter_le` is {anchorTerm le_succ_of_le_statement}`∀(n m : Nat), n ≤ m → n ≤ m + 1`. The incoming assumption that {anchorTerm le_succ_of_le_statement}`n ≤ m` essentially tracks the difference between {anchorName le_succ_of_le_statement}`n` and {anchorName le_succ_of_le_statement}`m` in the number of {anchorName le_succ_of_le_apply}`Nat.le.step` constructors. @@ -448,6 +461,9 @@ The short, highly-automated proof script is typically easier to maintain, becaus The recursive function is typically both harder to understand from the perspective of mathematical proofs and harder to maintain, but it can be a useful bridge for programmers who are beginning to work with interactive theorem proving. ## Finishing the Proof +%%% +tag := "finishing-splitList-shorter-proof" +%%% Now that both helper theorems have been proved, the rest of {anchorName splitList_shorter_le5}`splitList_shorter_le` will be completed quickly. The current proof state has one goal remaining: @@ -575,6 +591,10 @@ theorem splitList_shorter_snd (lst : List α) (h : lst.length ≥ 2) : ``` ## A Simpler Proof +%%% +tag := "splitList-shorter-le-simpler-proof" +%%% + :::paragraph Instead of using ordinary induction, {anchorName splitList_shorter_le_funInd1}`splitList_shorter_le` can be proved using functional induction, resulting in one case for each branch of {anchorName splitList}`splitList`: @@ -618,6 +638,9 @@ theorem splitList_shorter_le (lst : List α) : ``` # Merge Sort Terminates +%%% +tag := "merge-sort-terminates" +%%% Merge sort has two recursive calls, one for each sub-list returned by {anchorName splitList}`splitList`. Each recursive call will require a proof that the length of the list being passed to it is shorter than the length of the input list. @@ -811,6 +834,9 @@ termination_by n # Exercises +%%% +tag := "inequalities-exercises" +%%% Prove the following theorems without using {tactic}`grind`: diff --git a/book/FPLean/ProgramsProofs/InsertionSort.lean b/book/FPLean/ProgramsProofs/InsertionSort.lean index f174129..3de4dc9 100644 --- a/book/FPLean/ProgramsProofs/InsertionSort.lean +++ b/book/FPLean/ProgramsProofs/InsertionSort.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.ProgramsProofs.InsertionSort" #doc (Manual) "Insertion Sort and Array Mutation" => +%%% +tag := "insertion-sort-mutation" +%%% While insertion sort does not have the optimal worst-case time complexity for a sorting algorithm, it still has a number of useful properties: * It is simple and straightforward to implement and understand @@ -68,6 +71,9 @@ The inner loop takes the element pointed to by the pointer and moves it to the l In other words, each iteration inserts the next element of the array into the appropriate location in the sorted region. # The Inner Loop +%%% +tag := "inner-insertion-sort-loop" +%%% The inner loop of insertion sort can be implemented as a tail-recursive function that takes the array and the index of the element being inserted as arguments. The element being inserted is repeatedly swapped with the element to its left until either the element to the left is smaller or the beginning of the array is reached. @@ -112,6 +118,9 @@ isLt✝ : i' + 1 < arr.size # The Outer Loop +%%% +tag := "outer-insertion-sort-loop" +%%% The outer loop of insertion sort moves the pointer from left to right, invoking {anchorName insertionSortLoop}`insertSorted` at each iteration to insert the element at the pointer into the correct position in the array. The basic form of the loop resembles the implementation of {anchorTerm etc}`Array.map`: @@ -174,6 +183,9 @@ partial def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α := ``` ## Termination +%%% +tag := "insertionSortLoop-termination" +%%% Once again, the function terminates because the difference between the index and the size of the array being processed decreases on each recursive call. This time, however, Lean does not accept the {kw}`termination_by`: @@ -471,6 +483,9 @@ termination_by arr.size - i # The Driver Function +%%% +tag := "insertion-sort-driver-function" +%%% Insertion sort itself calls {anchorName insertionSort}`insertionSortLoop`, initializing the index that demarcates the sorted region of the array from the unsorted region to {anchorTerm insertionSort}`0`: @@ -494,6 +509,10 @@ A few quick tests show the function is at least not blatantly wrong: ``` # Is This Really Insertion Sort? +%%% +tag := "insertion-sort-in-place" +%%% + Insertion sort is _defined_ to be an in-place sorting algorithm. What makes it useful, despite its quadratic worst-case run time, is that it is a stable sorting algorithm that doesn't allocate extra space and that handles almost-sorted data efficiently. @@ -681,6 +700,9 @@ When running {lit}`sort --shared`, the array is copied as needed to preserve the # Other Opportunities for Mutation +%%% +tag := none +%%% The use of mutation instead of copying when references are unique is not limited to array update operators. Lean also attempts to “recycle” constructors whose reference counts are about to fall to zero, reusing them instead of allocating new data. @@ -688,7 +710,11 @@ This means, for instance, that {anchorName names}`List.map` will mutate a linked One of the most important steps in optimizing hot loops in Lean code is making sure that the data being modified is not referred to from multiple locations. # Exercises +%%% +tag := "insertion-sort-exercises" +%%% + * Write a function that reverses arrays. Test that if the input array has a reference count of one, then your function does not allocate a new array. -* Implement either merge sort or quicksort for arrays. Prove that your implementation terminates, and test that it doesn't allocate more arrays than expected. This is a challenging exercise! + * Implement either merge sort or quicksort for arrays. Prove that your implementation terminates, and test that it doesn't allocate more arrays than expected. This is a challenging exercise! diff --git a/book/FPLean/ProgramsProofs/SpecialTypes.lean b/book/FPLean/ProgramsProofs/SpecialTypes.lean index 512167d..e309b30 100644 --- a/book/FPLean/ProgramsProofs/SpecialTypes.lean +++ b/book/FPLean/ProgramsProofs/SpecialTypes.lean @@ -10,6 +10,9 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.SpecialTypes" #doc (Manual) "Special Types" => +%%% +tag := "runtime-special-types" +%%% Understanding the representation of data in memory is very important. Usually, the representation can be understood from the definition of a datatype. @@ -107,6 +110,9 @@ The following types have special representations: # Exercise +%%% +tag := "runtime-special-types-exercise" +%%% The {ref "positive-numbers"}[definition of {anchorName Pos (module := Examples.Classes)}`Pos`] does not take advantage of Lean's compilation of {anchorName all}`Nat` to an efficient type. At run time, it is essentially a linked list. diff --git a/book/FPLean/ProgramsProofs/Summary.lean b/book/FPLean/ProgramsProofs/Summary.lean index 67b6826..9a5f6de 100644 --- a/book/FPLean/ProgramsProofs/Summary.lean +++ b/book/FPLean/ProgramsProofs/Summary.lean @@ -10,8 +10,14 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.ProgramsProofs.InsertionSort" #doc (Manual) "Summary" => +%%% +tag := "programs-proofs-summary" +%%% # Tail Recursion +%%% +tag := none +%%% Tail recursion is recursion in which the results of recursive calls are returned immediately, rather than being used in some other way. These recursive calls are called _tail calls_. @@ -26,6 +32,9 @@ In Lean, only self-tail-calls are optimized into loops. In other words, two functions that each end with a tail call to the other will not be optimized. # Reference Counting and In-Place Updates +%%% +tag := none +%%% Rather than using a tracing garbage collector, as is done in Java, C#, and most JavaScript implementations, Lean uses reference counting for memory management. This means that each value in memory contains a field that tracks how many other values refer to it, and the run-time system maintains these counts as references appear or disappear. @@ -40,6 +49,9 @@ While tail calls can be identified by inspecting the function's definition, unde The debugging helper {anchorName dbgTraceIfSharedSig}`dbgTraceIfShared` can be used at key locations in the program to check that a value is not shared. # Proving Programs Correct +%%% +tag := none +%%% Rewriting a program in accumulator-passing style, or making other transformations that make it run faster, can also make it more difficult to understand. It can be useful to keep the original version of the program that is more clearly correct, and then use it as an executable specification for the optimized version. @@ -53,6 +65,9 @@ Fixing this problem usually requires thought about how to construct a more gener In particular, to prove that a function is equivalent to an accumulator-passing version, a theorem statement that relates arbitrary initial accumulator values to the final result of the original function is needed. # Safe Array Indices +%%% +tag := none +%%% The type {anchorTerm names}`Fin n` represents natural numbers that are strictly less than {anchorName names}`n`. {anchorName names}`Fin` is short for “finite”. @@ -65,6 +80,9 @@ Lean provides instances of most of the useful numeric type classes for {anchorNa The {anchorName names}`OfNat` instances for {anchorName names}`Fin` perform modular arithmetic rather than failing at compile time if the number provided is larger than the {anchorName names}`Fin` can accept. # Provisional Proofs +%%% +tag := none +%%% Sometimes, it can be useful to pretend that a statement is proved without actually doing the work of proving it. This can be useful when making sure that a proof of a statement would be suitable for some task, such as a rewrite in another proof, determining that an array access is safe, or showing that a recursive call is made on a smaller value than the original argument. @@ -80,6 +98,9 @@ Proving that {anchorTerm names}`3 < 2` can cause an out-of-bounds array access t Using {anchorTerm names}`sorry` is convenient during development, but keeping it in the code is dangerous. # Proving Termination +%%% +tag := none +%%% When a recursive function does not use structural recursion, Lean cannot automatically determine that it terminates. In these situations, the function could just be marked {kw}`partial`. diff --git a/book/FPLean/ProgramsProofs/TailRecursion.lean b/book/FPLean/ProgramsProofs/TailRecursion.lean index 79b8599..3e29cef 100644 --- a/book/FPLean/ProgramsProofs/TailRecursion.lean +++ b/book/FPLean/ProgramsProofs/TailRecursion.lean @@ -115,6 +115,9 @@ At each recursive call, the function argument on the stack is simply replaced wi # Tail and Non-Tail Positions +%%% +tag := "tail-positions" +%%% The reason why {anchorName TailSum}`Tail.sumHelper` is tail recursive is that the recursive call is in _tail position_. Informally speaking, a function call is in tail position when the caller does not need to modify the returned value in any way, but will just return it directly. @@ -139,6 +142,9 @@ This means that tail calls to {lit}`f` in {lit}`f`'s definition will be eliminat While it is certainly possible to eliminate a tail call to some other function, saving a stack frame, this is not yet implemented in Lean. # Reversing Lists +%%% +tag := "reversing-lists-tail-recursively" +%%% The function {anchorName NonTailReverse}`NonTail.reverse` reverses lists by appending the head of each sub-list to the end of the result: @@ -201,6 +207,9 @@ Appending lists is not commutative, so care must be taken to find an operation t Appending {anchorTerm NonTailReverse}`[x]` after the result of the recursion in {anchorName NonTailReverse}`NonTail.reverse` is analogous to adding {anchorName NonTailReverse}`x` to the beginning of the list when the result is built in the opposite order. # Multiple Recursive Calls +%%% +tag := "multiple-call-tail-recursion" +%%% In the definition of {anchorName mirrorNew (module := Examples.Monads.Conveniences)}`BinTree.mirror`, there are two recursive calls: @@ -219,6 +228,9 @@ In these cases, the depth of the structure is often logarithmic with respect to There are systematic techniques for making these functions tail-recursive, such as using _continuation-passing style_ and _defunctionalization_, but they are outside the scope of this book. # Exercises +%%% +tag := "tail-recursion-exercises" +%%% Translate each of the following non-tail-recursive functions into accumulator-passing tail-recursive functions: diff --git a/book/FPLean/ProgramsProofs/TailRecursionProofs.lean b/book/FPLean/ProgramsProofs/TailRecursionProofs.lean index 10df91f..0c8523b 100644 --- a/book/FPLean/ProgramsProofs/TailRecursionProofs.lean +++ b/book/FPLean/ProgramsProofs/TailRecursionProofs.lean @@ -10,12 +10,18 @@ set_option verso.exampleProject "../examples" set_option verso.exampleModule "Examples.ProgramsProofs.TCO" #doc (Manual) "Proving Equivalence" => +%%% +tag := "proving-tail-rec-equiv" +%%% Programs that have been rewritten to use tail recursion and an accumulator can look quite different from the original program. The original recursive function is often much easier to understand, but it runs the risk of exhausting the stack at run time. After testing both versions of the program on examples to rule out simple bugs, proofs can be used to show once and for all that the programs are equivalent. # Proving {lit}`sum` Equal +%%% +tag := "proving-sum-equal" +%%% To prove that both versions of {lit}`sum` are equal, begin by writing the theorem statement with a stub proof: ```anchor sumEq0 @@ -187,6 +193,9 @@ The induction hypothesis can be used for {lit}`Tail.sumHelper n ys`, not {lit}`T In other words, this proof is stuck. # A Second Attempt +%%% +tag := "proving-sum-equal-again" +%%% Rather than attempting to muddle through the proof, it's time to take a step back and think. Why is it that the tail-recursive version of the function is equal to the non-tail-recursive version? @@ -473,6 +482,9 @@ For example, in {anchorName nonTailEqRealDone}`non_tail_sum_eq_tail_sum`, the ac This may require rewriting the goal to make the neutral initial accumulator values occur in the right place. # Functional Induction +%%% +tag := "fun-induction" +%%% The proof of {anchorName nonTailEqRealDone}`non_tail_sum_eq_helper_accum` follows the implementation of {anchorName TailSum}`Tail.sumHelper` closely. There is not, however, a perfect match between the implementation and the structure expected by mathematical induction, which makes it necessary to manage the assumption {anchorName nonTailEqHelperDone}`n` carefully. @@ -546,14 +558,26 @@ This proof also matches the way the proof might be explained to a skilled progra ::: # Exercise +%%% +tag := "tail-recursion-proof-exercises" +%%% ## Warming Up +%%% +tag := none +%%% Write your own proofs for {anchorName NatZeroAdd}`Nat.zero_add`, {anchorName NatAddAssoc}`Nat.add_assoc`, and {anchorName NatAddComm}`Nat.add_comm` using the {kw}`induction` tactic. ## More Accumulator Proofs +%%% +tag := none +%%% ### Reversing Lists +%%% +tag := none +%%% Adapt the proof for {anchorName NonTailSum}`sum` into a proof for {anchorName NonTailReverse}`NonTail.reverse` and {anchorName TailReverse}`Tail.reverse`. The first step is to think about the relationship between the accumulator value being passed to {anchorName TailReverse}`Tail.reverseHelper` and the non-tail-recursive reverse. @@ -580,5 +604,9 @@ xs : List α ### Factorial +%%% +tag := none +%%% + Prove that {anchorName NonTailFact}`NonTail.factorial` from the exercises in the previous section is equal to your tail-recursive solution by finding the relationship between the accumulator and the result and proving a suitable helper theorem. diff --git a/book/FPLean/PropsProofsIndexing.lean b/book/FPLean/PropsProofsIndexing.lean index d6bcf73..bf2f5b0 100644 --- a/book/FPLean/PropsProofsIndexing.lean +++ b/book/FPLean/PropsProofsIndexing.lean @@ -56,6 +56,9 @@ Out-of-bounds errors are a common class of bugs, and Lean uses its dual nature a Understanding how this works requires an understanding of three key ideas: propositions, proofs, and tactics. # Propositions and Proofs +%%% +tag := "propositions-and-proofs" +%%% A _proposition_ is a statement that can be true or false. All of the following English sentences are propositions: @@ -139,6 +142,9 @@ theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl # Tactics +%%% +tag := "tactics" +%%% Proofs are normally written using _tactics_, rather than by providing evidence directly. Tactics are small programs that construct evidence for a proposition. @@ -271,6 +277,9 @@ theorem falseImpliesTrue : False → True := by decide # Evidence as Arguments +%%% +tag := "evidence-passing" +%%% In some cases, safely indexing into a list requires that the list have some minimum size, but the list itself is a variable rather than a concrete value. For this lookup to be safe, there must be some evidence that the list is long enough. @@ -314,6 +323,9 @@ In these cases, {anchorTerm thirdCritters}`by decide` can construct the evidence # Indexing Without Evidence +%%% +tag := "indexing-without-evidence" +%%% In cases where it's not practical to prove that an indexing operation is in bounds, there are other alternatives. Adding a question mark results in an {anchorName thirdOption}`Option`, where the result is {anchorName OptionNames}`some` if the index is in bounds, and {anchorName OptionNames}`none` otherwise. @@ -354,6 +366,9 @@ There is also a version that crashes the program when the index is out of bounds # Messages You May Meet +%%% +tag := "props-proofs-indexing-messages" +%%% In addition to proving that a statement is true, the {anchorTerm thirdRabbitErr}`decide` tactic can also prove that it is false. When asked to prove that a one-element list has more than two elements, it returns an error that indicates that the statement is indeed false: @@ -444,6 +459,9 @@ Adding a space causes Lean to treat the expression as a function application, an This error message results from having Lean attempt to treat {anchorTerm woodlandCritters}`woodlandCritters` as a function. ## Exercises +%%% +tag := "props-proofs-indexing-exercises" +%%% * Prove the following theorems using {anchorTerm exercises}`rfl`: {anchorTerm exercises}`2 + 3 = 5`, {anchorTerm exercises}`15 - 8 = 7`, {anchorTerm exercises}`"Hello, ".append "world" = "Hello, world"`. What happens if {anchorTerm exercises}`rfl` is used to prove {anchorTerm exercises}`5 < 18`? Why? * Prove the following theorems using {anchorTerm exercises}`by decide`: {anchorTerm exercises}`2 + 3 = 5`, {anchorTerm exercises}`15 - 8 = 7`, {anchorTerm exercises}`"Hello, ".append "world" = "Hello, world"`, {anchorTerm exercises}`5 < 18`. diff --git a/book/FPLean/TacticsInductionProofs.lean b/book/FPLean/TacticsInductionProofs.lean index 968c206..4fb901f 100644 --- a/book/FPLean/TacticsInductionProofs.lean +++ b/book/FPLean/TacticsInductionProofs.lean @@ -11,11 +11,15 @@ set_option verso.exampleModule "Examples.Induction" #doc (Manual) "Interlude: Tactics, Induction, and Proofs" => %%% +tag := "tactics-induction-proofs" number := false htmlSplit := .never %%% # A Note on Proofs and User Interfaces +%%% +tag := "proofs-and-uis" +%%% This book presents the process of writing proofs as if they are written in one go and submitted to Lean, which then replies with error messages that describe what remains to be done. The actual process of interacting with Lean is much more pleasant. @@ -28,6 +32,9 @@ As your skill in writing proofs increases, Lean's feedback will come to feel les Learning the interactive approach is very important. # Recursion and Induction +%%% +tag := "recursion-vs-induction" +%%% The functions {anchorName plusR_succ_left (module := Examples.DependentTypes.Pitfalls)}`plusR_succ_left` and {anchorName plusR_zero_left_thm (module:=Examples.DependentTypes.Pitfalls)}`plusR_zero_left` from the preceding chapter can be seen from two perspectives. On the one hand, they are recursive functions that build up evidence for a proposition, just as other recursive functions might construct a list, a string, or any other data structure. @@ -42,6 +49,9 @@ For example, if a concrete proof were desired for the number 3, then it could be Thus, it proves the statement for all natural numbers. # The Induction Tactic +%%% +tag := "induction-tactic" +%%% Writing proofs by induction as recursive functions that use helpers such as {anchorName plusR_zero_left_done (module:=Examples.DependentTypes.Pitfalls)}`congrArg` does not always do a good job of expressing the intentions behind the proof. While recursive functions indeed have the structure of induction, they should probably be viewed as an _encoding_ of a proof. @@ -182,6 +192,9 @@ This rewrite makes both sides of the equation identical, and Lean takes care of The proof is complete. # Tactic Golf +%%% +tag := "tactic-golf" +%%% So far, the tactic language has not shown its true value. The above proof is no shorter than the recursive function; it's merely written in a domain-specific language instead of the full Lean language. @@ -300,6 +313,9 @@ Additionally, these proofs tend to be more robust in the face of small changes t The game of tactic golf is a useful part of developing good taste and style when writing proofs. # Induction on Other Datatypes +%%% +tag := "induction-other-types" +%%% Mathematical induction proves a statement for natural numbers by providing a base case for {anchorName others}`Nat.zero` and an induction step for {anchorName others}`Nat.succ`. The principle of induction is also valid for other datatypes. @@ -449,6 +465,9 @@ theorem BinTree.mirror_count (t : BinTree α) : ``` # The {lit}`grind` Tactic +%%% +tag := "grind" +%%% The {tactic}`grind` tactic can automatically prove many theorems. Like {tactic}`simp`, it accepts an optional list of additional facts to take into consideration or functions to unfold; unlike {tactic}`simp`, it automatically takes local hypotheses into consideration. @@ -464,6 +483,9 @@ Because the proofs in this book are fairly modest, most of them do not provide a However, it is very convenient in some of the later proofs in the book. # Exercises +%%% +tag := "tactics-induction-proofs-exercises" +%%% * Prove {anchorName plusR_succ_left (module:=Examples.DependentTypes.Pitfalls)}`plusR_succ_left` using the {kw}`induction`{lit}` ...`{kw}`with` tactic. * Rewrite the proof of {anchorName plusR_succ_left (module:=Examples.DependentTypes.Pitfalls)}`plusR_succ_left` to use {kw}`<;>` in a single line. diff --git a/book/FPLean/TypeClasses/Coercions.lean b/book/FPLean/TypeClasses/Coercions.lean index e0f26be..892c8c8 100644 --- a/book/FPLean/TypeClasses/Coercions.lean +++ b/book/FPLean/TypeClasses/Coercions.lean @@ -12,6 +12,9 @@ set_option verso.exampleModule "Examples.Classes" set_option pp.rawOnError true #doc (Manual) "Coercions" => +%%% +tag := "coercions" +%%% In mathematics, it is common to use the same symbol to stand for different aspects of some object in different contexts. @@ -24,6 +27,9 @@ When Lean encounters an expression of one type in a context that expects a diffe Unlike Java, C, and Kotlin, the coercions are extensible by defining instances of type classes. # Strings and Paths +%%% +tag := "string-path-coercion" +%%% In the {ref "handling-input"}[source code to {lit}`feline`], a {moduleName}`String` is converted to a {moduleName}`FilePath` using the anonymous constructor syntax. In fact, this was not necessary: Lean defines a coercion from {moduleName}`String` to {moduleName}`FilePath`, so a string can be used in an position where a path is expected. @@ -43,6 +49,9 @@ def fileDumper : IO Unit := do On the last line of {anchorName fileDumper}`fileDumper`, the coercion from {moduleName}`String` to {moduleName}`FilePath` automatically converts {anchorName fileDumper}`f`, so it is not necessary to write {lit}`IO.FS.readFile ⟨f⟩`. # Positive Numbers +%%% +tag := "positive-number-coercion" +%%% Every positive number corresponds to a natural number. The function {anchorName posToNat}`Pos.toNat` that was defined earlier converts a {moduleName}`Pos` to the corresponding {moduleName}`Nat`: @@ -98,6 +107,9 @@ List.drop (Pos.toNat 2) [1, 2, 3, 4] : List Nat ::: # Chaining Coercions +%%% +tag := "chaining-coercions" +%%% When searching for coercions, Lean will attempt to assemble a coercion out of a chain of smaller coercions. For example, there is already a coercion from {anchorName chapterIntro}`Nat` to {anchorName chapterIntro}`Int`. @@ -197,6 +209,9 @@ It can also make the programmer's intentions more clear. ::: # Non-Empty Lists and Dependent Coercions +%%% +tag := "CoeDep" +%%% An instance of {anchorTerm chapterIntro}`Coe α β` makes sense when the type {anchorName chapterIntro}`β` has a value that can represent each value from the type {anchorName chapterIntro}`α`. Coercing from {moduleName}`Nat` to {moduleName}`Int` makes sense, because the type {moduleName}`Int` contains all the natural numbers, but a coercion from {moduleName}`Int` to {moduleName}`Nat` is a poor idea because {moduleName}`Nat` does not contain the negative numbers. @@ -227,6 +242,9 @@ instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where ``` # Coercing to Types +%%% +tag := "CoeSort" +%%% In mathematics, it is common to have a concept that consists of a set equipped with additional structure. For example, a monoid is some set $`S`, an element $`s` of $`S`, and an associative binary operator on $`S`, such that $`s` is neutral on the left and right of the operator. @@ -300,6 +318,9 @@ instance : CoeSort Bool Prop where In this case, the sort in question is {anchorTerm chapterIntro}`Prop` rather than {anchorTerm chapterIntro}`Type`. # Coercing to Functions +%%% +tag := "CoeFun" +%%% Many datatypes that occur regularly in programming consist of a function along with some extra information about it. For example, a function might be accompanied by a name to show in logs or by some configuration data. @@ -417,6 +438,9 @@ JSON.object ::: ## Aside: JSON as a String +%%% +tag := "json-string" +%%% It can be a bit difficult to understand JSON when encoded as Lean objects. To help make sure that the serialized response was what was expected, it can be convenient to write a simple converter from {anchorName JSON}`JSON` to {anchorName dropDecimals}`String`. @@ -485,6 +509,9 @@ With this definition, the output of serialization is easier to read: # Messages You May Meet +%%% +tag := "coercion-messages" +%%% Natural number literals are overloaded with the {anchorName OfNat}`OfNat` type class. Because coercions fire in cases where types don't match, rather than in cases of missing instances, a missing {anchorName OfNat}`OfNat` instance for a type does not cause a coercion from {moduleName}`Nat` to be applied: @@ -503,6 +530,9 @@ Hint: Additional diagnostic information may be available using the `set_option d ``` # Design Considerations +%%% +tag := "coercion-design-considerations" +%%% Coercions are a powerful tool that should be used responsibly. On the one hand, they can allow an API to naturally follow the everyday rules of the domain being modeled. diff --git a/book/FPLean/TypeClasses/Conveniences.lean b/book/FPLean/TypeClasses/Conveniences.lean index f7fafff..ff39468 100644 --- a/book/FPLean/TypeClasses/Conveniences.lean +++ b/book/FPLean/TypeClasses/Conveniences.lean @@ -13,9 +13,14 @@ set_option pp.rawOnError true #doc (Manual) "Additional Conveniences" => - +%%% +tag := "type-class-conveniences" +%%% # Constructor Syntax for Instances +%%% +tag := "instance-constructor-syntax" +%%% Behind the scenes, type classes are structure types and instances are values of these types. The only differences are that Lean stores additional information about type classes, such as which parameters are output parameters, and that instances are registered for searching. @@ -69,6 +74,9 @@ Placing a call to this function after {lit}`:=` in an instance declaration is th ::: # Examples +%%% +tag := "example-command" +%%% When experimenting with Lean code, definitions can be more convenient to use than {kw}`#eval` or {kw}`#check` commands. First off, definitions don't produce any output, which can help keep the reader's focus on the most interesting output. diff --git a/book/FPLean/TypeClasses/Indexing.lean b/book/FPLean/TypeClasses/Indexing.lean index 2798dff..833f0f4 100644 --- a/book/FPLean/TypeClasses/Indexing.lean +++ b/book/FPLean/TypeClasses/Indexing.lean @@ -18,6 +18,10 @@ The {ref "props-proofs-indexing"}[Interlude] describes how to use indexing notat This syntax is also governed by a type class, and it can be used for a variety of different types. # Arrays +%%% +tag := "array-indexing" +%%% + For instance, Lean arrays are much more efficient than linked lists for most purposes. In Lean, the type {anchorTerm arrVsList}`Array α` is a dynamically-sized array holding values of type {anchorName arrVsList}`α`, much like a Java {java}`ArrayList`, a C++ {cpp}`std::vector`, or a Rust {rust}`Vec`. Unlike {anchorTerm arrVsList}`List`, which has a pointer indirection on each use of the {anchorName arrVsList}`cons` constructor, arrays occupy a contiguous region of memory, which is much better for processor caches. @@ -49,6 +53,9 @@ failed to prove index is valid, possible solutions: ``` # Non-Empty Lists +%%% +tag := "non-empty-list-indexing" +%%% A datatype that represents non-empty lists can be defined as a structure with a field for the head of the list and a field for the tail, which is an ordinary, potentially empty list: diff --git a/book/FPLean/TypeClasses/OutParams.lean b/book/FPLean/TypeClasses/OutParams.lean index 2fc6a97..9bff7a7 100644 --- a/book/FPLean/TypeClasses/OutParams.lean +++ b/book/FPLean/TypeClasses/OutParams.lean @@ -32,6 +32,9 @@ def addPosNat : Pos → Nat → Pos These functions allow natural numbers to be added to positive numbers, but they cannot be used with the {moduleName}`Add` type class, which expects both arguments to {moduleName}`add` to have the same type. # Heterogeneous Overloadings +%%% +tag := "heterogeneous-operators" +%%% As mentioned in the section on {ref "overloaded-addition"}[overloaded addition], Lean provides a type class called {anchorName chapterIntro}`HAdd` for overloading addition heterogeneously. The {anchorName chapterIntro}`HAdd` class takes three type parameters: the two argument types and the return type. @@ -102,6 +105,9 @@ However, this solution is not very convenient for users of the positive number l # Output Parameters +%%% +tag := "output-parameters" +%%% This problem can also be solved by declaring {anchorName HPlus}`γ` to be an _output parameter_. Most type class parameters are inputs to the search algorithm: they are used to select an instance. @@ -129,6 +135,9 @@ The process of searching for an instance, possibly recursively, ends up being mo Output parameters can determine other types in the program, and instance search can assemble a collection of underlying instances into a program that has this type. # Default Instances +%%% +tag := "default-instances" +%%% Deciding whether a parameter is an input or an output controls the circumstances under which Lean will initiate type class search. In particular, type class search does not occur until all inputs are known. @@ -204,6 +213,9 @@ For more information on default instance priorities, please consult the Lean man # Exercises +%%% +tag := "out-params-exercises" +%%% Define an instance of {anchorTerm MulPPoint}`HMul (PPoint α) α (PPoint α)` that multiplies both projections by the scalar. It should work for any type {anchorName MulPPoint}`α` for which there is a {anchorTerm MulPPoint}`Mul α` instance. diff --git a/book/FPLean/TypeClasses/Polymorphism.lean b/book/FPLean/TypeClasses/Polymorphism.lean index 482fac2..eb93b48 100644 --- a/book/FPLean/TypeClasses/Polymorphism.lean +++ b/book/FPLean/TypeClasses/Polymorphism.lean @@ -26,6 +26,9 @@ It returns an {anchorTerm printlnType}`IO` action. # Checking Polymorphic Functions' Types +%%% +tag := "checking-polymorphic-types" +%%% Checking the type of a function that takes implicit arguments or uses type classes requires the use of some additional syntax. Simply writing @@ -48,6 +51,9 @@ There is a {lit}`u_1` after {lit}`Type`, which uses a feature of Lean that has n For now, ignore these parameters to {lit}`Type`. # Defining Polymorphic Functions with Instance Implicits +%%% +tag := "defining-polymorphic-functions-with-instance-implicits" +%%% :::paragraph A function that sums all entries in a list needs two instances: {moduleName}`Add` allows the entries to be added, and an {moduleName}`OfNat` instance for {anchorTerm ListSum}`0` provides a sensible value to return for the empty list: @@ -137,7 +143,9 @@ The API's clients are freed from the burden of plumbing together all of the nece # Methods and Implicit Arguments - +%%% +tag := "method-implicit-params" +%%% The type of {anchorTerm ofNatType}`OfNat.ofNat` may be surprising. It is {anchorTerm ofNatType}`: {α : Type} → (n : Nat) → [OfNat α n] → α`, in which the {anchorTerm ofNatType}`Nat` argument {anchorTerm ofNatType}`n` occurs as an explicit function parameter. @@ -166,12 +174,22 @@ Thus, in these cases, Lean uses an explicit parameter for the class's method. # Exercises +%%% +tag := "type-class-polymorphism-exercises" +%%% ## Even Number Literals +%%% +tag := none +%%% + Write an instance of {anchorName ofNatType}`OfNat` for the even number datatype from the {ref "even-numbers-ex"}[previous section's exercises] that uses recursive instance search. ## Recursive Instance Search Depth +%%% +tag := none +%%% There is a limit to how many times the Lean compiler will attempt a recursive instance search. This places a limit on the size of even number literals defined in the previous exercise. diff --git a/book/FPLean/TypeClasses/Pos.lean b/book/FPLean/TypeClasses/Pos.lean index adaecd1..fb85b70 100644 --- a/book/FPLean/TypeClasses/Pos.lean +++ b/book/FPLean/TypeClasses/Pos.lean @@ -71,6 +71,9 @@ Each of these error messages begins with {lit}`failed to synthesize`. This indicates that the error is due to an overloaded operation that has not been implemented, and it describes the type class that must be implemented. # Classes and Instances +%%% +tag := "classes-and-instances" +%%% A type class consists of a name, some parameters, and a collection of {deftech}_methods_. The parameters describe the types for which overloadable operations are being defined, and the methods are the names and type signatures of the overloadable operations. @@ -176,6 +179,9 @@ def fourteen : Pos := seven + seven ``` # Conversion to Strings +%%% +tag := "conversion-to-strings" +%%% Another useful built-in class is called {anchorName UglyToStringPos}`ToString`. Instances of {anchorName UglyToStringPos}`ToString` provide a standard way of converting values from a given type into strings. @@ -227,6 +233,9 @@ When more than one instance is defined, the most recent takes precedence. Additionally, if a type has a {anchorName UglyToStringPos}`ToString` instance, then it can be used to display the result of {kw}`#eval` so {anchorTerm sevenEvalStr}`#eval seven` outputs {anchorInfo sevenEvalStr}`7`. # Overloaded Multiplication +%%% +tag := "overloaded-multiplication" +%%% For multiplication, there is a type class called {anchorName MulPPoint}`HMul` that allows mixed argument types, just like {anchorName chapterIntro}`HAdd`. Just as {anchorTerm plusDesugar}`x + y` is interpreted as {anchorTerm plusDesugar}[`HAdd.hAdd x y`], {anchorTerm timesDesugar}`x * y` is interpreted as {anchorTerm timesDesugar}`HMul.hMul x y`. @@ -394,8 +403,14 @@ Hint: Additional diagnostic information may be available using the `set_option d ``` # Exercises +%%% +tag := "positive-numbers-exercises" +%%% ## Another Representation +%%% +tag := "positive-numbers-another-representation" +%%% An alternative way to represent a positive number is as the successor of some {anchorTerm chapterIntro}`Nat`. Replace the definition of {anchorName PosStuff}`Pos` with a structure whose constructor is named {anchorName AltPos}`succ` that contains a {anchorTerm chapterIntro}`Nat`: @@ -416,6 +431,9 @@ Define a datatype that represents only even numbers. Define instances of {module {moduleName}`OfNat` requires a feature that is introduced in {ref "tc-polymorphism"}[the next section]. ## HTTP Requests +%%% +tag := "http-request-ex" +%%% An HTTP request begins with an identification of a HTTP method, such as {lit}`GET` or {lit}`POST`, along with a URI and an HTTP version. Define an inductive type that represents an interesting subset of the HTTP methods, and a structure that represents HTTP responses. diff --git a/book/FPLean/TypeClasses/StandardClasses.lean b/book/FPLean/TypeClasses/StandardClasses.lean index f81b0b9..83fa44f 100644 --- a/book/FPLean/TypeClasses/StandardClasses.lean +++ b/book/FPLean/TypeClasses/StandardClasses.lean @@ -12,6 +12,9 @@ set_option verso.exampleModule "Examples.Classes" set_option pp.rawOnError true #doc (Manual) "Standard Classes" => +%%% +tag := "standard-classes" +%%% This section presents a variety of operators and functions that can be overloaded using type classes in Lean. @@ -19,6 +22,9 @@ Each operator or function corresponds to a method of a type class. Unlike C++, infix operators in Lean are defined as abbreviations for named functions; this means that overloading them for new types is not done using the operator itself, but rather using the underlying name (such as {moduleName}`HAdd.hAdd`). # Arithmetic +%%% +tag := "arithmetic-classes" +%%% Most arithmetic operators are available in a heterogeneous form, where the arguments may have different type and an output parameter decides the type of the resulting expression. For each heterogeneous operator, there is a corresponding homogeneous version that can found by removing the letter {lit}`h`, so that {moduleName}`HAdd.hAdd` becomes {moduleName}`Add.add`. @@ -63,6 +69,9 @@ The following arithmetic operators are overloaded: ::: # Bitwise Operators +%%% +tag := "bitwise-classes" +%%% Lean contains a number of standard bitwise operators that are overloaded using type classes. There are instances for fixed-width types such as {anchorTerm UInt8}`UInt8`, {anchorTerm UInt16}`UInt16`, {anchorTerm UInt32}`UInt32`, {anchorTerm UInt64}`UInt64`, and {anchorTerm USize}`USize`. @@ -257,6 +266,9 @@ In situations where {java}`compareTo` would be the right approach in Java, use { ::: # Hashing +%%% +tag := "hashing" +%%% Java and C# have {java}`hashCode` and {CSharp}`GetHashCode` methods, respectively, that compute a hash of a value for use in data structures such as hash tables. The Lean equivalent is a type class called {anchorName Hashable}`Hashable`: @@ -325,6 +337,9 @@ instance [Hashable α] : Hashable (BinTree α) where ::: # Deriving Standard Classes +%%% +tag := "deriving-standard-classes" +%%% Instance of classes like {moduleName}`BEq` and {moduleName}`Hashable` are often quite tedious to implement by hand. Lean includes a feature called _instance deriving_ that allows the compiler to automatically construct well-behaved instances of many type classes. @@ -359,6 +374,9 @@ Aside from the clear advantages in programmer productivity and code readability, When reviewing changes to code, modifications that involve updates to datatypes are much easier to read without line after line of formulaic modifications to equality tests and hash computation. # Appending +%%% +tag := "append-class" +%%% Many datatypes have some sort of append operator. In Lean, appending two values is overloaded with the type class {anchorName HAppend}`HAppend`, which is a heterogeneous operation like that used for arithmetic operations: @@ -412,6 +430,9 @@ results in ``` # Functors +%%% +tag := "Functor" +%%% A polymorphic type is a {deftech}_functor_ if it has an overload for a function named {anchorName FunctorDef}`map` that transforms every element contained in it by a function. While most languages use this terminology, C#'s equivalent of {anchorName FunctorDef}`map` is called {CSharp}`System.Linq.Enumerable.Select`. @@ -496,6 +517,9 @@ The composition {anchorTerm compDef}`f ∘ g` can also be written {anchorTerm co These rules prevent implementations of {anchorName FunctorDef}`map` that move the data around or delete some of it. # Messages You May Meet +%%% +tag := "standard-classes-messages" +%%% Lean is not able to derive instances for all classes. For example, the code @@ -511,6 +535,9 @@ If the code generator is found, then it is invoked on the provided type to creat This message, however, means that no code generator was found for {anchorName derivingNotFound}`ToString`. # Exercises +%%% +tag := "standard-classes-exercises" +%%% * Write an instance of {anchorTerm moreOps}`HAppend (List α) (NonEmptyList α) (NonEmptyList α)` and test it. * Implement a {anchorTerm FunctorLaws}`Functor` instance for the binary tree datatype. diff --git a/book/FPLean/TypeClasses/Summary.lean b/book/FPLean/TypeClasses/Summary.lean index 8ba5f43..a07beee 100644 --- a/book/FPLean/TypeClasses/Summary.lean +++ b/book/FPLean/TypeClasses/Summary.lean @@ -13,8 +13,14 @@ set_option verso.exampleModule "Examples.Classes" set_option pp.rawOnError true #doc (Manual) "Summary" => +%%% +tag :="type-classes-summary" +%%% # Type Classes and Overloading +%%% +tag := none +%%% Type classes are Lean's mechanism for overloading functions and operators. A polymorphic function can be used with multiple types, but it behaves in the same manner no matter which type it is used with. @@ -40,6 +46,9 @@ Instances may be marked with a {anchorTerm defaultAdd}`@[default_instance]` attr When an instance is a default instance, then it will be chosen as a fallback when Lean would otherwise fail to find an instance due to the presence of metavariables in the type. # Type Classes for Common Syntax +%%% +tag := none +%%% Most infix operators in Lean are overridden with a type class. For instance, the addition operator corresponds to a type class called {moduleName}`Add`. @@ -52,6 +61,10 @@ This evidence is described by a proposition, and Lean attempts to prove this pro When Lean is unable to check that list or array access operations are in bounds at compile time, the check can be deferred to run time by appending a {lit}`?` to the indexing syntax. # Functors +%%% +tag := none +%%% + A functor is a polymorphic type that supports a mapping operation. This mapping operation transforms all elements “in place”, changing no other structure. @@ -61,6 +74,10 @@ While functors are defined by having {anchorName FunctorDef}`map`, the {anchorNa For some functors, this can be done more efficiently than traversing the entire structure. # Deriving Instances +%%% +tag := none +%%% + Many type classes have very standard implementations. For instance, the Boolean equality class {moduleName}`BEq` is usually implemented by first checking whether both arguments are built with the same constructor, and then checking whether all their arguments are equal. @@ -71,6 +88,10 @@ Additionally, the {kw}`deriving instance`{lit}` ... `{kw}`for`{lit}`  Because each class for which instances can be derived requires special handling, not all classes are derivable. # Coercions +%%% +tag := none +%%% + Coercions allow Lean to recover from what would normally be a compile-time error by inserting a call to a function that transforms data from one type to another. For example, the coercion from any type {anchorName CoeOption}`α` to the type {anchorTerm CoeOption}`Option α` allows values to be written directly, rather than with the {anchorName CoeOption}`some` constructor, making {anchorName CoeOption}`Option` work more like nullable types from object-oriented languages. diff --git a/book/lakefile.lean b/book/lakefile.lean index 81ec4a8..8b0c898 100644 --- a/book/lakefile.lean +++ b/book/lakefile.lean @@ -6,6 +6,7 @@ package book where version := v!"0.1.0" leanOptions := #[⟨`weak.verso.examples.suggest, true⟩, + ⟨`weak.linter.verso.manual.headerTags, true⟩, ⟨`weak.verso.externalExamples.suppressedNamespaces, "A Adding Agh Argh Almost Alt AltPos AndDef AndThen AppendOverloads ApplicativeOptionLaws ApplicativeOptionLaws2 ApplicativeToFunctor Apply Argh AutoImpl B BadUnzip BetterHPlus BetterPlicity Blurble Both Busted C CheckFunctorPair Class Cls Cmp Connectives Cont Ctor D Decide Demo Desugared Details DirTree DirTree.Old DirTree.Readerish DirTree.T Double EEE EarlyReturn Eff Errs Eta Evaluator Even Ex Exercises Explicit ExplicitParens Extra Extras F F1 F2 Fake FakeAlternative FakeCoe FakeExcept FakeFunctor FakeMonad FakeOrElse FakeSeqRight FancyDo FastPos FinDef Finny Fixity Floop ForMIO Foo Foo2 Four FourPointFive Golf Golf' Guard H HelloName1 HelloName2 HelloName3 Huh IdentMonad Impl Improved Inductive Inflexible IterSub L Lawful ListExtras Loops Loops.Cont M MMM Main1 Main2 Main3 Match MatchDef Mine Modify MonadApplicative MonadApplicativeDesugar MonadApplicativeProof1 MonadApplicativeProof2 MonadApplicativeProof3 MonadApplicativeProof4 MonadLaws Monadicish Monads.Err Monads.Option Monads.State Monads.Writer More MoreClear MoreMonadic Mut MyList1 MyList15 MyList3 MyListStuff MyMonadExcept MyMonadLift MySum NRT NT NatLits Nested New NoTac Non Numbering Numbering.Short Old One OneAttempt Oooops Ooops Oops Opt Option OrElse Orders Original Other OverloadedBits OverloadedInt OwnInstances Partial PipelineEx PointStuff ProblematicHPlus Prod Proofs PropStuff Provisional Provisional2 R Ranges Readerish ReallyNoTypes Reorder SameDo SeqCounterexample SeqLeftSugar SeqRightSugar Ser Short St StEx StdLibNoUni Str StructNotation Structed SubtypeDemo SugaryOrElse Sum T TTT Tactical TailRec Temp ThenDoUnless Three Transformed Two U Up UseList VariousTypes Verbose Wak Whatevs WithAndThen WithDo WithFor WithInfix WithMatch WithPattern"⟩]