doc: implicit arguments

doc/SUMMARY.md

@@ -11,9 +11,11 @@
   - [Function Abstraction and Evaluation](./funabst.md)
   - [Introducing Definitions](./introdef.md)
   - [What makes dependent type theory dependent?](./dep.md)
+- [Organizational features](./organization.md)
+  - [Sections](./sections.md)
+  - [Namespaces](./namespaces.md)
+  - [Implicit Arguments](./implicit.md)
 - [Functions](./functions.md)
-- [Sections](./sections.md)
-- [Namespaces](./namespaces.md)
 - [Type classes](./typeclass.md)
 - [The `do` Notation](./do.md)
 - [Tactics](./tactics.md)

doc/dep.md

@@ -21,13 +21,13 @@ These types vary depending on the first argument, ``α``.
 
 This is an instance of a *dependent function type*, or *dependent arrow type*. Given ``α : Type`` and ``β : α → Type``,
 think of ``β`` as a family of types over ``α``, that is, a type ``β a`` for each ``a : α``.
-In that case, the type ``(x : α) → β x`` denotes the type of functions ``f`` with the property that,
+In that case, the type ``(a : α) → β a`` denotes the type of functions ``f`` with the property that,
 for each ``a : α``, ``f a`` is an element of ``β a``. In other words, the type of the value returned by ``f`` depends on its input.
 
-Notice that ``(x : α) → β`` makes sense for any expression ``β : Type``. When the value of ``β`` depends on ``x``
-(as does, for example, the expression ``β x`` in the previous paragraph), ``(x : α) → β`` denotes a dependent function type.
-When ``β`` doesn't depend on ``x``, ``(x : α) → β`` is no different from the type ``α → β``.
-Indeed, in dependent type theory (and in Lean), ``α → β`` is just notation for ``(x : α) → β`` when ``β`` does not depend on ``x``.
+Notice that ``(a : α) → β`` makes sense for any expression ``β : Type``. When the value of ``β`` depends on ``a``
+(as does, for example, the expression ``β a`` in the previous paragraph), ``(a : α) → β`` denotes a dependent function type.
+When ``β`` doesn't depend on ``a``, ``(a : α) → β`` is no different from the type ``α → β``.
+Indeed, in dependent type theory (and in Lean), ``α → β`` is just notation for ``(a : α) → β`` when ``β`` does not depend on ``a``.
 
 Returning to the example of lists, we can use the command `#check` to inspect the type of the following `List` functions
 We will explain the ``@`` symbol and the difference between the round and curly brackets momentarily.
@@ -39,17 +39,17 @@ We will explain the ``@`` symbol and the difference between the round and curly
 #check @List.append  -- {α : Type u_1} → List α → List α → List α
 ```
 
-Just as dependent function types ``(x : α) → β x`` generalize the notion of a function type ``α → β`` by allowing ``β`` to depend on ``α``,
-dependent cartesian product types ``(x : α) × β x`` generalize the cartesian product ``α × β`` in the same way. Dependent products are also
-called *sigma* types, and you can also write them as `Σ x : α, β x`. You can use `⟨a, b⟩` or `Sigma.mk a b` to create a dependent pair.
+Just as dependent function types ``(a : α) → β a`` generalize the notion of a function type ``α → β`` by allowing ``β`` to depend on ``α``,
+dependent cartesian product types ``(a : α) × β a`` generalize the cartesian product ``α × β`` in the same way. Dependent products are also
+called *sigma* types, and you can also write them as `Σ a : α, β a`. You can use `⟨a, b⟩` or `Sigma.mk a b` to create a dependent pair.
 
 ```lean
 universes u v
 
-def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (x : α) × β x :=
+def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
   ⟨a, b⟩
 
-def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ x : α, β x :=
+def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
   Sigma.mk a b
 
 #reduce f

doc/implicit.md

@@ -0,0 +1,142 @@
+## Implicit Arguments
+
+Suppose we define the `compose` function as.
+
+```lean
+def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+```
+
+The function `compose` takes three types, ``α``, ``β``, and ``γ``, and two functions, ``g : β → γ`` and ``f : α → β``, a value `x : α`, and
+returns ``g (f x)``, the composition of ``g`` and ``f``.
+We say `compose` is polymorphic over types ``α``, ``β``, and ``γ``. Now, let's use `compose`:
+
+```lean
+# def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
+#   g (f x)
+def double (x : Nat) := 2*x
+def triple (x : Nat) := 3*x
+
+#check compose Nat Nat Nat double triple 10 -- Nat
+#eval  compose Nat Nat Nat double triple 10 -- 60
+
+def appendWorld (s : String) := s ++ "world"
+#check String.length -- String → Nat
+
+#check compose String String Nat String.length appendWorld "hello" -- Nat
+#eval  compose String String Nat String.length appendWorld "hello" -- 10
+```
+
+Because `compose` is polymorphic over types ``α``, ``β``, and ``γ``, we have to provide them in the examples above.
+But this information is redundant: one can infer the types from the arguments ``g`` and ``f``.
+This is a central feature of dependent type theory: terms carry a lot of information, and often some of that information can be inferred from the context.
+In Lean, one uses an underscore, ``_``, to specify that the system should fill in the information automatically.
+
+```lean
+# def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
+#  g (f x)
+# def double (x : Nat) := 2*x
+# def triple (x : Nat) := 3*x
+#check compose _ _ _ double triple 10 -- Nat
+#eval  compose Nat Nat Nat double triple 10 -- 60
+# def appendWorld (s : String) := s ++ "world"
+# #check String.length -- String → Nat
+#check compose _ _ _ String.length appendWorld "hello" -- Nat
+#eval  compose _ _ _ String.length appendWorld "hello" -- 10
+```
+It is still tedious, however, to type all these underscores. When a function takes an argument that can generally be inferred from context,
+Lean allows us to specify that this argument should, by default, be left implicit. This is done by putting the arguments in curly braces, as follows:
+
+```lean
+def compose {α β γ : Type} (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+# def double (x : Nat) := 2*x
+# def triple (x : Nat) := 3*x
+#check compose double triple 10 -- Nat
+#eval  compose double triple 10 -- 60
+# def appendWorld (s : String) := s ++ "world"
+# #check String.length -- String → Nat
+#check compose String.length appendWorld "hello" -- Nat
+#eval  compose String.length appendWorld "hello" -- 10
+```
+All that has changed are the braces around ``α β γ: Type``.
+It makes these three arguments implicit. Notationally, this hides the specification of the type,
+making it look as though ``compose`` simply takes 3 arguments.
+
+Variables can also be specified as implicit when they are declared with
+the ``variables`` command:
+
+```lean
+universe u
+
+section
+  variable {α : Type u}
+  variable (x : α)
+  def ident := x
+end
+
+variables (α β : Type u)
+variables (a : α) (b : β)
+
+#check ident
+#check ident a
+#check ident b
+```
+
+This definition of ``ident`` here has the same effect as the one above.
+
+Lean has very complex mechanisms for instantiating implicit arguments, and we will see that they can be used to infer function types, predicates, and even proofs.
+The process of instantiating these "holes," or "placeholders," in a term is part of a bigger process called *elaboration*.
+The presence of implicit arguments means that at times there may be insufficient information to fix the meaning of an expression precisely.
+An expression like ``ident`` is said to be *polymorphic*, because it can take on different meanings in different contexts.
+
+One can always specify the type ``T`` of an expression ``e`` by writing ``(e : T)``.
+This instructs Lean's elaborator to use the value ``T`` as the type of ``e`` when trying to elaborate it.
+In the following example, this mechanism is used to specify the desired types of the expressions ``ident``.
+
+```lean
+def ident {α : Type u} (a : α) : α := a
+
+#check (ident : Nat → Nat) -- Nat → Nat
+```
+
+Numerals are overloaded in Lean, but when the type of a numeral cannot be inferred, Lean assumes, by default, that it is a natural number.
+So the expressions in the first two ``#check`` commands below are elaborated in the same way, whereas the third ``#check`` command interprets ``2`` as an integer.
+
+```lean
+#check 2         -- Nat
+#check (2 : Nat) -- Nat
+#check (2 : Int) -- Int
+```
+
+Sometimes, however, we may find ourselves in a situation where we have declared an argument to a function to be implicit,
+but now want to provide the argument explicitly. If ``foo`` is such a function, the notation ``@foo`` denotes the same function with all
+the arguments made explicit.
+
+```lean
+# def ident {α : Type u} (a : α) : α := a
+variables (α β : Type)
+
+#check @ident           -- {α : Type u} → α → α
+#check @ident α         -- α → α
+#check @ident β         -- β → β
+#check @ident Nat       -- Nat → Nat
+#check @ident Bool true -- Bool
+```
+
+Notice that now the first ``#check`` command gives the type of the identifier, ``ident``, without inserting any placeholders.
+Moreover, the output indicates that the first argument is implicit.
+
+Named arguments enable you to specify an argument for a parameter by matching the argument with
+its name rather than with its position in the parameter list. You can use them to specify explicit *and* implicit arguments.
+If you don't remember the order of the parameters but know their names, you can send the arguments in any order.
+You may also provide the value for an implicit parameter when
+Lean failed to infer it. Named arguments also improve the readability of your code by identifying what
+each argument represents.
+
+```lean
+# def ident {α : Type u} (a : α) : α := a
+
+#check ident (α := Nat)  -- Nat → Nat
+#check ident (α := Bool) -- Bool → Bool
+```

doc/organization.md

@@ -0,0 +1,4 @@
+# Organizational features
+
+In this section we introduce some organizational features of Lean that are not a part of its kernel per se,
+but make it possible to work in the framework more efficiently.

doc/sections.md

@@ -33,12 +33,12 @@ variables (g : β → γ) (f : α → β) (h : α → α)
 variable (x : α)
 
 def compose := g (f x)
-def do_twice := h (h x)
-def do_thrice := h (h (h x))
+def doTwice := h (h x)
+def doThrice := h (h (h x))
 
 #print compose
-#print do_twice
-#print do_thrice
+#print doTwice
+#print doThrice
 ```
 Printing them out shows that all three groups of definitions have exactly the same effect.
 
@@ -57,8 +57,8 @@ section useful
   variable (x : α)
 
   def compose := g (f x)
-  def do_twice := h (h x)
-  def do_thrice := h (h (h x))
+  def doTwice := h (h x)
+  def doThrice := h (h (h x))
 end useful
 ```