# Differences in the type signatures using dependent types

What is the difference between the following types for the $$head$$ function on a vector of integers.

($$head$$ takes a natural number $$n$$ and a vector $$v$$ of length $$n$$ or $$(n+1)$$ (depending on the type), and returns the first element of the vector. The key premise here is that the input vector should be non-empty)

1. $$\Pi n:nat. vector ~(n+1) \rightarrow int$$

2. $$\Pi n:nat. (n > 0) \rightarrow vector~n \rightarrow int$$

The first type is along the lines of $$first$$ function in the ATAPL textbook by Pierce et.al. (page 46). However, I want to know the difference (from type checking perspective) w.r.t the second type which requires a proof that $$(n > 0)$$.

Does the second type mean that the language should support Proposition (similar to Coq)? Specifically, I am wondering if the second type is possible in a first order dependent typed language like $$\lambda LF$$ calculus that does not support any explicit propositions/proofs (Fig 2-1, page 51, Section 2.2 of ATAPL textbook).

• They are equivalent up to function extensionality. – ice1000 yesterday