Multi tool use

Using implicit parameters in Agda

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 _:

_

(A : Set)

_

-- 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:

proof

idProof = proof ℕ


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

proof

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

proof'

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:

What are the differences between proof and proof'?

proof

proof'

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

ℕ

proof

Why do the three constructors using proof' not work?

proof'

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.

idProof = proof' (λ z → z)

1 Answer
1

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

proof

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

proof

idProof

When you write

idProof : ℕ → ℕ
idProof = proof ℕ


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

idProof

ℕ

proof ℕ

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 ℕ.

A

proof'

ℕ

idProof = proof'

A

ℕ

idProof = {x : ℕ} → proof' x

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.

idProof

ℕ → ℕ

{x : _} → ...

Set

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

idProof = proof' (λ z → z)

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:

proof' : {A : Set} -> A -> A

A

A

B -> B

B

ℕ → ℕ

A

ℕ → ℕ

Conclusion: Agda picks ℕ → ℕ for A.

ℕ → ℕ

A

idProof = proof' {ℕ}

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.