@@ -120,7 +120,7 @@ Atomic types are described in table~\ref{tab:atomicTypes}.
120120 \centering
121121 \caption{Table of atomic Nix Expression Language types}
122122 \begin{tabular}{ ||c||p{2cm}||p{4cm}|| } \hline
123− \textbf{Atomic type} & \textbf{Description} & \textbf{Example terms} \\ \hline
123+ \textbf{Atomic type} & \textbf{Description} & \textbf{Example terms} \\ \hline \hline
124124 URI & A string literal representing a URI. Does not require quoting. & \texttt{https://example.com} \\ \hline
125125 Path literal & A path literal referring to either a relative or absolute path. Does not require quoting. & \texttt{../../directory/file.txt} \\ \hline
126126 Integer & The current C implementation of Nix allows values of 64-bit signed integers. & \texttt{69} \newline \texttt{-42} \\ \hline
@@ -559,6 +559,45 @@ The term \texttt{x: y: x // y} would field the following type:
559559 \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma
560560\end{equation}
561561
562+\subsection{Atmoic types}
563+
564+Nix is a dynamic language, and as such, allows dynamic coercions between certain types. This means that we can not use the dynamic types from the interpreter to perform static type checking -- if we did that we would reject \emph{a lot} of valid programs.\footnote{``Valid'' not just in the sense that they would not produce runtime errors, but ``valid'' in the sense that the programmer would judge the program as being ``correct''.}
565+
566+For this reason, we will have to define a smaller set of static types that will be employed in our type system. The static types along with the corresponding dynamic types from table~\ref{tab:atomicTypes} are shown in table~\ref{tbl:staticTypes}.
567+
568+\begin{table}[hbp]
569+ \centering
570+ \caption{Mapping from static types to dynamic types}
571+ \begin{tabular}{ ||c||c|| } \hline
572+ \textbf{Static type} & \textbf{Dynamic types} \\ \hline \hline
573+ String & URI, Path literal, String \\ \hline
574+ Number & Integer, Float \\ \hline
575+ Bool & Bool \\ \hline
576+ Null & Null \\ \hline
577+ \end{tabular}
578+ \label{tbl:staticTypes}
579+\end{table}
580+
581+\subsection{Addition}
582+
583+Among all operators, addition (\texttt{+}) has semantics that stand out from the rest: addition can be applied to wither two \texttt{Number} operands or two \texttt{String} operands. All other operands are monomorphic in that they can only be applied to two operands of a predefined type. In that sense addition in polymorphic.
584+
585+Since our current implementation does not support sum types (see section~\ref{sec:sumTypes} for more detail), it is non-trivial to encode the type of addition in our current type system. We wanted to encode the type without having to resort to extending the type system too much (without implementing sum types).
586+
587+The simplest approach is to introduce a simple predicate which is satisfied only if the argument is either of type \texttt{Number} or \texttt{String}:
588+
589+\newcommand{\strOrNum}{(\text{String} || \text{Number})}
590+
591+\begin{equation}
592+ \strOrNum \sim \alpha
593+\end{equation}
594+
595+With this predicate the type of the addition operator (\texttt{+}) now becomes:
596+
597+\begin{equation}
598+ \forall \alpha. \; \strOrNum \sim \alpha \Rightarrow \alpha \rightarrow \alpha \rightarrow \alpha
599+\end{equation}
600+
562601\subsection{Typing rules}
563602
564603\begin{equation}
@@ -612,7 +651,7 @@ The term \texttt{x: y: x // y} would field the following type:
612651\begin{equation}
613652 \trfrac
614653 {\Gamma \vdash e \optDot \text{x} = \tau}
615− {\Gamma \vdash (e \; \text{?} \; \text{x}) : Bool}
654+ {\Gamma \vdash (e \; \text{?} \; \text{x}) : \text{Bool}}
616655\end{equation}
617656
618657\begin{equation}
@@ -639,6 +678,24 @@ The term \texttt{x: y: x // y} would field the following type:
639678 {\Gamma \vdash (\text{if} \; e_1 \; \text{then} \; e_2 \; \text{else} \; e_3) : \tau}
640679\end{equation}
641680
681+\begin{equation}
682+ \trfrac
683+ {\Gamma \vdash e : \tau \qquad \{\text{x} = e;\} \in \xi}
684+ {\Gamma \vdash (\Pi \xi).\text{x} = \tau}
685+\end{equation}
686+
687+\begin{equation}
688+ \trfrac
689+ {\text{x} \notin \xi}
690+ {(\Pi \xi) \optDot \text{x} = \tau}
691+\end{equation}
692+
693+\begin{equation}
694+ \trfrac
695+ {\Gamma, \xi \vdash e : \tau}
696+ {\Gamma \vdash (\text{with } (\Pi \xi)\text{; } e) : \tau}
697+\end{equation}
698+
642699\section{Implementation} \label{sec:implementation}
643700
644701\cite{github-source}
@@ -690,6 +747,10 @@ The technique is not in applicable if the ``result'' of a predicate is not a typ
690747
691748Another limitation is that we can not remove predicates if their ``result'' type variable is not present in the head of the type like in type \ref{eq:optFieldPredExample}, since we would be losing typing information by doing so.
692749
750+\subsection{Type hints}
751+
752+\subsection{Sum types} \label{sec:sumTypes}
753+
693754\section{Conclusion}
694755
695756Nix is a rapidly growing ecosystem. At the time of writing, nixpkgs, the Nix package registry, contains over 60000 packages\footnote{\url{https://github.com/NixOS/nixpkgs}} that can be either installed or used as dependencies in other projects. There is much interest in the approach used by Nix, and making the ever-growing codebase of configurations easier to manage and extend would be a welcome development.