@@ -5,6 +5,7 @@
55\usepackage{hyperref}
66\usepackage{microtype}
77\usepackage{trfrac}
8+\usepackage{multirow}
89% \usepackage{caption}
910% \usepackage[main=english,russian]{babel}
1011
@@ -20,6 +21,7 @@
2021% \newfloat{figure}{hbp}{lst}
2122
2223\newcommand{\parr}[1]{\medskip\textbf{#1}\hspace{0.6cm}}
24+\newcommand{\strOrNum}{(\text{String} || \text{Number})}
2325
2426
2527% \year{2021}
@@ -282,7 +284,7 @@ in d
282284 \label{lst:let}
283285\end{figure}
284286
285−\subsection{With expression}
287+\subsection{With expression} \label{sec:withExp}
286288
287289\emph{With expressions} are a way to bring all values from an \emph{attribute set} into scope. It is conceptually very similar to \emph{let expressions} discussed in section~\ref{sec:let}. The syntax can be roughly describe like so: \texttt{with <set>; <body>} where \texttt{<set>} is an expression which evaluates to an \emph{attribute set} and all values from the set are available as definitions in the \texttt{<body>} expression. An example of a \emph{with expression} can be found in listing~\ref{lst:with}.
288290
@@ -411,7 +413,7 @@ Traditionally in languages similar to \emph{simply-typed lambda calculus} genera
411413
412414Apart from \emph{let expressions} Nix also has \emph{attribute sets} discussed in section~\ref{sec:attrSet}, definitions in which are semantically similar to those in \emph{let expressions}. \emph{Attribute set} definitions also seem like a good point for \emph{generalization}.
413415
414−\subsection{Inferring recursive types}
416+\subsection{Inferring recursive types} \label{sec:recLet}
415417
416418Recursive definitions pose a challenge for type inference without developer-supplied type annotations (which will be the case for the vast majority of code). There are three major approaches to inferring types of recursive definitions:
417419
@@ -509,7 +511,7 @@ We will not describe the row predicates we have chosen for Nix. Note the analogy
509511\newcommand{\update}{\mathbin{/\!\!/}}
510512\newcommand{\optDot}{.\!?}
511513
512−\paragraph{Attribute set field predicate}
514+\paragraph{Attribute set field predicate} \label{sec:attrSetPred}
513515
514516\begin{equation} \label{eq:fieldPred}
515517 \alpha. \text{x} = \beta
@@ -569,16 +571,45 @@ For this reason, we will have to define a smaller set of static types that will
569571 \centering
570572 \caption{Mapping from static types to dynamic types}
571573 \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
574+ \textbf{Static type} & \textbf{Dynamic types} \\ \hline \hline
575+ \multirow{3}{*}{String} & URI \\ \cline{2-2}
576+ & Path literal \\ \cline{2-2}
577+ & String \\ \hline \hline
578+ \multirow{2}{*}{Number} & Integer \\ \cline{2-2}
579+ & Float \\ \hline \hline
580+ Bool & Bool \\ \hline \hline
581+ Null & Null \\ \hline
577582 \end{tabular}
578583 \label{tbl:staticTypes}
579584\end{table}
580585
581−\subsection{Addition}
586+\begin{table*}[hbp]
587+ \centering
588+ \caption{Table of Nix Expression Language operators and their static types}
589+ \begin{tabular}{||c||c||c||c||} \hline
590+ \textbf{Operator} & \textbf{Operator description} & \textbf{Static type} \\ \hline \hline
591+ \texttt{-} & Numeric negation & $\text{Number} \rightarrow \text{Number}$ \\ \hline
592+ \texttt{!} & Boolean negation & $\text{Bool} \rightarrow \text{Bool}$ \\ \hline
593+ \texttt{++} & List concatenation & $\forall \alpha. \; [\alpha] \rightarrow [\alpha] \rightarrow [\alpha]$ \\ \hline
594+ \texttt{==} & Equality & $\forall \alpha. \; \alpha \rightarrow \alpha \rightarrow \text{Bool}$ \\ \hline
595+ \texttt{!=} & Not equality & $\forall \alpha. \; \alpha \rightarrow \alpha \rightarrow \text{Bool}$ \\ \hline
596+ \texttt{<} & Less than & $\text{Number} \rightarrow \text{Number} \rightarrow \text{Bool}$ \\ \hline
597+ \texttt{<=} & Less than or equal & $\text{Number} \rightarrow \text{Number} \rightarrow \text{Bool}$ \\ \hline
598+ \texttt{>} & Greater than & $\text{Number} \rightarrow \text{Number} \rightarrow \text{Bool}$ \\ \hline
599+ \texttt{>=} & Greater than or equal & $\text{Number} \rightarrow \text{Number} \rightarrow \text{Bool}$ \\ \hline
600+ \texttt{+} & Addition & $\forall \alpha. \; \strOrNum \sim \alpha \Rightarrow \alpha \rightarrow \alpha \rightarrow \alpha$ \\ \hline
601+ \texttt{-} & Subtraction & $\text{Number} \rightarrow \text{Number} \rightarrow \text{Number}$ \\ \hline
602+ \texttt{*} & Multiplication & $\text{Number} \rightarrow \text{Number} \rightarrow \text{Number}$ \\ \hline
603+ \texttt{/} & Division & $\text{Number} \rightarrow \text{Number} \rightarrow \text{Number}$ \\ \hline
604+ \texttt{\&\&} & Boolean ``and'' & $\text{Bool} \rightarrow \text{Bool} \rightarrow \text{Bool}$ \\ \hline
605+ \texttt{||||} & Boolean ``and'' & $\text{Bool} \rightarrow \text{Bool} \rightarrow \text{Bool}$ \\ \hline
606+ \texttt{->} & Implication & $\text{Bool} \rightarrow \text{Bool} \rightarrow \text{Bool}$ \\ \hline
607+ \texttt{//} & Attribute set update & $ \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma$ \\ \hline
608+ \end{tabular}
609+ \label{tbl:allOperators}
610+\end{table*}
611+
612+\subsection{Addition} \label{sec:addition}
582613
583614Among 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.
584615
@@ -586,8 +617,6 @@ Since our current implementation does not support sum types (see section~\ref{se
586617
587618The simplest approach is to introduce a simple predicate which is satisfied only if the argument is either of type \texttt{Number} or \texttt{String}:
588619
589−\newcommand{\strOrNum}{(\text{String} || \text{Number})}
590−
591620\begin{equation}
592621 \strOrNum \sim \alpha
593622\end{equation}
@@ -600,6 +629,12 @@ With this predicate the type of the addition operator (\texttt{+}) now becomes:
600629
601630\subsection{Typing rules}
602631
632+What follows is a formal description of the developed type system. For brevity we have omitted rules for typing literal constant values described in tables \ref{tab:atomicTypes} and \ref{tbl:staticTypes}, and most operators described in table~\ref{tbl:allOperators} as these rules are trivial.
633+
634+\subsubsection{Lists}
635+
636+After doing an informal analysis of existing Nix codebases we have concluded that it is not idiomatic to have heterogeneous lists in Nix. Thus, we have chosen to enforce homogenous lists in our static type system:
637+
603638\begin{equation}
604639 \trfrac
605640 {\Gamma \vdash e_1:\tau \quad \cdots \quad \Gamma \vdash e_n:\tau}
@@ -608,10 +643,14 @@ With this predicate the type of the addition operator (\texttt{+}) now becomes:
608643
609644\begin{equation}
610645 \trfrac
611− {\Gamma \vdash e_3:\tau \qquad \Gamma \vdash e_1 \update e_2 \sim e_3}
612− {\Gamma \vdash (e_2 \update e_2) : \tau}
646+ {\Gamma \vdash e_1:[\tau] \qquad \Gamma \vdash e_2 : [\tau]}
647+ {\Gamma \vdash (e_1 +\!\!+ \: e_2) : [\tau]}
613648\end{equation}
614649
650+\subsubsection{Lambda abstractions}
651+
652+Typing rules for both lambda abstraction definitions and application is common among type system derived from Hindley-Milner:
653+
615654\begin{equation}
616655 \trfrac
617656 {\Gamma \vdash e_1:\tau_1 \rightarrow \tau_2 \qquad \Gamma \vdash e_2 : \tau_1}
@@ -620,82 +659,145 @@ With this predicate the type of the addition operator (\texttt{+}) now becomes:
620659
621660\begin{equation}
622661 \trfrac
623− {\Gamma \vdash e_1:[\tau] \qquad \Gamma \vdash e_2 : [\tau]}
624− {\Gamma \vdash (e_1 +\!\!+ \: e_2) : [\tau]}
662+ {\Gamma, \text{x}: \tau_1 \vdash e : \tau_2}
663+ {\Gamma \vdash (\text{x: } e) : \tau_1 \rightarrow \tau_2}
625664\end{equation}
626665
666+\subsubsection{Addition}
667+
668+The rational for having a special case for the addition operator is layed out in section~\ref{sec:addition}:
669+
627670\begin{equation}
628671 \trfrac
629672 {\Gamma \vdash e_1:\tau \qquad \Gamma \vdash e_2 : \tau \qquad \Gamma \vdash (\text{String} || \text{Number}) \sim \tau}
630673 {\Gamma \vdash (e_1 + e_2) : \tau}
631674\end{equation}
632675
676+\subsubsection{Conditional expressions}
677+
678+Conditionals are also very similar to what is described in the Hindley–Milner type system:
679+
633680\begin{equation}
634681 \trfrac
635− {\Gamma \vdash e.\text{x} = \tau}
636− {\Gamma \vdash (e.\text{x}) : \tau}
682+ {\Gamma \vdash e_1 : \text{Bool} \qquad \Gamma \vdash e_2 : \tau \qquad \Gamma \vdash e_3 : \tau}
683+ {\Gamma \vdash (\text{if} \; e_1 \; \text{then} \; e_2 \; \text{else} \; e_3) : \tau}
637684\end{equation}
638685
686+\subsubsection{\texttt{let}-generalization}
687+
688+Just like in many functional type systems, our type system will support let-generalization -- constants bound in a \texttt{let} expression are generalized as much as possible. All free type variables that were defined while inferring an expression are closed over.
689+
690+A simple version of rule is as follows:
691+
639692\begin{equation}
640693 \trfrac
641− {\Gamma \vdash e.\text{x} = \tau}
642− {\Gamma \vdash (e \optDot \text{x}) = \tau}
694+ {\Gamma \vdash e_1 : \tau_1 \qquad \Gamma, (\text{x}: \forall \{\text{ftv}(\tau_1) - \text{ftv}(\Gamma)\}. \; \tau_1) \vdash e_2 : \tau_2}
695+ {\Gamma \vdash (\text{let} \; \text{x = } e_1; \; \text{in} \; e_2) : \tau_2}
643696\end{equation}
644697
698+where $\text{fvt}(\alpha)$ is the set of all free variables that occur in $\alpha$.
699+
700+Of course, this does not cover all possible syntactic constructs -- it is only concerned with inferring a single declaration. It is trivially extendable to a series of independent declarations. Inferring recursive declarations is discussed in section~\ref{sec:recLet}.
701+
702+Inferring \emph{let expressions} trivially extends to inferring fields of \emph{attribute sets} and is omitted for brevity.
703+
704+\subsubsection{Instantiation}
705+
706+When using expressions with generalized types, we need to instantiate theme to concrete types:
707+
645708\begin{equation}
646709 \trfrac
647− {\Gamma \vdash e_2 : \tau \qquad \Gamma \vdash e_1 \optDot \text{x} = \tau}
648− {\Gamma \vdash (e.\text{x} \; \text{or} \; e_2) : \tau}
710+ {\Gamma \vdash e : \forall \alpha. \; \tau_1}
711+ {\Gamma \vdash e: [\alpha \rightarrow \tau_2] \tau_1}
649712\end{equation}
650713
714+where $[\alpha \rightarrow \beta]\gamma$ denotes the result of substituting all free occurrences of $\alpha$ in $\gamma$ with $\beta$.
715+
716+\subsubsection{Attribute sets}
717+
718+Basic \emph{attribute set} operations are now trivially expressible through the predicate defined in section~\ref{sec:attrSetPred}:
719+
651720\begin{equation}
652721 \trfrac
653− {\Gamma \vdash e \optDot \text{x} = \tau}
654− {\Gamma \vdash (e \; \text{?} \; \text{x}) : \text{Bool}}
722+ {\Gamma \vdash e_1 : \tau_1 \qquad \Gamma \vdash e_2 : \tau_2 \qquad \Gamma \vdash \tau_1 \update \tau_2 \sim \tau_3}
723+ {\Gamma \vdash (e_1 \update e_2) : \tau_3}
655724\end{equation}
656725
657726\begin{equation}
658727 \trfrac
659− {\Gamma \vdash e_1 : \tau_1 \qquad \Gamma, (\text{x}: \forall \{\text{ftv}(\tau_1) - \text{ftv}(\Gamma)\}. \; \tau_1) \vdash e_2 : \tau_2}
660− {\Gamma \vdash (\text{let} \; \text{x = } e_1; \; \text{in} \; e_2) : \tau_2}
728+ {\Gamma \vdash e.\text{x} = \tau}
729+ {\Gamma \vdash (e.\text{x}) : \tau}
661730\end{equation}
662731
663732\begin{equation}
664733 \trfrac
665− {\Gamma \vdash e : \forall \alpha. \; \tau_1}
666− {\Gamma \vdash e: [\alpha \rightarrow \tau_2] \tau_1}
734+ {\Gamma \vdash e_2 : \tau \qquad \Gamma \vdash e_1 \optDot \text{x} = \tau}
735+ {\Gamma \vdash (e.\text{x} \; \text{or} \; e_2) : \tau}
667736\end{equation}
668737
669738\begin{equation}
670739 \trfrac
671− {\Gamma, \text{x}: \tau_1 \vdash e : \tau_2}
672− {\Gamma \vdash (\text{x: } e) : \tau_1 \rightarrow \tau_2}
740+ {\Gamma \vdash e \optDot \text{x} = \tau}
741+ {\Gamma \vdash (e \; \text{?} \; \text{x}) : \text{Bool}}
673742\end{equation}
674743
744+When defining typing rules for \emph{attribute sets} we will use the notion of rows similar to what is used in the \emph{Rose} paper~\cite{morris2019abstracting}: for typing purposes an attribute set will be defined as a product of a set of \emph{rows} – key-value pairs: $\Pi \xi$ where $\xi$ is a set of \emph{rows}.
745+
746+A key-value pair will be denoted as $\text{x} = \alpha$ where `x' is the name of a field and $\alpha$ is the type of the field.
747+
748+Of course, a \emph{set of rows} can not contain multiple \emph{rows} with the same key.
749+
750+With that we can define how those predicate are actually satisfied:
751+
675752\begin{equation}
676753 \trfrac
677− {\Gamma \vdash e_1 : \text{Bool} \qquad \Gamma \vdash e_2 : \tau \qquad \Gamma \vdash e_3 : \tau}
678− {\Gamma \vdash (\text{if} \; e_1 \; \text{then} \; e_2 \; \text{else} \; e_3) : \tau}
754+ {(\text{x} = \tau) \in \xi}
755+ {(\Pi \xi).\text{x} = \tau}
679756\end{equation}
680757
681758\begin{equation}
682759 \trfrac
683− {\Gamma \vdash e : \tau \qquad \{\text{x} = e;\} \in \xi}
684− {\Gamma \vdash (\Pi \xi).\text{x} = \tau}
760+ {\text{x} \notin \xi}
761+ {(\Pi \xi) \optDot \text{x} = \tau}
685762\end{equation}
686763
687764\begin{equation}
688765 \trfrac
689− {\text{x} \notin \xi}
690− {(\Pi \xi) \optDot \text{x} = \tau}
766+ {\Gamma \vdash e.\text{x} = \tau}
767+ {\Gamma \vdash (e \optDot \text{x}) = \tau}
768+\end{equation}
769+
770+where $(\text{x} = \tau) \in \xi$ denotes the presence of the \emph{row} $(\text{x} = \tau)$ in the \emph{set} $\xi$, and $\text{x} \notin \xi$ denotes the absence of a \emph{row} with the key `x' in the \emph{set} $\xi$.
771+
772+The definition of the ``update'' predicate uses standard set comprehension notation:
773+
774+\begin{equation}
775+ \trfrac
776+ {}
777+ {\Pi \xi_1 \update \Pi \xi_2 \sim \Pi (\xi_2 \cup \{a = \tau || (a = \tau) \leftarrow \xi_1, a \notin \xi_2\})}
691778\end{equation}
692779
780+\subsubsection{with expressions}
781+
782+\emph{with expressions} discussed in section~\ref{sec:withExp} are not difficult to define a typing rule for:
783+
693784\begin{equation}
694785 \trfrac
695− {\Gamma, \xi \vdash e : \tau}
696− {\Gamma \vdash (\text{with } (\Pi \xi)\text{; } e) : \tau}
786+ {\Gamma \vdash e_1: \Pi \xi \qquad \Gamma, \xi \vdash e_2 : \tau}
787+ {\Gamma \vdash (\text{with } e_1\text{; } e_2) : \tau}
697788\end{equation}
698789
790+\emph{with expressions} do, however, pose a particularly hard problem when implementing the type system – we can't always statically know the fields in $e_1$ -- it can be passed in as a function argument. This means that the typing environment of a function can depend on its argument. Implementing this in a wholistic manner would require our type system support a form of dependent types. That is not a direction we want to pursue -- introducing dependent types would greatly complicate the type system to a point where automated type inference would not practical and the type system would be a lot harder to work with.
791+
792+Instead, we opted to define a heuristic which in our testing was proven to cover most practical cases: when encountering a variable in the body of a with expression:
793+
794+\begin{enumerate}
795+ \item if a variable was defined in the body of the with expression and is in scope, return that type
796+ \item if the \emph{attribute set} from the \emph{with expression} is statically known and defined a key with the appropriate name then return that types
797+ \item if the \emph{attribute set} from the \emph{with expression} is not statically known and the outer context of the \emph{with expression} contains a variable with the appropriate name, return that type
798+ \item else, create a constraint that the first operand in the \emph{with expression} contains a field with the appropriate name and type
799+\end{enumerate}
800+
699801\section{Implementation} \label{sec:implementation}
700802
701803\cite{github-source}