Using implicit parameters in Agda

Question

I am just starting out with Agda and have been following the LearnYouAnAgda tutorial, in which I have been shown this proof for identity:

proof : (A : Set) → A → A
proof _ x = x

From what I understand the _ is necessary to omit the parameter (A : Set). I wanted to use an implicit parameter to allow me to omit the _:

-- using implicit parameter
proof' : {A : Set} → A → A
proof' x = x

This proof works. I then wanted to apply it to a specific case, as is done in the tutorial. I define ℕ and give the type signature for what I want to prove:

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

idProof : ℕ → ℕ

The constructor given in the tutorial using proof is:

idProof = proof ℕ

I don't fully understand this, since I expected proof would need 2 parameters considering the constructor we have already defined.

I wanted to write a constructor using proof' but I found that none of the following worked:

idProof = proof' ℕ
idProof = {x : ℕ} → proof' x
idProof = {x : Set} → proof' x

Using the solver however I found this worked:

idProof = proof' (λ z → z)

My questions are:

1. What are the differences between proof and proof'?

2. Why is it acceptable to use a single parameter, ℕ, for proof?

3. Why do the three constructors using proof' not work?

Bonus:

A small explanation of how idProof = proof' (λ z → z) works (esp. the lambda) would be appreciated, unless it would likely be out of my current level of understanding of Agda.

Answer 1

I don't fully understand this, since I expected proof would need 2 parameters considering the constructor we have already defined.

proof does expect 2 parameters. But idProof also expects one parameters.

When you write

idProof : ℕ → ℕ
idProof = proof ℕ

It's equivalent to first introducing idProof's ℕ and then passing it to proof ℕ like so.

idProof : ℕ → ℕ
idProof n = proof ℕ n

I wanted to write a constructor using proof' but I found that none of the following worked:

• idProof = proof' ℕ

The A parameter for proof' is implicit. So there is no need to pass ℕ explicitly. You can just write idProof = proof' and let Agda figure out that A should be ℕ.

• idProof = {x : ℕ} → proof' x and idProof = {x : Set} → proof' x

idProof is of type ℕ → ℕ but {x : _} → ... is used to construct a Set, not a function so it can't work.

Bonus: A small explanation of how idProof = proof' (λ z → z) works (esp. the lambda)

proof' : {A : Set} -> A -> A tries to figure out what Ashould be based on its argument and the type of the hole it is used in. Here:

• it is passed an identity function so A should have the shape B -> B for some B;
• it used in a hole of type ℕ → ℕ so A should be of the shape ℕ → ℕ.

Conclusion: Agda picks ℕ → ℕ for A.