CODEWITHSUNDEEP
lean
ScarletAmaranth
ScarletAmaranth

Reputation: 5101

Why both the typeclass and implicit argument mechanism?

So we can have explicit arguments, denoted by ().
We can also have implicit arguments, denoted by {}.

So far so good.

However, why do we also need the [] notation for type classes specifically?

What is the difference between the following two:

theorem foo  {x : Type} : ∀s : inhabited x, x := sorry
theorem foo' {x : Type} [s : inhabited x] : x := sorry

Upvotes: 0

Views: 268

Answers (1)

user7396200
user7396200

Reputation: 561

Implicit arguments are inserted automatically by Lean's elaborator. The {x : Type} that appears in both of your definitions is one example of an implicit argument: if you have s : inhabited nat, then you can write foo s, which will elaborate to a term of type nat, because the x argument can be inferred from s.

Type class arguments are another kind of implicit argument. Rather than being inferred from later arguments, the elaborator runs a procedure called type class resolution that will attempt to generate a term of the designated type. (See chapter 10 of https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf.) So, your foo' will actually take no arguments at all. If the expected type x can be inferred from context, Lean will look for an instance of inhabited x and insert it:

def foo' {x : Type} [s : inhabited x] : x := default x
instance inh_nat : inhabited nat := ⟨3⟩
#eval (2 : ℕ) + foo' -- 5

Here, Lean infers that x must be nat, and finds and inserts the instance of inhabited nat, so that foo' alone elaborates to a term of type nat.

Upvotes: 1

Related Questions