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.
  • 3
    What do you mean "well-defined"? Does Agda accept it? If so, isn't that evidence enough? If not, that would seem more compelling than anything we could say. – Derek Elkins Apr 24 '16 at 3:19
  • I've modified the question. – jonaprieto Apr 25 '16 at 6:09
  • As the code you provided doesn't parse, at least in Agda 2.4.2.5, I suspect that isn't how you defined the function in Agda. – Derek Elkins Apr 25 '16 at 6:13
up vote 8 down vote accepted

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.

  • I am confused about how the identity function is not a dependent type because I see it depends on a term that in this case is A, a term of Set – jonaprieto Apr 27 '16 at 23:46
  • The term A in the type (A : Set) → A → A is a bound variable and does not really exist. If you say you see an A then I will say that there is no A in (B : Set) → B → B. The types (A : Set) → A → A and (B : Set) → B → B are equal. It is just silly notation that makes you think there is an A in there. The type of idd is not dependent, but it is a dependent product. Assuming X is a variable of type Set, the type of idd X is dependent. It depends on X. – Andrej Bauer May 1 '16 at 18:21

I'll use the following code for answer your questions:

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

Is idd a polymorphic function? No. Agda (without universe polymorphism) is a monomorphic language. The idd function is only defined on small types, i.e. Set. The function is not defined on Set1, Set2, ...

Has idd a dependent type? Yes. I'll quote Bove and Dybjer [2009, p. 64]:

Here we see a first use of dependent types: the type A -> A depends on the variable A : Set ranging over the small types.

Bove, A. and Dybjer, P. (2009). Dependent Types at Work. In: LerNet ALFA Summer School 2008. Ed. by Bove, A., Soares Barbosa, L., Pardo, A. and Sousa Pinto, J. Vol. 5520. Lecture Notes in Computer Science. Springer, pp. 57–99.

Your Answer

 
discard

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.

Not the answer you're looking for? Browse other questions tagged or ask your own question.