@@ -0,0 +1,330 @@
1+\PassOptionsToPackage{main=english,russian}{babel}
2+
3+\documentclass[]{TechDoc}
4+
5+\usepackage{float}
6+
7+\selectlanguage{english}
8+
9+\floatstyle{boxed}
10+\newfloat{Listing}{hbp}{lst}
11+
12+\newcommand{\parr}[1]{\medskip\textbf{#1}\hspace{0.6cm}}
13+
14+%include polycode.fmt
15+
16+\title{Static analyzer for the Nix Expression Language}
17+\author{Студент группы БПИ 174}{И. И. Костюченко}
18+% \academicTeacher{Доцент департамента программной инженерии факультета компьютерных наук, канд. техн. наук}{Х. М. Салех}
19+
20+% \documentTitle{Техническое задание}
21+% \documentCode{RU.17701729.04.03-01 ТЗ 01-1}
22+
23+\begin{document}
24+\maketitle
25+
26+\begin{abstract}
27+ Configuring and building even the most straightforward software projects is often not simple -- it requires downloading and installing copious amounts of prerequisite software. This often makes reproducing builds of a project on different machines problematic. The Nix package manager aims to address this problem by providing a unified language for describing software packages in a purely functional way. This language is called the Nix Expression Language. Since all of the complexity of software configuration needs to be expressed in the Nix Expression Language, the expressions themselves often become quite complicated, making it difficult to understand and extend existing expressions without introducing errors. A widespread tool for easing the understandability and correctness of expressions in other languages is static type checking. This paper will explore the techniques that can be used to add static type checking to the Nix Expression Language.
28+\end{abstract}
29+
30+\newpage
31+
32+\tableofcontents
33+
34+\section*{Introduction}
35+
36+Today developing software is riddled with large amounts of complexity -- newer software is built on top of older software, dragging the whole stack below as dependencies. As a result, building software requires a large number of dependencies to be preinstalled. Modern build systems like Gradle\footnote{\url{https://gradle.org}}, Maven\footnote{\url{https://maven.apache.org}}, and Stack\footnote{\url{https://docs.haskellstack.org/en/stable/README/}} try to mitigate the issue by automatically downloading and installing the required dependencies. However, in most cases, such tools can only manage language-level dependencies, requiring the user to install additional libraries and tools manually.
37+
38+Such manual dependency management leads to several problems. Firstly, when a user wants to work on a project he has not encountered before, he will have to install the required dependencies, leading to additional tedious work. Furthermore, the required versions of project dependencies might conflict with the versions that another project requires. The user will have to manually switch the versions of executables and libraries when switching between projects.
39+
40+This problem is partially solved by so-called virtual environments tools. A virtual environment is a way of restricting and customizing the available external tools (usually compilers) with the ability to dynamically switch between them. The tools can generally be split into one of two categories:
41+
42+\begin{enumerate}
43+ \item \emph{language-specific tools} which simplify installing and switching between different versions of some tools (usually compilers). Examples of such tools are:
44+ \begin{enumerate}
45+ \item |rustup|\footnote{\url{https://github.com/rust-lang/rustup}} for Rust tools
46+ \item |ghcup|\footnote{\url{https://www.haskell.org/ghcup/}} for Haskell tools
47+ \item |Ruby Version Manager|\footnote{\url{http://rvm.io}} for Ruby tools
48+ \end{enumerate}
49+ \item \emph{general-purpose tools} which automate switching the available tools (or versions of tools) that have been previously installed in some other way:
50+ \begin{enumerate}
51+ \item |direnv|\footnote{\url{https://direnv.net}}
52+ \item |autoenv|\footnote{\url{https://github.com/inishchith/autoenv}}
53+ \item |asdf|\footnote{\url{https://github.com/asdf-vm/asdf}}
54+ \item |ondir|\footnote{\url{https://github.com/alecthomas/ondir}}
55+ \end{enumerate}
56+\end{enumerate}
57+
58+Even so, such tools still require explicit user action: the user needs to explicitly switch between (or install) the necessary tools when switching projects in the case of \emph{language-specific tools}, the user needs to explicitly install the required tools in some other way for them to be imported by \emph{general-purpose tools}.
59+
60+Secondly, manual dependency management impedes the reproducibility of the project builds -- building the same project on multiple machines will, in all likelihood, produce different results since the machines will likely differ in many ways that impact the build, such as having slightly different versions\footnote{``Version'' here refers to actual variations on the bit level, and not just version numbers.} of libraries and executables.
61+
62+Nix~\cite{dolstra2008nixos} attempts to solve the problems mentioned above by describing software project builds in a generic and language-agnostic way. Furthermore, the resulting descriptions define the build process in a complete and deterministic way -- everything that impacts the build in any way needs to be explicitly defined, even system-level libraries are reproducible on the bit level.
63+
64+Defining the build process in such a detailed and pedantic manner is not generally easy and often requires large amounts of boilerplate, which provides much room for error. While most build systems define project builds with static configurations using formats such as YAML~\cite{ben2009yaml}, Nix employs a fully-fledged programming language as its configuration language. This programming language is called the Nix Expression Language\footnote{\url{https://nixos.wiki/wiki/Nix_Expression_Language}}.
65+
66+Using a fully-fledged programming language allows the users to reuse common definitions and create new domain-specific abstractions. This helps to mitigate a lot of the aforementioned potential problems.
67+
68+Nix Expression Language is a dynamic, lazy, purely functional programming language. The purely functional nature of the language aids in build reproducibility guarantees that Nix aims to provide.
69+
70+Even considering the tremendous benefits that using a programming language for build configuration brings, the dynamic nature of the language often still makes it challenging to understand and reuse existing code. This is in part due to the large amounts of code required to describe real-world systems in all of their complexity fully.\footnote{The standard Nix package repository |nixpkgs| contains 2 million lines of code.}
71+
72+Refactoring existing code is also tricky since the generated expressions are only really checked for correctness\footnote{Here, ``correctness'' is used to mean the absence of evaluation-time errors.} at their evaluation time, and the evaluation time of expressions is difficult to predict due to the lazy nature of the language.
73+
74+Static type checking is the process of analyzing the types of expressions and detecting type errors in programs without evaluating them.
75+
76+Even though static type checking in most mainstream programming languages does not influence the semantics of the programs, it is nonetheless widely used. This is an indication of the usefulness of static type checking during development. Type checking helps detect likely ``incorrect'' programs without evaluating them (very helpful during refactoring), and aids in understanding existing code since types often expose some semantics of expressions (this is especially true for purely functional programs).
77+
78+The Nix Expression Language does not currently support static type checking of any kind. Of course, retrofitting a static type checker onto an existing dynamic programming language will reject programs that will not produce errors at runtime. However, this is still a goal worth pursuing because even with all of the situations when the type checker produces false negatives, inferring types for existing expressions, as mentioned above, will aid in understanding existing code and surface potentially problematic areas of code to the developer.
79+
80+\section{Nix Expression Language}
81+
82+In this chapter we will examine the semantics of major terms of the Nix Expression Language. We will from now on abbreviate \emph{Nix Expression Language} as \emph{Nix} as it is in most cases clear from the context what is being referred to: the language or the system as a whole.
83+
84+\subsection{Atomic types}
85+
86+Atomic types are described in table~\ref{tab:atomicTypes}.
87+
88+\begin{table}[hbp]
89+ \centering
90+ \begin{tabular}{ ||c||p{6cm}||p{6cm}|| } \hline
91+ \textbf{Atomic type} & \textbf{Description} & \textbf{Example terms} \\ \hline
92+ URI & A string literal representing a URI. Does not require quoting. & \texttt{https://example.com} \\ \hline
93+ Path literal & A path literal referring to either a relative or absolute path. Does not require quoting. & \texttt{../../directory/file.txt} \\ \hline
94+ Integer & The current C implementation of Nix allows values of 64-bit signed integers. & \texttt{69} \newline \texttt{-42} \\ \hline
95+ Float & Floating point integers. & \texttt{42.9} \newline \texttt{-69.42} \\ \hline
96+ Bool & Boolean values. & \texttt{true} \newline \texttt{false} \\ \hline
97+ Null & A type with a single value. & \texttt{null} \\ \hline
98+ \end{tabular}
99+ \caption{Table of atomic Nix Expression Language types}
100+ \label{tab:atomicTypes}
101+\end{table}
102+
103+\subsection{Strings}
104+
105+\subsubsection{Double quoted string literals}
106+
107+Double quoted string literals are string literals just like in many other programming languages. It can contain esaped newline character literals \texttt{\\n} which will be preserved as shown in listing~\ref{lst:newlineString}.
108+
109+\begin{Listing}
110+ \begin{minipage}{\textwidth}
111+ \begin{verbatim}
112+"Sampel\nPalnet"
113+ \end{verbatim}
114+ \end{minipage}
115+ \caption{Nix Expression Language double quoted string literal example}
116+ \label{lst:newlineString}
117+\end{Listing}
118+
119+\subsubsection{Multiline string literals}
120+
121+Multiline string literals are enclosed by pairs of single quotes (\texttt{''} as opposed to \texttt{"}). Newlines are preserved and indentation is stripped from the beginning of the literal. An example multiline string literal is shown in listing~\ref{lst:multilineString}.
122+
123+\begin{Listing}
124+ \begin{minipage}{\textwidth}
125+ \begin{verbatim}
126+''
127+Sampel
128+Palnet''
129+
130+"Sampel\nPalnet"
131+ \end{verbatim}
132+ \end{minipage}
133+ \caption{Nix Expression Language multiline string literal example and an equivalent double quoted string literal}
134+ \label{lst:multilineString}
135+\end{Listing}
136+
137+\subsubsection{String interpolation}
138+
139+The Nix Expression Language also allows for arbitrary expressions of the language to be interpolated in string using the following syntax: \texttt{\$\{ <expression> \}} where \texttt{<expression>} is a Nix expression.An example of string interpolation is show in listing~\ref{lst:stringInterpolation}.
140+
141+\begin{Listing}
142+ \begin{minipage}{\textwidth}
143+ \begin{verbatim}
144+"one is ${ if 1 == 2 then "equal" else "not equal" } to two."
145+
146+"one is not equal to two."
147+ \end{verbatim}
148+ \end{minipage}
149+ \caption{Nix Expression Language string interpolation example with the resulting string.}
150+ \label{lst:stringInterpolation}
151+\end{Listing}
152+
153+\subsection{Lists}
154+
155+Nix support a list type. List literals are enclosed by square brackets \texttt{[]} and the elements are separated by whitespace. Examples of list literals are shown in listing~\ref{lst:list}.
156+
157+\begin{Listing}
158+ \begin{minipage}{\textwidth}
159+ \begin{verbatim}
160+[1 2 "hello" ../../file.txt https://example.com]
161+ \end{verbatim}
162+ \end{minipage}
163+ \caption{Nix Expression Language List literals.}
164+ \label{lst:list}
165+\end{Listing}
166+
167+\subsection{Attribute sets} \label{sec:attrSet}
168+
169+An attribute set is internally implemented as a hashmap with strings as keys where values can be arbitrary expressions. An example attribute set literal is shown in listing~\ref{lst:attrSet}.
170+
171+\begin{Listing}
172+ \begin{minipage}{\textwidth}
173+ \begin{verbatim}
174+{ a = 42;
175+ b = 6 + 9;
176+ c = ../file.txt;
177+ d = "henlo, world";
178+}
179+ \end{verbatim}
180+ \end{minipage}
181+ \caption{Nix Expression Language attribute set literals.}
182+ \label{lst:attrSet}
183+\end{Listing}
184+
185+\subsection{Recursive attribute sets} \label{sec:recAttrSet}
186+
187+While ordinary \emph{attribute sets} from discussed in section~\ref{sec:attrSet} can only reference values defined outside of the attribute set literal, \emph{recursive attribute sets} can also reference values defined in the attribute set literal itself. The keys of the attribute set are essentially available in scope of the attribute set values. An example of \emph{recursive attribute set} are given in listing~\ref{lst:recAttrSet}. Note that it is syntactically distiguished form normal \emph{attribute set} literals by the \texttt{rec} key word at the beginning.
188+
189+\begin{Listing}
190+ \begin{minipage}{\textwidth}
191+ \begin{verbatim}
192+rec {
193+ a = 42;
194+ b = a + 9;
195+ c = world;
196+ d = "henlo, ${c}";
197+}
198+ \end{verbatim}
199+ \end{minipage}
200+ \caption{Nix Expression Language recursive attribute set literals.}
201+ \label{lst:recAttrSet}
202+\end{Listing}
203+
204+\subsection{Let expressions} \label{sec:let}
205+
206+A \emph{let expression} has two parts: the \emph{declarations} and the \emph{body}. The format can be roughly described like so: \texttt{let <definitions> in <body>}. A \emph{let expression} allows us to define values in the \emph{declarations} that can be reused in the \emph{body} of the expression. Just like \emph{recursive attribute sets} from section~\ref{sec:recAttrSet} all declared values are available in scope in the defined expressions. An example of \emph{let expressions} is available in listing~\ref{lst:let}.
207+
208+\begin{Listing}
209+ \begin{minipage}{\textwidth}
210+ \begin{verbatim}
211+let
212+ c = world;
213+ d = "henlo, ${c}";
214+in d
215+ \end{verbatim}
216+ \end{minipage}
217+ \caption{Nix Expression Language \emph{let} expression literals.}
218+ \label{lst:let}
219+\end{Listing}
220+
221+\subsection{With expression}
222+
223+\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}.
224+
225+\begin{Listing}
226+ \begin{minipage}{\textwidth}
227+ \begin{verbatim}
228+let
229+ c = world;
230+ d = "henlo, ${c}";
231+in d
232+ \end{verbatim}
233+ \end{minipage}
234+ \caption{Nix Expression Language \emph{with} expression literals.}
235+ \label{lst:with}
236+\end{Listing}
237+
238+\section{Existing typecheckers}
239+
240+In this section we will examine existing attempts at developing a typechecker for the Nix Expression Language, determine the features of the implemented type systems and assess how well maintained are the implementations.
241+
242+\subsection{regnat/tix} \label{sec:regnat/tix}
243+
244+regnat/tix\footnote{\url{https://github.com/regnat/tix}} is an implementation of typechecker for the \emph{Nix Expression Language} implemented in \emph{OCaml}\footnote{\url{https://ocaml.org}}. The type checker itself is implemented on a different much simpler language named \emph{Nix Light}. To typecheck a normal \emph{Nix} program(expression) the program need to be first converted to an equivalent \emph{Nix Light} program. The type checker has a row-polymorphism-inspired feature: records are represented as a product of one-row types. In \emph{Nix Light} lists are represented as a single-liked heterogeneous list. The type system does not have support for parametric polymorphism in favour of a gradual typing paradigm.
245+
246+\parr{Status} The last commit was published in 2017 and the project is now abandoned in favour of regnat/ptyx which we examin in section~\ref{sec:regnat/ptyx}.
247+
248+\subsection{regnat/ptyx} \label{sec:regnat/ptyx}
249+
250+regnat/ptyx\footnote{\url{https://github.com/regnat/ptyx}} is in essence a reimplementation of regnat/tix in Haskell\footnote{\url{https://www.haskell.org}} which we examined in section~\ref{sec:regnat/tix}. The basic ideas and techniques are the same. In fact, so much so, that the simpler language is also called \emph{Nix Light} and \emph{Nix} expression are also converted to it before type checking. There is still no support for parametric polymorphism.
251+
252+\parr{Status} The last commit was published in 2018. Unsupported language features include lists and attribute sets.
253+
254+\subsection{haskell-nix/hnix}
255+
256+haskell-nix/hnix\footnote{\url{https://github.com/haskell-nix/hnix}} is primarily not a typechecker, but rather the goal of the project is to fully reimplement the \emph{Nix Expression Language} interpreter in \emph{Haskell}. There is, however a number of modules dedicated to a typechecker implementation which was migrated into the project. Contrary to how it may seem, the typechecker is not integrated with the rest of the project in any significant way. The type system itself is based on the Hindley-Milner type system. However, the type system was not extended with additional features to better support the dynamic nature of \emph{Nix}. For instance, there is no support for row-polymorphism which greatly impedes typechecking any code that interacts with \emph{attribute sets} in any way.
257+
258+\parr{Status} Last time the typechecker was modified in any substantial way was in 2019. It does not appear to be actively developed. Furthermore, there is no description of the implemented type system.
259+
260+
261+\section{Existing Approaches}
262+
263+\subsection{Type System Approach}
264+
265+There has been much research done in the field of type systems for functional programming languages. The most notable contribution was the introduction of the Damas-Milner\footnote{The Damas-Milner type system is sometimes referred to as the Hindley–Milner type system.} type system and the W inference algorithm~\cite{damas1982principal}, which was later proven to be sound and complete~\cite{vaughanproof}.
266+
267+The Damas-Milner type system is a type system for lambda calculus with parametric polymorphism. The most notable property of the Damas-Milner type system is the proven ability of the W algorithm to infer the most general types without any user-provided type annotations.
268+
269+While the Damas-Milner describes a simple language, it is robust enough to be used as the basis for more advanced type systems such as the one used in the Haskell programming language~\cite{jones1999typing}, which extends the Damas-Milner type system in many ways which break the excellent properties it provides but remains extremely useful in practice.
270+
271+Since the Nix Expression Language is a relatively simple functional programming language, extending the Damas-Milner type system and algorithms to fit the language will be the approach we take as the tried and true method.
272+
273+\subsection{Type Checker Error Handling}
274+
275+Due to the inevitable presence of false negatives during type checking, for the type checker to be useful enough to be worth implementing, the algorithm should gracefully recover after encountering expressions that it deems to be ``wrong''.
276+
277+Since the interpreter of the programs will not be related to the developed type checker in any way, the type checker can not influence the semantics of the programs. This fact can be used to implement the following failure recovery heuristic: when the type checker encounters an expression that yields type checking errors, the errors are collected to be displayed to the user, and the expression is given the least general type possible such that it does not yield type errors.
278+
279+This is, in general, always possible since any syntactically valid expression will be correct with respect to types if every subexpression is assigned the polymorphic type:
280+
281+\begin{equation}
282+ \forall \alpha. \alpha
283+\end{equation}
284+
285+In some cases, this approach will likely yield too little information to be useful, but it seems like a reasonable solution.
286+
287+\subsection{Improving Type Checker Error Reporting}
288+
289+The original W inference algorithm is a single-stage inference algorithm, meaning that it attempts to satisfy type constraints as soon as it encounters them. A consequence of this is that errors are reported as soon as they are encountered. Often, the information available about the program at the time the error had occurred is very limited due to not all of the program being processed. This leads to poor error reporting.
290+
291+In contrast to the single-stage algorithm, the two-stage algorithm~\cite{jones2005practical,serrano2016type} collects the type constraints as the first stage of type checking and solves the collected constraints as a second step. This leads to most errors occurring during the second stage when all available type information has already been collected. As a result, better type errors are produced. This is the preferable approach for our goals.
292+
293+\subsection{Row-Polymorphism}
294+
295+One of the language-level constructs in the Nix Expression Language is the ``attribute set'' which can be thought of as a first-class hashmap with strings as keys. In combination with the dynamic nature of the language, these ``attribute sets'' have the semantics of row-polymorphic records.
296+
297+There has been some research conducted in the field of type systems with row-polymorphic records~\cite{morris2019abstracting,leijen2005extensible}. The approach that should be taken in developing a static type checker for the Nix Expression Language is describing row-polymorphic attribute sets with a construct similar\footnote{The way it should be displayed to the user will be distinct, since, unlike in Haskell, the Nix Expression Language does not have constraints as a language construct.} to Haskell constraints~\cite{orchard2010haskell}.
298+
299+\subsection{Message Reporting}
300+
301+Displaying errors to the user is not as simple as it might initially seem. For the type checker to be as helpful as possible, error messages should display the encountered issues in the language contexts in which they had occurred. Ideally, the errors should point to the exact terms that are most likely problematic.
302+
303+Even if all of the information necessary for detailed error messages is collected during type checking, displaying errors to the user is a problem that deserves its own research\footnote{This also relates to how types are laid out when displaying to the user even when no errors have occurred.}. The users might have different screen sizes. The error message should reflow all of the displayed text, code, and type annotations to accommodate the available space.
304+
305+Hughes introduced a general-purpose algebraic pretty-printer~\cite{hughes1995design}, which was later improved upon~\cite{wadler2003prettier}, to solve precisely this problem. Using one of the pretty-printers based on that research is the industry standard and will be used by our type checker.
306+
307+\subsection{Language Server Architecture}
308+
309+A Language Server is a server providing language-specific code analysis. It communicates with various code editors using the Language Server Protocol\footnote{\url{https://microsoft.github.io/language-server-protocol/}}.
310+
311+Language Servers have received wide adoption across a large variety of programming languages. Integrating the developed type checker into a Language Server with ``go-to-definition'' and ``show types on hover'' support would significantly improve the experience of developing in the Nix Expression Language.
312+
313+One of the actively developed language servers is the Haskell Language Server\footnote{\url{https://github.com/haskell/haskell-language-server}}. To manage the complexities of tracking changes in files and dependencies between them, the Haskell Language Server employs the Shake library~\cite{mitchell2012shake}. It is described as an alternative to Make\footnote{\url{https://www.gnu.org/software/make/}} embedded as a DSL into Haskell with the ability to dynamically update the dependency tree, among other improvements.
314+
315+As it is already tested as the basis for a Language Server implementation, building our Language Server on top of the Shake library seems like the correct architectural decision.
316+
317+\subsection{Conclusion}
318+
319+Nix 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.
320+
321+Even though the developed type checker will need to check code for an existing dynamic language, and no type checker can cover all of the valid cases, producing false negatives, covering most of the cases encountered in practice would be useful enough to be worth using. Furthermore, plenty of research has already been conducted on which the Nix Expression Language type checker can be based.
322+
323+Integrating the type checker into a Language Server would provide additional utility and afford the ability to implement additional features, such as ``go-to-definition'' in a practical way.
324+
325+\bibliographystyle{gost2008}
326+\bibliography{bibl}
327+
328+\registrationList
329+
330+\end{document}