<commit_before>\section{Indexing descriptions}
\label{sec:indexing-desc}

\begin{wstructure}
!!! Need Help !!!
<- Motivation
    <- Desc: expressivity of simply-typed data-types: inductive types
        <- Values do not influence types
    /> Example: Vectors
        <- Cannot be defined by just induction
            <- Vectors of all size need to be defined at the *same* time
            -> Defined as a *family* of types
                -> Index
        -> I -> IDesc I: Inductive family
    ???
\end{wstructure}

\note{ Need care: motivating motivation of indexing. }

So far, we have explored the well-known realm of inductive types. We
have built upon the experience gained in using simply-typed languages,
such as Haskell or OCaml. In our dependent setting, we provided these
data-types by the mean of $\Desc$, a universe of descriptions. 

While inductive types are the alpha and omega of simply-typed
languages, evolving in a dependent setting fosters new
opportunities. The typical example is bounded lists, also known as
vectors. A vector is a list decorated by its length. Having this
information prevents hazardous operations, such as taking the head of
an empty vector: the head function only takes vectors of length
$\NatSuc{n}$, as enforced by its type. This is made possible by the
very specificity of dependently-typed systems: terms -- the length --
are allowed to influence types -- the vector type. \note{Reference
  paper to cite about vectors in dependent types?}

However, this new class of objects cannot be defined by mere
induction. In the case of vectors, for instance, we have to define the
whole \emph{family} of vector in one go: vectors of all size needs to
be defined at the same time. Where simply-typed languages have
inductive types, in dependently typed programming we the basic grammar of
data-types should be that of inductive families of types. To this end, we
rely on \emph{indexing}. We are going to transform the $\Desc$ universe into
$\IDesc$, the universe of indexed descriptions. We express inductive families
by the $I \To \IDesc{I}$ type.  \note{pwm: Vec might not be the best
motivating example here, since it doesn't appear in the paper (more on that
later). Come to think of it, this is entirely too vague without spelling out
a concrete example.} 

\subsection{Desc, atomically}

\begin{wstructure}
<- Adding hindx have introduced some duplication
    <- indx == hindx 1
    -> We can factor out commonalities 
        /> Obtain an equivalent presentation
        /> Still embeddable (refer to the Agda model)
\end{wstructure}

Before moving on indexed descriptions, we have to carry out some
maintenance work on descriptions. We presented $\Desc$ as the grammar
of inductive types. Hence, the codes closely follow this grammar. In
the following, we adopt an alternative presentation. With $\DSigma$,
we are actually \emph{quoting} a standard type-former, namely

$$\Bhab{\Sigma}{\PI{\V{S}}{\Set} (S \To \Set) \To \Set}$$

In the alternative presentation, we go further and present all our
codes as quotations of standard type-formers. This presentation is
shown in Figure~\ref{fig:type-former-desc}. The reader will notice the
introduction of $\DProd{}{}$ that overlaps with $\DSigma{}{}$. Unlike
$\DSigma{}{}$, $\DProd{}{}$ is first-order, hence amenable to a
definitional treatment. \note{We could replace $\DUnit$ by $\DConst$
  here, instead of doing it in the following section. This is also a
  story about being first-order, so that would make sense, isn't it?}

This reorganisation is strictly equivalent to the previous one
(Fig.~\ref{fig:hindx_desc}). Just as the previous version, it is also
self-descriptive. We refer the reader to the companion technical
report for details. In this finer-grained presentation, we can define
$\DIndx$ and $\DHindx$ as follow:

\[\begin{array}{l@{\:\mapsto\:\:}l}
\DIndx{D}         & \DProd{\DId}{D}                      \\
\DHindx{H}{D}     & \DProd{(\DPi{H}{(\LAM{\_} \DId)})}{D}
\end{array}
\]

Consequently, the examples previously developed can be
straightforwardly translated into this new presentation. For example,
here is the new definition of $\NatD$:

\[\stk{
\NatD : \Desc \\
\NatD \mapsto \DSigma{(\EnumT{[ \NatZero, \NatSuc{} ]})}
                     {[ \DUnit \quad \DId ]}
}\]


In the following, we adopt this last version as our de
facto universe of inductive types. In particular, we are going to
evolve this presentation into an indexed one.

\note{Shall we talk about the Type Theory being Desc Zero? or such story?}

\begin{figure}

\[\stk{
\begin{array}{ll}
\stk{
\data \Desc : \Set \where \\
\;\;\begin{array}{@{}l@{\::\:\:}l@{\quad}l}
    \DId            & \Desc                                   \\
    \DUnit          & \Desc                                   \\
    \DProd{}{}      & \PI{\V{D}, \V{D'}}{\Desc} \Desc         \\
    \DSigma         & \PI{\V{S}}{\Set} \PIS{S \To \Desc} \Desc \\
    \DPi            & \PI{\V{S}}{\Set} \PIS{S \To \Desc} \Desc 
\end{array}
}
\vspace{0.2in}
\\
\stk{
\descop{\_\:}{} : \Desc \To \Set \To \Set \\
\begin{array}{@{}l@{\:=\:\:}ll}
\descop{\DId}{X}          &  X                                           \\
\descop{\DUnit}{X}        &  \Unit                                       \\
\descop{\DProd{D}{D'}}{X} &  \TIMES{\descop{D}{X}}{\descop{D'}{X}}       \\
\descop{\DSigma{S}{D}}{X} &  \SIGMA{\V{s}}{S} \descop{D\: s}{X}                \\
\descop{\DPi{S}{D}}{X}    &  \PI{\V{s}}{S} \descop{D\: s}{X}            
\end{array}
}
\end{array}
}\]

\caption{Universe of descriptions based on Type-formers}
\label{fig:type-former-desc}

\end{figure}

\subsection{From Desc to IDesc}

\begin{wstructure}
<- Labelling Id
    <- We had: data Desc : Set -> Set
    -> We want: data IDesc : (I -> Set) -> Set
        <- Indexed functor (?)
        -> It is sufficient to label Id
            <- Where the functor is built
\end{wstructure}

In the previous section, we have presented the $\Desc$ universe as the
grammar of functors in the category $\Set$. We have seen how to encode
inductive types in this setting. To encode an inductive family indexed
by $\Bhab{\V{I}}{\Set}$, we rely on functors in the category
$\Set^I$. We call these \emph{indexed functors}. 
\note{pwm: What's our story \emph{vis-\`{a}-vis} the 2 notions of indexed
functor at play here: $(I\to\Set)\to\Set$ and $(I\to\Set)\to(I\to\Set)$?}  
In the following, we
implement $I \To \IDesc{I}$ as a grammar for indexed functors:

\[\stk{
\data \IDesc{} (\Bhab{\V{I}}{\Set}) : \Set \where \\
\;\;\ldots \\
\\
\idescop{\_\:}{}{} : \PI{\V{I}}{\Set} \IDesc{I} \To (\V{I} \To \Set) \To \Set    \\
\ldots
}\]

This generalisation can be achieved by a minor evolution of $\Desc$
(Fig.~\ref{fig:type-former-desc}). Indeed, the functorial nature of the
atomic $\Desc$ is entirely captured by the $\DId$ code. We get an indexed
functor by turning $\DId$ into an index-dependent $\DVar$ code:

\[\stk{
\data \IDesc{} (\Bhab{\V{I}}{\Set}) : \Set \where \\
\;\;\begin{array}{@{}l@{\::\:\:}l@{\quad}l}
    \DVar{}         & I \To \IDesc{I}                                   \\
    \ldots          & \ldots
\end{array} \\
\\
\idescop{\_\:}{}{} :_{\PI{\V{I}}{\Set}} \IDesc{I} \To (\V{I} \To \Set) \To \Set        \\
\begin{array}{@{}l@{\:=\:\:}ll}
\idescop{\DVar{i}}{I}{P}      &  P~i                                                 \\
\ldots                        &  \ldots
\end{array}
}\]

\begin{wstructure}
<- Also replacing '1 by 'const  [figure]
    <- For convenience
        <- 'const X equivalent to 'sigma X (\_ -> '1)
        /> Easier to abstract
            <- Extensionally same
            /> 'const more useful in practice
\end{wstructure}

The resulting code of $\IDesc$ is presented in
Figure~\ref{fig:idesc}. The reader will notice that we have also
replaced $\DUnit$ by a more general $\DConst$ code. Whereas $\DUnit$
was interpreted as the unit set, $\DConst{X}$ is interpreted as $X$,
for any $\Bhab{X}{\Set}$. Extensionally, $\DConst{X}$ and
$\DSigma{X}{\DUnit}$ are equivalent. However, $\DConst$ is more
succinct. More importantly, $\DConst$ is \emph{first-order}, unlike
its equivalent encoding. From a definitional perspective, we are
giving more opportunities to the type-system, hence reducing the
burden on the programmer.

\begin{figure}

\[\stk{
\begin{array}{ll}
\stk{
\data \IDesc{} (\Bhab{\V{I}}{\Set}) : \Set \where \\
\;\;\begin{array}{@{}l@{\::\:\:}l@{\quad}l}
    \DVar{}         & I \To \IDesc{I}                                   \\
    \DConst{}       & \Set \To \IDesc{I}                                \\<commit_msg>Desc@ICFP: introduce \DConst when moving Desc to a type former presentation. Transfered from IDesc and avoid redundancy.<commit_after>\section{Indexing descriptions}
\label{sec:indexing-desc}

\begin{wstructure}
!!! Need Help !!!
<- Motivation
    <- Desc: expressivity of simply-typed data-types: inductive types
        <- Values do not influence types
    /> Example: Vectors
        <- Cannot be defined by just induction
            <- Vectors of all size need to be defined at the *same* time
            -> Defined as a *family* of types
                -> Index
        -> I -> IDesc I: Inductive family
    ???
\end{wstructure}

\note{ Need care: motivating motivation of indexing. }

So far, we have explored the well-known realm of inductive types. We
have built upon the experience gained in using simply-typed languages,
such as Haskell or OCaml. In our dependent setting, we provided these
data-types by the mean of $\Desc$, a universe of descriptions. 

While inductive types are the alpha and omega of simply-typed
languages, evolving in a dependent setting fosters new
opportunities. The typical example is bounded lists, also known as
vectors. A vector is a list decorated by its length. Having this
information prevents hazardous operations, such as taking the head of
an empty vector: the head function only takes vectors of length
$\NatSuc{n}$, as enforced by its type. This is made possible by the
very specificity of dependently-typed systems: terms -- the length --
are allowed to influence types -- the vector type. \note{Reference
  paper to cite about vectors in dependent types?}

However, this new class of objects cannot be defined by mere
induction. In the case of vectors, for instance, we have to define the
whole \emph{family} of vector in one go: vectors of all size needs to
be defined at the same time. Where simply-typed languages have
inductive types, in dependently typed programming we the basic grammar of
data-types should be that of inductive families of types. To this end, we
rely on \emph{indexing}. We are going to transform the $\Desc$ universe into
$\IDesc$, the universe of indexed descriptions. We express inductive families
by the $I \To \IDesc{I}$ type.  \note{pwm: Vec might not be the best
motivating example here, since it doesn't appear in the paper (more on that
later). Come to think of it, this is entirely too vague without spelling out
a concrete example.} 

\subsection{Desc, atomically}

\begin{wstructure}
<- Adding hindx have introduced some duplication
    <- indx == hindx 1
    -> We can factor out commonalities 
        /> Obtain an equivalent presentation
        /> Still embeddable (refer to the Agda model)
\end{wstructure}

Before moving on indexed descriptions, we have to carry out some
maintenance work on descriptions. We presented $\Desc$ as the grammar
of inductive types. Hence, the codes closely follow this grammar. In
the following, we adopt an alternative presentation. With $\DSigma$,
we are actually \emph{quoting} a standard type-former, namely

$$\Bhab{\Sigma}{\PI{\V{S}}{\Set} (S \To \Set) \To \Set}$$

In the alternative presentation, we go further and present all our
codes as quotations of standard type-formers. This presentation is
shown in Figure~\ref{fig:type-former-desc}. The reader will notice
that we replace $\DUnit$ by a more general $\DConst$ code. Whereas
$\DUnit$ was interpreted as the unit set, $\DConst{X}$ is interpreted
as $X$, for any $\Bhab{X}{\Set}$. Extensionally, $\DConst{X}$ and
$\DSigma{X}{\DUnit}$ are equivalent. However, $\DConst$ is more
succinct. More importantly, $\DConst$ is \emph{first-order}, unlike
its equivalent encoding. From a definitional perspective, we are
giving more opportunities to the type-system, hence reducing the
burden on the programmer. For the same reason, we introduce
$\DProd{}{}$ that overlaps with $\DSigma{}{}$.

This reorganisation is strictly equivalent to the previous one
(Fig.~\ref{fig:hindx_desc}). Just as the previous version, it is also
self-descriptive. We refer the reader to the companion technical
report for details. In this finer-grained presentation, we can define
$\DIndx$ and $\DHindx$ as follow:

\[\begin{array}{l@{\:\mapsto\:\:}l}
\DIndx{D}         & \DProd{\DId}{D}                      \\
\DHindx{H}{D}     & \DProd{(\DPi{H}{(\LAM{\_} \DId)})}{D}
\end{array}
\]

Consequently, the examples previously developed can be
straightforwardly translated into this new presentation. For example,
here is the new definition of $\NatD$:

\[\stk{
\NatD : \Desc \\
\NatD \mapsto \DSigma{(\EnumT{[ \NatZero, \NatSuc{} ]})}
                     {[ \DUnit \quad \DId ]}
}\]


In the following, we adopt this last version as our de
facto universe of inductive types. In particular, we are going to
evolve this presentation into an indexed one.

\note{Shall we talk about the Type Theory being Desc Zero? or such story?}

\begin{figure}

\[\stk{
\begin{array}{ll}
\stk{
\data \Desc : \Set \where                                      \\
\;\;\begin{array}{@{}l@{\::\:\:}l@{\quad}l}
    \DId            & \Desc                                    \\
    \DConst{}       & \Set \To \Desc                           \\
    \DProd{}{}      & \PI{\V{D}, \V{D'}}{\Desc} \Desc          \\
    \DSigma         & \PI{\V{S}}{\Set} \PIS{S \To \Desc} \Desc \\
    \DPi            & \PI{\V{S}}{\Set} \PIS{S \To \Desc} \Desc 
\end{array}
}
\vspace{0.2in}
\\
\stk{
\descop{\_\:}{} : \Desc \To \Set \To \Set \\
\begin{array}{@{}l@{\:=\:\:}ll}
\descop{\DId}{X}          &  X                                           \\
\descop{\DConst{Z}}{X}    &  Z                                           \\
\descop{\DProd{D}{D'}}{X} &  \TIMES{\descop{D}{X}}{\descop{D'}{X}}       \\
\descop{\DSigma{S}{D}}{X} &  \SIGMA{\V{s}}{S} \descop{D\: s}{X}          \\
\descop{\DPi{S}{D}}{X}    &  \PI{\V{s}}{S} \descop{D\: s}{X}            
\end{array}
}
\end{array}
}\]

\caption{Universe of descriptions based on Type-formers}
\label{fig:type-former-desc}

\end{figure}

\subsection{From Desc to IDesc}

\begin{wstructure}
<- Labelling Id
    <- We had: data Desc : Set -> Set
    -> We want: data IDesc : (I -> Set) -> Set
        <- Indexed functor (?)
        -> It is sufficient to label Id
            <- Where the functor is built
\end{wstructure}

In the previous section, we have presented the $\Desc$ universe as the
grammar of functors in the category $\Set$. We have seen how to encode
inductive types in this setting. To encode an inductive family indexed
by $\Bhab{\V{I}}{\Set}$, we rely on functors in the category
$\Set^I$. We call these \emph{indexed functors}. 
\note{pwm: What's our story \emph{vis-\`{a}-vis} the 2 notions of indexed
functor at play here: $(I\to\Set)\to\Set$ and $(I\to\Set)\to(I\to\Set)$?}  
In the following, we
implement $I \To \IDesc{I}$ as a grammar for indexed functors:

\[\stk{
\data \IDesc{} (\Bhab{\V{I}}{\Set}) : \Set \where \\
\;\;\ldots \\
\\
\idescop{\_\:}{}{} : \PI{\V{I}}{\Set} \IDesc{I} \To (\V{I} \To \Set) \To \Set    \\
\ldots
}\]

This generalisation can be achieved by a minor evolution of $\Desc$
(Fig.~\ref{fig:type-former-desc}). Indeed, the functorial nature of the
atomic $\Desc$ is entirely captured by the $\DId$ code. We get an indexed
functor by turning $\DId$ into an index-dependent $\DVar$ code:

\[\stk{
\data \IDesc{} (\Bhab{\V{I}}{\Set}) : \Set \where \\
\;\;\begin{array}{@{}l@{\::\:\:}l@{\quad}l}
    \DVar{}         & I \To \IDesc{I}                                   \\
    \ldots          & \ldots
\end{array} \\
\\
\idescop{\_\:}{}{} :_{\PI{\V{I}}{\Set}} \IDesc{I} \To (\V{I} \To \Set) \To \Set        \\
\begin{array}{@{}l@{\:=\:\:}ll}
\idescop{\DVar{i}}{I}{P}      &  P~i                                                 \\
\ldots                        &  \ldots
\end{array}
}\]

\begin{wstructure}
<- Also replacing '1 by 'const  [figure]
    <- For convenience
        <- 'const X equivalent to 'sigma X (\_ -> '1)
        /> Easier to abstract
            <- Extensionally same
            /> 'const more useful in practice
\end{wstructure}

The resulting code of $\IDesc$ is presented in
Figure~\ref{fig:idesc}. 

\begin{figure}

\[\stk{
\begin{array}{ll}
\stk{
\data \IDesc{} (\Bhab{\V{I}}{\Set}) : \Set \where \\
\;\;\begin{array}{@{}l@{\::\:\:}l@{\quad}l}
    \DVar{}         & I \To \IDesc{I}                                   \\
    \DConst{}       & \Set \To \IDesc{I}                                \\
{'fraction_non_alphanumeric': 0.1442528397386852, 'fraction_numerical': 0.0007062562533105762, 'mean_word_length': 2.5870804306523114, 'pattern_counts': {'":': 0, '<': 33, '<?xml version=': 0, '>': 35, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 19, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4538434', 'n_tokens_mistral': 5426, 'n_tokens_neox': 5214, 'n_words': 2000}