@@ -516,7 +516,7 @@ The type $\alpha$ should be an attribute set and it should contain a field $x$ o
516516
517517The term \texttt{x: x.y} would field the following type:
518518
519−\begin{equation}
519+\begin{equation} \label{eq:dotExample}
520520 \forall \alpha \beta. \; \alpha.\text{y} = \beta \Rightarrow \alpha \rightarrow \beta
521521\end{equation}
522522
@@ -530,7 +530,7 @@ The type $\alpha$ should be an attribute set and if it contains the field $x$, t
530530
531531The term \texttt{x: x.y or 1} would field the following type:
532532
533−\begin{equation}
533+\begin{equation} \label{eq:optFieldPredExample}
534534 \forall \alpha. \; \alpha \optDot \text{y} = \text{Number} \Rightarrow \alpha \rightarrow \text{Number}
535535\end{equation}
536536
@@ -538,7 +538,7 @@ This predicate also arises from the use of the \emph{attribute set field presenc
538538
539539The term \texttt{x: x ? y} would field the following type:
540540
541−\begin{equation}
541+\begin{equation} \label{eq:optFieldPredExample2}
542542 \forall \alpha \beta. \; \alpha \optDot \text{y} = \beta \Rightarrow \alpha \rightarrow \text{Bool}
543543\end{equation}
544544
@@ -550,23 +550,56 @@ The term \texttt{x: x ? y} would field the following type:
550550
551551All $\alpha$, $\beta$ and $\gamma$ should be \emph{attribute sets}. The \emph{attribute set} $\gamma$ should contain all fields from both $\alpha$ and $\beta$, preferring the types from $\beta$ if they happen to overlap. That is, if $\alpha$ and $\beta$ both contain a field with the same name, then $\gamma$ should contain the same field with the type from $\beta$. This behaviour matches the way the \emph{update operator} (\texttt{//}) works as discussed in section~\ref{sec:update}.
552552
553−The term \texttt{x: x ? y} would field the following type:
553+The term \texttt{x: y: x // y} would field the following type:
554554
555−\begin{equation}
556− \forall \alpha \beta. \; \alpha \optDot \text{y} = \beta \Rightarrow \alpha \rightarrow \text{Bool}
555+\begin{equation} \label{eq:updatePredExample}
556+ \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma
557557\end{equation}
558558
559−\subsubsection{Making predicates more user-friendly}
559+\subsection{Making predicates more user-friendly}
560+
561+\subsubsection{A novel technique}
560562
561563The reader might observe that, although the predicates have a parallel with the Nix term syntax, visually parsing predicates and mentally applying them to the specified type variables can be difficult even in such simple examples. Here we will explore a technique that can be used to make these predicates easier for the programmer to work with.
562564
565+The technique is based on the fact that a type variable by itself can only convey the following information:
566+
567+\begin{enumerate}
568+ \item positional information -- a specific position in a type
569+ \item identity information -- the type variable is equivalent to other type variable with the same name within the scope where it is declared
570+\end{enumerate}
571+
563572Note that all of what follows is only concerned with syntactic constructs. It does in no way alter the semantic of the predicates described above.
564573
565574We would like to point out that all of the predicates have an operand which is the ``result'' of the predicate -- a single type variable which is said to be equivalent to a more complex expression. That is $\beta$ in predicates \ref{eq:fieldPred} and \ref{eq:optFieldPred}, and $\gamma$ in predicate \ref{eq:upatePred}.
566575
567576The observation we need to make is that \emph{referential transparency}\footnote{\url{https://en.wikipedia.org/wiki/Referential_transparency}} is it natural notion in functional programming languages like Nix, and it is natural to replace variables with their definitions. In some sense the ``results'' of predicates described above can be interpreted as being ``defined'' by the predicate to be ``equal'' to the combination of the other operands, and, as such, can be replaced with their definitions.
568577
569−Of course, this all breaks down once the ``result'' of the predicate is ``defined'' in more than one predicate, and it is not applicable to those cases.
578+This means that we can syntactically replace \emph{type variables} with a portion of a predicate -- replace the variable with the definition. If we apply this technique to the type~\ref{eq:dotExample} we get the following type:
579+
580+\begin{equation}
581+ \forall \alpha. \; \alpha \rightarrow \alpha.\text{y}
582+\end{equation}
583+
584+When applied to the type~\ref{eq:updatePredExample} it yields:
585+
586+\begin{equation}
587+ \forall \alpha \beta. \; \alpha \rightarrow \beta \rightarrow (\alpha \update \beta)
588+\end{equation}
589+
590+We believe the derived type above are a lot easier to understand than their initial counterparts.
591+
592+\subsubsection{Implementation notes}
593+
594+For practical reasons, when applying the technique, there should be a threshold that limits the syntactic complexity of types that can be ``inlined''. This is due to the types being potentially as big as literals in the source expressions.
595+
596+Complexity of types should also be used as a heuristic in cases where there are multiple potential ``definitions'' for the same type variable – it is preferable to use the ``definitions'' with the lowest syntactic complexity as it leads to simpler types.
597+
598+\subsubsection{Limitations}
599+
600+The technique is not in applicable if the ``result'' of a predicate is not a type variable like in type \ref{eq:optFieldPredExample2}.
601+
602+Another 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.
570603
571604\section{Implementation} \label{sec:implementation}
572605