# Implementation of vectors as dependent types in CoC

I'm trying to understand dependent types in CoC and I am having trouble finding examples that are actually carried out in CoC, specifically without inductive types or pattern matching. The most commonly used example of a dependent type seems to be that of vectors (seen as lists with a fixed number of elements), so I'm trying to write it as follows. I start with the Church encoding of naturals: $$\textit{N} := \forall t ^ * . (t \to t) \to t \to t \\ \textit{Z} := \lambda t ^ * . \lambda s ^ {t \to t} . \lambda z ^ t . z \\ \textit{S} := \lambda p ^ N . \lambda t ^ * . \lambda s ^ {t \to t} . \lambda z ^ t . (s \ (p \ t \ s \ z)) \\$$ For the first method, I have the following: $$\textit{Vec} := \lambda \alpha ^ * . \lambda p ^ N . \forall t ^ {N \to *} . \forall n ^ {(t \ Z)} . \forall c ^ {\forall q ^ N . \alpha \to (t \ q) \to (t \ (S \ q))} . (t \ p) \\ \textit{Nil} := \lambda \alpha ^ * . \lambda t ^ {N \to *} . \lambda n ^ {(t \ Z)} . \lambda c ^ {\forall q ^ N . \alpha \to (t \ q) \to (t \ (S \ q))} . n \\ \textit{Cons} := \lambda \alpha ^ * . \lambda p ^ N . \lambda e ^ \alpha . \lambda r ^ {(\textit{Vec} \ \alpha \ p)} . \lambda t ^ {N \to *} . \lambda n ^ {(t \ Z)} . \lambda c ^ {\forall q ^ N . \alpha \to (t \ q) \to (t \ (S \ q))} . (c \ p \ e \ (r \ t \ n \ c)) \\ \textit{Nil} : \forall \alpha ^ * . (\textit{Vec} \ \alpha \ Z) \\ \textit{Cons} : \forall \alpha ^ * . \forall p ^ N . \alpha \to (\textit{Vec} \ \alpha \ p) \to (\textit{Vec} \ \alpha \ (S \ p)) \\$$ This seems to work, which is already progress from the first version of my question. The part that I don't like with this solution is that for $$Cons$$ I need to provide both the input vector $$v$$ and its length $$p$$ even though the length is already implicit in $$v$$. Is there a way around that, or this is the best we can do?

Another idea would be to define $$Vec$$ using a polymorphic type constructor in its signature: $$\textit{Vec} := \lambda \alpha ^ * . \forall t ^ {* \to *} . \forall u ^ * . u \to (\forall v ^ * . \alpha \to v \to (t \ v)) \to ? \\ \textit{Nil} := \lambda \alpha ^ * . \lambda t ^ {* \to *} . \lambda u ^ * . \lambda n ^ u . \lambda c ^ {\forall v ^ * . \alpha \to v \to (t \ v)} . n \\ \textit{Cons} := \lambda \alpha ^ * . \lambda e ^ \alpha . \lambda r ^ T . \lambda t ^ {* \to *} . \lambda u ^ * . \lambda n ^ u . \lambda c ^ {\forall u ^ * . \alpha \to v \to (t \ v)} . (c \ ? \ a \ (r \ t \ u \ n \ c)) \\$$ But in this case it is not clear how to complete the definitions of $$Vec$$ and $$Cons$$. Also the signatures have become a lot more complicated and the natural number dependency is no longer visible (I suspect it can be added somehow via naturals defined over $$\square$$ instead of $$*$$).

• I think I can provide a useful hint to myself and others that might be interested about this question: in order for a type $\forall t : A . B$ to be truly dependent, we need to use the variable $x$ inside $B$. But if $x$ corresponds to a value, the only way I can come up with to make a type is if the context already has a function that takes in a value and returns a type. So in my first attempt to implement vectors I'll try $Vec := \lambda \alpha : * . \lambda n : Nat . \forall t : Nat \to * . ?$. Dec 3, 2021 at 9:10
• Another possible hint: Define your type in Coq (or Lean, I guess?) and print the type of the automatically generated eliminator: it's going to be similar to the type you're looking for.
– cody
Dec 3, 2021 at 15:35