@@ -516,7 +516,7 @@ The type $\alpha$ should be an attribute set and it should contain a field $x$ o
517The term \texttt{x: x.y} would field the following type:
517The term \texttt{x: x.y} would field the following type:
519−\begin{equation}
519+\begin{equation} \label{eq:dotExample}
520 \forall \alpha \beta. \; \alpha.\text{y} = \beta \Rightarrow \alpha \rightarrow \beta
520 \forall \alpha \beta. \; \alpha.\text{y} = \beta \Rightarrow \alpha \rightarrow \beta
521\end{equation}
521\end{equation}
@@ -530,7 +530,7 @@ The type $\alpha$ should be an attribute set and if it contains the field $x$, t
531The term \texttt{x: x.y or 1} would field the following type:
531The term \texttt{x: x.y or 1} would field the following type:
533−\begin{equation}
533+\begin{equation} \label{eq:optFieldPredExample}
534 \forall \alpha. \; \alpha \optDot \text{y} = \text{Number} \Rightarrow \alpha \rightarrow \text{Number}
534 \forall \alpha. \; \alpha \optDot \text{y} = \text{Number} \Rightarrow \alpha \rightarrow \text{Number}
535\end{equation}
535\end{equation}
@@ -538,7 +538,7 @@ This predicate also arises from the use of the \emph{attribute set field presenc
539The term \texttt{x: x ? y} would field the following type:
539The term \texttt{x: x ? y} would field the following type:
541−\begin{equation}
541+\begin{equation} \label{eq:optFieldPredExample2}
542 \forall \alpha \beta. \; \alpha \optDot \text{y} = \beta \Rightarrow \alpha \rightarrow \text{Bool}
542 \forall \alpha \beta. \; \alpha \optDot \text{y} = \beta \Rightarrow \alpha \rightarrow \text{Bool}
543\end{equation}
543\end{equation}
@@ -550,23 +550,56 @@ The term \texttt{x: x ? y} would field the following type:
551All $\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}.
551All $\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}.
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:
555−\begin{equation}
555+\begin{equation} \label{eq:updatePredExample}
556− \forall \alpha \beta. \; \alpha \optDot \text{y} = \beta \Rightarrow \alpha \rightarrow \text{Bool}
556+ \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma
557\end{equation}
557\end{equation}
559−\subsubsection{Making predicates more user-friendly}
559+\subsection{Making predicates more user-friendly}
561+\subsubsection{A novel technique}
561The 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.
563The 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.
565+The technique is based on the fact that a type variable by itself can only convey the following information:
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
563Note that all of what follows is only concerned with syntactic constructs. It does in no way alter the semantic of the predicates described above.
572Note that all of what follows is only concerned with syntactic constructs. It does in no way alter the semantic of the predicates described above.
565We 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}.
574We 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}.
567The 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.
576The 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.
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:
581+ \forall \alpha. \; \alpha \rightarrow \alpha.\text{y}
584+When applied to the type~\ref{eq:updatePredExample} it yields:
587+ \forall \alpha \beta. \; \alpha \rightarrow \beta \rightarrow (\alpha \update \beta)
590+We believe the derived type above are a lot easier to understand than their initial counterparts.
592+\subsubsection{Implementation notes}
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.
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.
598+\subsubsection{Limitations}
600+The technique is not in applicable if the ``result'' of a predicate is not a type variable like in type \ref{eq:optFieldPredExample2}.
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.
571\section{Implementation} \label{sec:implementation}
604\section{Implementation} \label{sec:implementation}