CODEWITHSUNDEEP
coq
Yusuke Yoshimoto
Yusuke Yoshimoto

Reputation: 151

Are arrows in Coq aliases of universal quantifications?

I'm reading chapter 4 of the reference manual of Coq. According to the typing rules described by the reference, the type of term fun x: nat => x is forall x: nat, nat.

Assume that E is [nat: Set].

              ...                                 ...
------------------------------ Prod-Set  ------------------- Var
E[] ⊢ forall x: nat, nat : Set           E[x: nat] ⊢ x : nat
------------------------------------------------------------ Lam
        E[] ⊢ fun x: nat => x : forall x: nat, nat

However, when I Check this term by Coq, it is typed nat -> nat.

Welcome to Coq 8.5pl2 (July 2016)

Coq < Check fun x: nat => x.
fun x : nat => x
     : nat -> nat

Are these two types same ones? If so, do arrows have hidden names of bound variables?

Upvotes: 3

Views: 192

Answers (2)

ejgallego
ejgallego

Reputation: 6852

As others have said arrow is indeed a notation. See theories/Init/Logic.v#L13 in the Coq sources:

Notation "A -> B" := (forall (_ : A), B) : type_scope.

This file is loaded by the Prelude, you can avoid it with with -noinit.

Upvotes: 5

Vinz
Vinz

Reputation: 6047

The actual type of fun x: nat => x is nat -> nat because their is no type dependency. The arrow is syntax sugar for forall _:nat, nat: the type of the body does not depend on the value of x, only the body itself is using x. An example of type dependency would be vector.

vector A n is the type of list of length n containing elements of type A. Let's consider the concat function which concatenate two vectors:

concat : forall n m: nat, vector n A -> vector m A -> vector (n + m) A

It takes as input two integers, n and m, two vectors of respective size n and m and concatenate them. This time, the type of concat depends on the value of n and m so you have to name them and use the forall instead of the ->. If you try to write nat -> nat -> vector n A -> ..., the variable n won't be correctly bounded.

Upvotes: 3

Related Questions