Cheap and Secure Web Hosting Provider : See Now

[Solved]: About the Identity function in Agda

, , No Comments
Problem Detail: 

I've defined the identity function in Agda as follows:

idd : (∀ {ℓ} {A: Set ℓ}) → A → A idd a = a 

I want to ask you if the following reasonings are correct:

  • The type of this function is A -> A.
  • idd is a polymorphic function, where (∀ {ℓ} {A: Set ℓ}) matches any type.
  • Because is a polymorphic function, I can say idd is of dependent type.
Asked By : jonaprieto

Answered By : Andrej Bauer

Your code does not work. I would suggest that you forget about the universe levels for the time being (the $\ell$ thing) and focus on simpler things first. Here is working code:

idd : (A : Set) → A → A idd A a = a 

The type of idd is (A : Set) → A → A. It is a dependent product, i.e., it could be written as $\prod_{A : \mathsf{Set}} A \to A$ in mathematical notation. If we have a type B then the type of id B is B → B.

You say:

The type of this function is A -> A.

No. The type if idd is exactly what it says, namely (A : Set) → A → A.

idd is a polymorphic function, where (∀ {ℓ} {A: Set ℓ}) matches any type.

Let us forget about . In this case the question is whether idd is a polymorphic function. The answer is "yes" because A matches any type.

Because is a polymorphic function, I can say idd is of dependent type.

No. This is the wrong way to think. The function idd does not have a dependent type. It has the fixed type (A : Set) → A → A. However, this fixed type is a dependent product.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/56415

3.2K people like this

 Download Related Notes/Documents

0 comments:

Post a Comment

Let us know your responses and feedback