<p>I don't have time to fully answer your question, but a good paper to read for insight into how to proceed is Bob Atkey's paper, <a href="https://bentnib.org/fomega-parametricity.html" rel="nofollow noreferrer"><em>Relational Parametricity for Higher Kinds</em></a>.</p>
<p>This paper shows how to do Church encodings for a wide variety of type constructors. Most relevantly for your question, it shows how to take least fixed points of indexed functors. You'll want to read sections 4.3-4.5 especially carefully.</p>

CC BY-SA 4.0
2021-12-10T10:24:20.697Z
2021-12-10T10:24:20.697Z
Neel Krishnaswami
<p>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:
<span class="math-container">$$
\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)) \\
$$</span>
For the first method, I have the following:
<span class="math-container">$$
\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)) \\
$$</span>
This seems to work, which is already progress from the first version of my question. <strong>The part that I don't like with this solution is that for <span class="math-container">$Cons$</span> I need to provide both the input vector <span class="math-container">$v$</span> and its length <span class="math-container">$p$</span> even though the length is already implicit in <span class="math-container">$v$</span>. Is there a way around that, or this is the best we can do?</strong></p>
<p>Another idea would be to define <span class="math-container">$Vec$</span> using a polymorphic type constructor in its signature:
<span class="math-container">$$
\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)) \\
$$</span>
<strong>But in this case it is not clear how to complete the definitions of <span class="math-container">$Vec$</span> and <span class="math-container">$Cons$</span>. 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 <span class="math-container">$\square$</span> instead of <span class="math-container">$*$</span>).</strong></p>

CC BY-SA 4.0
2021-12-03T09:10:59.447Z
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 * . ?$.
Cristian Gratie
CC BY-SA 4.0
2021-12-03T15:35:32.350Z
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
<dependent-type><calculus-of-constructions>
Implementation of vectors as dependent types in CoC
Cristian Gratie
# Implementation of vectors as dependent types in CoC

(Asked by: username_0 on 2021-12-01)

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 $\*$).**

**Tags:** dependent-type, calculus-of-constructions
> **Comments:**
> **username_0**: 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 * . ?$.  
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2021-12-10. Score: 3

I don't have time to fully answer your question, but a good paper to read for insight into how to proceed is Bob Atkey's paper, [*Relational Parametricity for Higher Kinds*](https://bentnib.org/fomega-parametricity.html).

This paper shows how to do Church encodings for a wide variety of type constructors. Most relevantly for your question, it shows how to take least fixed points of indexed functors. You'll want to read sections 4.3-4.5 especially carefully.


---

