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

  • $\begingroup$ They are equivalent up to function extensionality. $\endgroup$ – ice1000 yesterday

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.