Implicit Arguments
Suppose we define the compose function as.
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:
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.
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:
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 variable command:
universe u
section
variable {α : Type u}
variable (x : α)
def ident := x
end
variable (α β : Type u)
variable (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.
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.
#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.
def ident {α : Type u} (a : α) : α := a
variable (α β : 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.
def ident {α : Type u} (a : α) : α := a
#check ident (α := Nat) -- Nat → Nat
#check ident (α := Bool) -- Bool → Bool