Functional Programming In Lean (Christiansen)

leanprover.github.io/functional_programming_in_lean/title.html

101 flashcards · Mathematics · by lakesare

What does it mean that Lean is: functional VS with dependent types?
functional - treats functions as 1st class citizens dependent types - treats types as 1st class citizens
In unix: make In Lean: ___________?
Lake
What does LSP stand for?
Language Server Protocol The Language Server Protocol (LSP) is an open protocol for use between source code editors/IDEs.
What is Language Server Protocol (LSP) for in Lean?
For Lean ↔ IDE communication. The Language Server Protocol (LSP) is an open protocol for use between source code editors/IDEs.
How do you write if-else in Lean?
if _______ then _______ else _______
What is Lean saying in this "has type String → String" error message?
#eval complains it can't show us a function.
What's the default type of integer literals in Lean?
ℕ
Name 2 ways to create a variable "hi" in Lean.
def hi := 5 (without type) def hi : ℕ := 5 (with type) In the definition of hi, 5 is simple enough that Lean is able to determine the definition's type automatically. However, most definitions are not so simple, so it will usually be necessary to add a type. This is done using a colon after the name being defined.
How do we define all variables (functions, variables, etc.) in Lean?
With def. In many languages, definitions of functions use a different syntax than definitions of other values. For instance, Python function definitions begin with the def keyword, while other definitions are defined with an equals sign. In Lean, functions are defined using the same def keyword as other values.
[Structures] What is this syntax for in Lean?
For initializing a structure. Structures exist to "bundle up" a collection of data, naming it and treating it as a single unit.
[Structures] What is "deriving Repr" for?
Generates code for displaying our structure in #eval.
[Structures] How would you fix "invalid {...} notation" error for structures?
As usual, the situation can be remedied by providing a type annotation. To make programs more concise, Lean also allows the structure type annotation inside the curly braces.
[Structures] How would we write it more concisely? Lean only has immutable structures, so we can't just do p.x = 0.
Lengthy syntax has drawbacks. First off, if a new field is added to a structure, then every site that updates any field at all must be updated, causing maintenance difficulties. Secondly, if the structure contains multiple fields with the same type, then there is a real risk of copy-paste coding leading to field contents being duplicated or switched. Finally, the program becomes long and bureaucratic.Lean provides a convenient syntax for replacing some fields in a structure while leaving the ot…
[Structures] What's the alternative way to create a Point?
Point.mk 4 5 By default, the constructor for a structure named S is named S.mk. Here, S is a namespace qualifier, and mk is the name of the constructor itself. Every structure has a constructor. Here, the term "constructor" may be a source of confusion. Unlike constructors in languages such as Java or Python, constructors in Lean are not arbitrary code to be run when a datatype is initialized. Instead, constructors simply gather the data to be stored in the newly-allocated data structure. It is…
[Structures] What's hi::?
It's the constructor name (changed from mk:: to hi::)
[Inductive datatypes] What are: sum datatypes VS recursive datatypes?
sum datatypes - allow choices recursive datatypes - can include instances of themselves Datatypes that allow choices are called sum types and datatypes that can include instances of themselves are called recursive datatypes.
[Inductive datatypes] Why are 1. sum 2. recursive types called inductive? Datatypes that allow choices are called sum types and datatypes that can include instances of themselves are called recursive datatypes.
Because we can use mathematical induction to prove statements about them. Recursive sum types are called inductive datatypes, because mathematical induction may be used to prove statements about them.
[Inductive datatypes] What 2 types do inductive types consist of?
sum datatypes - allow choices recursive datatypes - can include instances of themselves Makes sense, induction = recursion + sum (base case)! Datatypes that allow choices are called sum types and datatypes that can include instances of themselves are called recursive datatypes.
[Inductive datatypes] What are these? Many of the built-in types are actually inductive datatypes in the standard library. For instance, Bool is an inductive datatype.
| false : Bool constructor, and | true : Bool constructor. Unlike structures, inductive datatypes may have multiple constructors. Here, there are two constructors, true and false, and neither takes any arguments. Just as a structure declaration places its names in a namespace named after the declared type, an inductive datatype places the names of its constructors in a namespace. In the Lean standard library, true and false are re-exported from this namespace so that they can be written alone,…
[Inductive datatypes] Visually imagine the Nat inductive datatype. Bool inductive datatype.
Here, zero represents 0, while succ represents the successor of some other number. The Nat mentioned in succ's declaration is the very type Nat that is in the process of being defined. Successor means "one greater than", so the successor of five is six and the successor of 32,185 is 32,186. Using this definition, 4 is represented as Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))). This definition is almost like the definition of Bool with slightly different names. The only real difference is…
[Inductive datatypes] What does match do?
if n was constructed by Nat.zero - return true if n was constructed by Nat.succ - return false The match expression is provided the function's argument n for destructuring. If n was constructed by Nat.zero, then the first branch of the pattern match is taken, and the result is true. If n was constructed by Nat.succ, then the second branch is taken, and the result is false.
[Inductive datatypes] How to create 0?
[Inductive datatypes] How to create 2?
What could List Nat mean?
A list of natural numbers type. Lean uses a space to:- pass an argument to a function,- to pass an argument to a type.
What does "polymorphism" mean: in functional languages VS in object-oriented languages.
in functional languages - taking types as arguments. In functional programming, the term polymorphism typically refers to datatypes and definitions that take types as arguments.in object-oriented languages - taking arguments of different types. This is different from the object-oriented programming community, where the term typically refers to subclasses that may override some behavior of their superclass.
[Inductive datatypes] What arguments does List.cons accept?
List.cons(head_el, remainder_of_the_list) cons stands for constructor.The first argument to cons is the head of the list, and the second argument is its tail. //=> [3, 5, 7]
[Inductive datatypes] What's the data type of this?
List Nat Alternative way to write it.
[Inductive datatypes] Visually imagine: inductive datatype VS function that works with inductive datatypes.
inductive datatype function that works with inductive datatypes Generally, functions follow the shape of the data: recursive datatypes lead to recursive functions, and polymorphic datatypes lead to polymorphic functions.
[Notation] What do xs conventionally denote?
List of unknowns values, "exes". Names such as xs and ys are conventionally used to stand for lists of unknown values. The s in the name indicates that they are plural, so they are pronounced "exes" and "whys" rather than "x s" and "y s".
[Notation] What do these conventionally denote in Lean? ? ! D
? - return an Option A Lean naming convention is to define operations that might fail in groups using the suffixes ? for a version that returns an Option! - raise an exception ! for a version that crashes when provided with invalid input,D - return default value D for a version that returns a default value when the operation would otherwise fail. For instance, head requires the caller to provide mathematical evidence that the list is not empty, head? returns an Option, head! crashes the program…
[Inductive datatypes] What's the data type of these: ("five", 5) [2, 3, 5, 7]
("five", 5) - Prod String Int [2, 3, 5, 7] - List Nat
I stopped at The Prod structure, short for "Product",
[Inductive datatypes] What is the analogy of datatype: prod String Int String × Intsum String Int String ⊕ Int
prod String Int - both, a tuple (logical AND) The Prod structure, short for "Product", is a generic way of joining two values together. For instance, a Prod Nat String contains a Nat and a String.sum String Int - either or (logical OR) The Sum datatype is a generic way of allowing a choice between values of two different types. For instance, a Sum String Int is either a String or an Int.
[Inductive datatypes] What's the difference between: Unit data type VS Empty data type?
Unit - has 1 argumentless constructor Unit is a type with just one argumentless constructor, called unit. In other words, it describes only a single value, which consists of said constructor applied to no arguments whatsoever.Empty - has 0 constructors The Empty datatype has no constructors whatsoever. Thus, it indicates unreachable code, because no series of calls can ever terminate with a value at type Empty.
[Inductive datatypes] What is this a shortcut for?
For the implicit argument { α : Type }. When writing polymorphic functions in Lean, it is typically not necessary to list all the implicit arguments. Instead, they can simply be mentioned. If Lean can determine their type, then they are automatically inserted as implicit arguments.
[Inductive datatypes] What's the purpose of using let here?
To avoid calculating unzip twice. However, both recursive calls will have the same result, so there is no reason to make the recursive call twice.In Lean, the result of the recursive call can be named, and thus saved, using let. Local definitions with let resemble top-level definitions with def: it takes a name to be locally defined, arguments if desired, a type signature, and then a body following :=. After the local definition, the expression in which the local definition is available (called…
What are these ?m.xxxxx called?
metavariables - a part of the program that could not be inferred In Lean's output, ?m.XYZ represents a part of a program that could not be inferred. These unknown parts are called metavariables, and they occur in some error messages. In order to evaluate an expression, Lean needs to be able to find its type, and the type was unavailable because the empty list does not have any entries from which the type can be found. In general, messages that say something like "failed to infer" or that mentio…
What's a wordier way to write this?
Names can be directly defined within a namespace. For instance, the name double can be defined in the Nat namespace. Because Nat is also the name of a type, dot notation is available to call Nat.double on expressions with type Nat: #eval (4 : Nat).double.
[Notation] What could ⟨1, 2⟩ denote?
A structure. In some contexts, it can be convenient to pass arguments positionally, rather than by name, but without naming the constructor directly. For instance, defining a variety of similar structure types can help keep domain concepts separate, but the natural way to read the code may treat each of them as being essentially a tuple. In these contexts, the arguments can be enclosed in angle brackets ⟨ and ⟩. A Point can be written ⟨1, 2⟩. => { x := 1.000000, y := 2.000000 }
[Notation] How to interpolate strings in Lean? Python: f'hello {2 + 2}' Javascript: `hello ${2 + 2}`
s!"hello {2 + 2}" => "three fives is 15"
What would be the 2 elements of a classic "Hello World" in Lean?
def main : IO Unit := IO.println "Hello, world!" The simplest way to run a Lean program is to use the --run option to the Lean executable. Create a file called Hello.lean and enter the following contents:lean --run Hello.lean Then, from the command line, run this. When Lean is invoked with the --run option, it invokes the program's main definition. In programs that do not take command-line arguments, main should have type IO Unit. This means that main is not a function, because there are no arr…
What does RTS stand for?
Run-Time System
[Notation] What's the analogy for the do block?
do models imperative programs. Just as SQL can be thought of as a special-purpose language for interacting with databases, the do syntax can be thought of as a special-purpose sub-language within Lean that is dedicated to modeling imperative programs. IO actions that are built with a do block are executed by executing the statements in order. To enable programs to use multiple effects, there is a sub-language of Lean called do notation that allows these primitive IO actions to be safely compose…
[Notation] What's the difference in scope of let: in a do block in an usual expression?
in a do block - ENTIRE do block scope in an usual expression - just the next line scope In a do block, let has a slightly different meaning than in an ordinary expression. Ordinarily, the local definition in a let can be used in just one expression, which immediately follows the local definition. In a do block, local bindings introduced by let are available in all statements in the remainder of the do block, rather than just the next one. When an if expression occurs as a statement in a do, as…
[Notation] What's the difference: let := __________ VS let ← __________?
let := ordinary value The definition of name uses :=, rather than ←, because String.dropRightWhile is an ordinary function on strings, rather than an IO action.let ← executes the action Using an arrow means that the value of the expression is an IO action that should be executed, with the result of the action saved in the local variable. A do expression contains a sequence of statements, which may be:ordinary local definitions with let and :=, where the defined name refers to the value of the p…
[Notation] What's the type of hi variable?
IO.FS.Stream ← strips BaseIO! If the expression to the right of the arrow has type IO α, then the variable has type α in the remainder of the do block. IO.getStdin and IO.getStdout are IO actions in order to allow stdin and stdout to be locally overridden in a program, which can be convenient.
[Creating Lean project] What's inside lakefile.lean file? Results of executing "lake new greeting"
Configuration that lake needs to BUILD the project.
[Creating Lean project] What's inside lean-toolchain file? Results of executing "lake new greeting"
Lean version.
[Creating Lean project] Where can you find the binary file after running lake build?
/build/bin/greeting To build the package, run the command lake build. After a number of build commands scroll by, the resulting binary has been placed in build/bin. Running ./build/bin/greeting results in Hello, world!. 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. The standard Lean build tool is…
How can we fix "fail to show termination" error?
Add the partial keyword. The dump function is declared partial, because it calls itself recursively on input that is not immediately smaller than an argument. When a function is declared to be partial, Lean does not require a proof that it terminates. On the other hand, partial functions are also much less amenable to proofs of correctness, because allowing infinite loops in Lean's logic would make it unsound. However, there is no way to prove that dump terminates, because infinite input (such…
[Notation] What's a wordier way to write this?
Name 2 ways to test IO actions.
lake build; and execute the binary #eval Quickly testing IO actions with #eval can be much more convenient that compiling and running whole programs. However, there are some limitations. For instance, reading from standard input simply returns empty input. Additionally, the IO action is re-executed whenever Lean needs to update the diagnostic information that it provides to users, and this can happen at unpredictable times.
What's the name for the variables of type IO α?
IO actions. Values of type IO α are called IO actions. 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 language allow side effects to occur during evaluation, Lean does not. Instead, Lean has a type called IO that represents descriptions of programs that use side effects. These descriptions are then executed by the language's run-time system, which…
What does pure 5 do? Values of type IO α are called IO actions. One of the simplest IO actions is pure.
performs NO side effects returns 5 The simplest IO action is pure, which returns its argument and has no actual side effects. Pure.pure.{0, 0} : {f : Type → Type} → [self : Pure f] → {α : Type} → α → f αIf a : α, then pure a : f α represents a monadic action that does nothing and returns a.
What's the name of this?
Type class. This declaration says that there is a type class Plus that overloads operations with respect to a type α. In particular, there is one overloaded operation called plus that takes two αs and returns an α. Once again, there is a terminology clash with object-oriented languages. In object-oriented programming, a method is essentially a function that is connected to a particular object in memory, with special access to the object's private state. Objects are interacted with via their met…
[Type class] Give the analogy for: type class and instance of a type class.
type class - collection of methods A type class describes a collection of overloadable operations.instance of a type class - provides implementation of methods (for a particular type) To overload these operations for a new type, an instance is created that contains an implementation of each operation for the new type. Type classes are also a means of describing types that share common attributes (namely, implementations of certain operations), but they don't really have anything else in common…
Visually imagine what Lean wants when it says this.
Each of these error messages begins with failed to synthesize instance. 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.
[Type Class] What is HAdd short for?
Heterogenous Addition Lean's built-in addition operator is syntactic sugar for a type class called HAdd, which flexibly allows the arguments to addition to have different types. HAdd is short for heterogeneous addition. For instance, an HAdd instance can be written to allow a Nat to be added to a Float, resulting in a new Float.
[Type Class] What's the signature of instance: AAA BBB?
instance : TypeClass Type where
[Type Class] How would we go about overloading + * for our newly defined type? def seven : Pos := Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))
+ - define an instance of the Add typeclass * - define an instance of the Mul typeclass Lean's built-in addition operator is syntactic sugar for a type class called HAdd, which flexibly allows the arguments to addition to have different types. HAdd is short for heterogeneous addition. For instance, an HAdd instance can be written to allow a Nat to be added to a Float, resulting in a new Float. When a programmer writes x + y, it is interpreted as meaning HAdd.hAdd x y.There is a simpler type cla…
What's the Lean 4 version of these? Lean 3
constant => axiom axiom ✅ The keyword constant has been deleted in Lean 4, and axiom should be used instead. def ✅ theorem ✅ lemma ✅ example ✅
Visually imagine the fundamental difference between: constant, axiom def, theorem, lemma, example
constant, axiom - only type is allowed def, theorem, lemma, example - only type AND body is allowed
Analogy for: do block VS by block?
do block - puts Lean into monad mode by block - puts lean into tactic mode To write a proof with tactics, begin the definition with by. Writing by puts Lean into tactic mode until the end of the next indented block.
What's an interesting way to implement this?
However, the obligation to show that the list has at least three entries can be imposed on the caller by adding an argument that consists of evidence that the indexing operation is safe.When the function is called on a concrete list, its length is known. In these cases, by simp can construct the evidence automatically.
In Lean, what's the keyword for: mathematical definition VS theorem?
definition - def With definitions it matters very much which particular value is selected—after all, a definition of addition that always returns 0 is clearly wrong.theorem - theorem Generally speaking, with a proof, what matters is that there is evidence that a proposition is true, but it's not particularly important which evidence was provided. In Lean, it is conventional to declare theorems with the theorem keyword instead of def. This helps readers see which declarations are intended to be…
What does this type say: {α : Type} → [ToString α] → α → IO Unit?
Lean will determine α type automatically there must be a ToString instance for α type!!! This type says that IO.println accepts an argument of type α, which Lean should determine automatically, and that there must be a ToString instance available for α.It returns an IO action. Additionally, there is a u_1 after Type, which uses a feature of Lean that has not yet been introduced. For now, ignore these parameters to Type.
Give an analogy for why we need to implement these interfaces: Add OfNat?
Add - so that we can do x + xs.sum! A function that sums all entries in a list needs two instances: Add allows the entries to be added.OfNat - so that we can return 0 literal! And an OfNat instance for 0 provides a sensible value to return for the empty list. def fourNats : List Nat := [1, 2, 3, 4]#eval fourNats.sum -- 10
Visually imagine: list VS array.
list - [____________] array - #[____________] (dynamically-sized!) Lean arrays are much more efficient than linked lists for most purposes. In Lean, the type Array α is a dynamically-sized array holding values of type α, much like a Java ArrayList, a C++ std::vector, or a Rust std::vec. Unlike List, arrays occupy a contiguous region of memory, which is much better for processor caches. Also, looking up a value in an array takes constant time, while lookup in a linked list takes time proportiona…
What's notable about the negation operator (¬)?
It has a very low precedence. The logical negation operator has a very low precedence, which means that ¬idahoSpiders.inBounds 5 is equivalent to ¬(idahoSpiders.inBounds 5).
What does abbrev approximately expand into?
@[reducible] def abbrev is essentially equivalent to @[reducible] def, which is relevant for instance search because it will look through reducible definitions so what we for example often do in the compiler and elaborator is abbrev MyMonadM := ReaderT Context StateReftT State BaseMonadM and since we are using abbrev here instance search automagically finds the monad instance. The definition of what it means for an index to be in bounds should be written as an abbrev because the tactics used to…
Visually imagine the @[reducible] definition.
Behind the scenes, some definitions are internally marked as being unfoldable during during overload resolution, while others are not. Definitions that are to be unfolded are called reducible. Control over reducibility is essential to allow Lean to scale: fully unfolding all definitions can result in very large types that are slow for a machine to process and difficult for users to understand. Definitions produced with abbrev are marked as reducible. There are a few pragmatic differences betwee…
Boolean equality VS propositional equality?
Boolean equality is the same kind of equality that is found in other programming languages. It is a function that takes two values and returns a Bool. Boolean equality is written with two equals signs, just as in Python and C#. Because Lean is a pure functional language, there's no separate notions of reference vs value equality—pointers cannot be observed directly. Propositional equality is the mathematical statement that two things are equal. Propositional equality is not a function; rather,…
[Typeclasses] What typeclass would you use to implement indexing notation xs[i]?
GetElem The class GetElem cont idx elem dom implements the xs[i] notation.
[Typeclasses] What typeclass would you use to implement ++?
Append => { head := "Banded Garden Spider", tail := ["Long-legged Sac Spider", "Wolf Spider"] } The syntax xs ++ ys desugars to HAppend.hAppend xs ys. For homogeneous cases, it's enough to implement an instance of Append, which follows the usual pattern:
What does deriving instance do?
It automatically creates the instance! Instance of classes like BEq and 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. In fact, the deriving Repr phrase in the definition of Point in the section on structures is an example of instance deriving. Aside from the clear advantages in programmer productivity and code readability, deriving instances…
Visually imagine: a polymorphic type a usual type
a polymorphic type a usual type
What kind of a thing are Functor, Applicative, Monad, etc. in Lean?
Functor, Applicative, Monad are all typeclasses.
Visually imagine the default method definition in a typeclass.
A default method definition provides a default implementation of a method in terms of the other methods. However, instance implementors may choose to override this default with something more efficient. Default method definitions contain := in a class definition. The definition of the Functor class uses one more language feature that has not yet been discussed: default method definitions. Normally, a class will specify some minimal set of overloadable operations that make sense together, and th…
Visually imagine the expanded version of two + two.
Add.add two two Lean's built-in addition operator is syntactic sugar for a type class called HAdd, which flexibly allows the arguments to addition to have different types. HAdd is short for heterogeneous addition. For example, an HAdd instance can be written to allow a Nat to be added to a Float, resulting in a new Float. When a programmer writes x + y, it is interpreted as meaning HAdd.hAdd x y.
Visually imagine what Lean wants when it says this. def four : PosType := Add.add two two
Each of these error messages begins with failed to synthesize instance. 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.
Visually imagine what to insert in this code.
Visually imagine metonymy.
The substitution of the name of an attribute for that of the thing meant, for example suit for business executive, or the track for horse racing. The Pentagon (pictured), the headquarters building of the United States Department of Defense, is a common metonym used to refer to the U.S. military and its leadership. In mathematics, it is common to use the same symbol to stand for different aspects of some object in different contexts. For example, if a ring is referred to in a context where a set…
What can be instead of some in a general version of this syntax?
Any pattern!
What does it mean for a type to be inhabited.
There is at least one element of that type. Many theorems hold under the additional assumption that a type is inhabited, which is to say, it has at least one element. For example, if α is a type, ∃ x : α, x = x is true only if α is inhabited.
What does Coe stand for?
Coercion Coe α β is the typeclass for coercions from α to β. It can be transitively chained with other Coe instances, and coercion is automatically used when x has type α but it is used in a context where β is expected. You can use the ↑x operator to explicitly trigger coercion.
How to make the coercion from Pos to Nat possible?
Add instance : Coe Pos Nat. => [3, 4] Using #check shows the result of the instance search that was used behind the scenes:#check [1, 2, 3, 4].drop (2 : Pos)=> List.drop (Pos.toNat 2) [1, 2, 3, 4] : List Nat
What does CoeDep stand for?
Dependent coercion Can NonEmptyList be coerced into List? Well, depends! It is impossible to write an instance of Coe (List α) (NonEmptyList α), because there's no non-empty list that can represent the empty list. This limitation can be worked around by using another version of coercions, which are called dependent coercions. Dependent coercions can be used when the ability to coerce from one type to another depends on which particular value is being coerced.Just as the OfNat type class takes t…
What's the analogy for: CoeTail VS CoeHead?
CoeTail - executed once, in the end of coercions. Unlike Coe, CoeTail is consulted only as the last step in a sequence of coercions, and it is used at most once.CoeHead - executed once, at the start of coercions. Similarly, there is a CoeHead class that is used at most once at the beginning of a chain of coercions.
Visually imagine a member of a Monoid type. Monoid = Magma + associativity + identity (magma is closed)
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. S is referred to as the "carrier set" of the monoid. The natural numbers with one and multiplication also form a monoid.
Name 2 syntaxes we can instantiate: structure VS typeclass.
Both can use both {} and where! structure typeclass While values that have structure types are typically defined using either ⟨...⟩ syntax or with braces and fields, and instances are typically defined using where, both syntaxes work for both kinds of definition.Generally speaking, the where syntax should be used for instances, and the curly-brace syntax should be used for structures.
What does the deriving clause at the end of the definition do?
It automatically creates an instance! instance : Repr NonEmptyList Evgenia: not sure if this is the right syntax Many type classes have very standard implementations. For instance, the Boolean equality class 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. Instances for these classes can be created automatically.When defining an inductive type or a structure, a deriving clause at the…
What does CoeFun stand for?
Coerce to function A type class called CoeFun can transform values from non-function types to function types.
Name 2 arguments CoeFun expects.
from: Type to: a type of the final function CoeFun has two parameters: the first is the type whose values should be transformed into functions, and the second is an output parameter that determines exactly which function type is being targeted. Because all Adders should be transformed into Nat → Nat functions, the argument to CoeFun's second parameter was ignored.
Which errors do these coercions save us from: Coe CoeFun?
Coe - tries to save us from type errors. The Coe class is used to recover from type errors. When Lean has an expression of type α in a context that expects something with type β, Lean first attempts to string together a chain of coercions that can transform αs into βs, and only displays the error when this cannot be done.CoeFun - tries to save us from "not a function" errors. The CoeFun class intercepts what would otherwise be a "not a function" error when compiling a function application, and…
What's the difference between: associativity VS This operator is left-associative.precedence? This operator has precedence 35.
associativity - is about how && interacts with other && precedence - is about thow && interacts with other operators In Lean, infix operators can be declared using the infix, infixl, and infixr commands, which create (respectively) non-associative, left-associative, and right-associative operators. When used multiple times in a row, a left associative operator stacks up the opening parentheses on the left side of the expression. The addition operator + is left associative, so w + x + y + z is e…
Visually imagine an instance implicit.
Specifications of required instances in square brackets are called instance implicits. Behind the scenes, every type class defines a structure that has a field for each overloaded operation. Instances are values of that structure type, with each field containing an implementation. At a call site, Lean is responsible for finding an instance value to pass for each instance implicit argument. The most important difference between ordinary implicit arguments and instance implicits is the strategy t…
Visually imagine class + instance in terms of structure + value.
A difference between class and structure is that Lean keeps a Class-instance Table.
Give a catchphrase for class Add.
Interface Add.
Give a catchphrase for instance nnn : Add String.
String implements interface Add.
Give a catchphrase for [s : Add α].
Find the instance Add String.