3
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ 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 * . ?$. $\endgroup$ Dec 3, 2021 at 9:10
  • $\begingroup$ 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. $\endgroup$
    – cody
    Dec 3, 2021 at 15:35

1 Answer 1

3
$\begingroup$

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.

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.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.