@@ -1,28 +1,42 @@
1−\PassOptionsToPackage{main=english,russian}{babel}
1+\documentclass[a4paper,conference]{IEEEtran}
22
3−\documentclass[]{TechDoc}
4−
5−\usepackage{float}
3+% \usepackage{float}
64\usepackage{mathtools}
5+\usepackage{hyperref}
6+\usepackage{microtype}
7+% \usepackage{caption}
8+% \usepackage[main=english,russian]{babel}
9+
10+% \selectlanguage{english}
11+
12+% \sectionsAreChapters
713
8−\selectlanguage{english}
914
10−\sectionsAreChapters
15+%include polycode.fmt
16+
1117
12−\floatstyle{boxed}
13−\newfloat{Listing}{hbp}{lst}
18+% \floatstyle{boxed}
19+% \newfloat{figure}{hbp}{lst}
1420
1521\newcommand{\parr}[1]{\medskip\textbf{#1}\hspace{0.6cm}}
1622
17−%include polycode.fmt
1823
19−\year{2021}
24+% \year{2021}
2025\title{Static analyzer for the Nix Expression Language}
21−\author{Student, BSE174}{I. I. Kostyuchenko}
22−\academicTeacher{Associate Professor, PhD}{V. V. Kuliamin}
23−
24−\documentTitle{Explanatory note}
25−\documentCode{RU.17701729.04.05-01 ПЗ 01-1}
26+% \author{Student, BSE174}{I. I. Kostyuchenko}
27+% \academicTeacher{Associate Professor, PhD}{V. V. Kuliamin}
28+
29+% \documentTitle{Explanatory note}
30+% \documentCode{RU.17701729.04.05-01 ПЗ 01-1}
31+
32+\author{
33+ \IEEEauthorblockN{Kostyuchenko Ilya}
34+ \IEEEauthorblockA{
35+ Faculty of Computer Science,\\
36+ Higher School of Economics,\\
37+ Moscow, Russia
38+ }
39+}
2640
2741\begin{document}
2842\maketitle
@@ -31,19 +45,19 @@
3145 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.
3246\end{abstract}
3347
34−\begin{otherlanguage}{russian}
48+% \begin{otherlanguage}{russian}
3549
36− \begin{abstract}
37− Настройка и сборка даже самых простых программных проектов часто бывает непростой задачей -- для этого требуется загрузить и установить большое количество необходимого программного обеспечения. Это часто делает проблематичным воспроизведение сборок проекта на разных компьютерах. Менеджер пакетов Nix стремится решить эту проблему, предоставляя единый язык для описания пакетов программного обеспечения чисто функциональным способом. Этот язык называется языком Nix Expression Language. Поскольку вся сложность конфигурации программного обеспечения должна быть выражена на языке Nix Expression Language, сами выражения часто становятся довольно сложными, что затрудняет понимание и расширение существующих выражений без ошибок. Широко распространенным инструментом для облегчения понимания и проверки корректности выражений на других языках является статическая проверка типов. В этой статье будут рассмотрены методы, которые можно использовать для добавления статической проверки типов в язык выражений Nix Expression Language.
38− \end{abstract}
50+% \begin{abstract}
51+% Настройка и сборка даже самых простых программных проектов часто бывает непростой задачей -- для этого требуется загрузить и установить большое количество необходимого программного обеспечения. Это часто делает проблематичным воспроизведение сборок проекта на разных компьютерах. Менеджер пакетов Nix стремится решить эту проблему, предоставляя единый язык для описания пакетов программного обеспечения чисто функциональным способом. Этот язык называется языком Nix Expression Language. Поскольку вся сложность конфигурации программного обеспечения должна быть выражена на языке Nix Expression Language, сами выражения часто становятся довольно сложными, что затрудняет понимание и расширение существующих выражений без ошибок. Широко распространенным инструментом для облегчения понимания и проверки корректности выражений на других языках является статическая проверка типов. В этой статье будут рассмотрены методы, которые можно использовать для добавления статической проверки типов в язык выражений Nix Expression Language.
52+% \end{abstract}
3953
40−\end{otherlanguage}
54+% \end{otherlanguage}
4155
4256\parr{Source code} \url{https://github.com/ilyakooo0/tix}
4357
44−\newpage
58+% \newpage
4559
46−\tableofcontents
60+% \tableofcontents
4761
4862\section*{Introduction}
4963
@@ -101,7 +115,8 @@ Atomic types are described in table~\ref{tab:atomicTypes}.
101115
102116\begin{table}[hbp]
103117 \centering
104− \begin{tabular}{ ||c||p{6cm}||p{6cm}|| } \hline
118+ \caption{Table of atomic Nix Expression Language types}
119+ \begin{tabular}{ ||c||p{2cm}||p{4cm}|| } \hline
105120 \textbf{Atomic type} & \textbf{Description} & \textbf{Example terms} \\ \hline
106121 URI & A string literal representing a URI. Does not require quoting. & \texttt{https://example.com} \\ \hline
107122 Path literal & A path literal referring to either a relative or absolute path. Does not require quoting. & \texttt{../../directory/file.txt} \\ \hline
@@ -110,7 +125,6 @@ Atomic types are described in table~\ref{tab:atomicTypes}.
110125 Bool & Boolean values. & \texttt{true} \newline \texttt{false} \\ \hline
111126 Null & A type with a single value. & \texttt{null} \\ \hline
112127 \end{tabular}
113− \caption{Table of atomic Nix Expression Language types}
114128 \label{tab:atomicTypes}
115129\end{table}
116130
@@ -120,7 +134,7 @@ Atomic types are described in table~\ref{tab:atomicTypes}.
120134
121135Double 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}.
122136
123−\begin{Listing}
137+\begin{figure}
124138 \begin{minipage}{\textwidth}
125139 \begin{verbatim}
126140"Sampel\nPalnet"
@@ -128,13 +142,13 @@ Double quoted string literals are string literals just like in many other progra
128142 \end{minipage}
129143 \caption{Nix Expression Language double quoted string literal example}
130144 \label{lst:newlineString}
131−\end{Listing}
145+\end{figure}
132146
133147\subsubsection{Multiline string literals}
134148
135149Multiline 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}.
136150
137−\begin{Listing}
151+\begin{figure}
138152 \begin{minipage}{\textwidth}
139153 \begin{verbatim}
140154''
@@ -146,43 +160,43 @@ Palnet''
146160 \end{minipage}
147161 \caption{Nix Expression Language multiline string literal example and an equivalent double quoted string literal}
148162 \label{lst:multilineString}
149−\end{Listing}
163+\end{figure}
150164
151−\subsubsection{String interpolation}
165+% \subsubsection{String interpolation}
152166
153−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}.
167+% 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}.
154168
155−\begin{Listing}
156− \begin{minipage}{\textwidth}
157− \begin{verbatim}
158−"one is ${ if 1 == 2 then "equal" else "not equal" } to two."
169+% \begin{figure}
170+% \begin{minipage}{\textwidth}
171+% \begin{verbatim}
172+% "one is ${ if 1 == 2 then "equal" else "not equal" } to two."
159173
160−"one is not equal to two."
161− \end{verbatim}
162− \end{minipage}
163− \caption{Nix Expression Language string interpolation example with the resulting string.}
164− \label{lst:stringInterpolation}
165−\end{Listing}
174+% "one is not equal to two."
175+% \end{verbatim}
176+% \end{minipage}
177+% \caption{Nix Expression Language string interpolation example with the resulting string.}
178+% \label{lst:stringInterpolation}
179+% \end{figure}
166180
167181\subsection{Lists}
168182
169183Nix 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}.
170184
171−\begin{Listing}
185+\begin{figure}
172186 \begin{minipage}{\textwidth}
173187 \begin{verbatim}
174−[1 2 "hello" ../../file.txt https://example.com]
188+[1 2 "hello" ../../file.txt]
175189 \end{verbatim}
176190 \end{minipage}
177191 \caption{Nix Expression Language List literals.}
178192 \label{lst:list}
179−\end{Listing}
193+\end{figure}
180194
181195\subsection{Attribute sets} \label{sec:attrSet}
182196
183197An 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}.
184198
185−\begin{Listing}
199+\begin{figure}
186200 \begin{minipage}{\textwidth}
187201 \begin{verbatim}
188202{ a = 42;
@@ -194,11 +208,11 @@ An attribute set is internally implemented as a hashmap with strings as keys whe
194208 \end{minipage}
195209 \caption{Nix Expression Language attribute set literals.}
196210 \label{lst:attrSet}
197−\end{Listing}
211+\end{figure}
198212
199213Fields (keys) of an attribute set can be accessed through the \emph{dot} (\texttt{.}) operator as shown in listing~\ref{lst:attrSetAccess}. Accessing an absent field yields a runtime error.
200214
201−\begin{Listing}
215+\begin{figure}
202216 \begin{minipage}{\textwidth}
203217 \begin{verbatim}
204218{ a = 42;
@@ -210,29 +224,30 @@ Fields (keys) of an attribute set can be accessed through the \emph{dot} (\textt
210224 \end{minipage}
211225 \caption{Nix Expression Language attribute set field accessing.}
212226 \label{lst:attrSetAccess}
213−\end{Listing}
227+\end{figure}
214228
215229\subsection{Attribute set updates} \label{sec:update}
216230
217231There is a binary \emph{update} operator that takes two \emph{attribute sets} as operands and ``merges'' them in a shallow manner, preferring values from the right operand. The operator is written as two forward slashes \texttt{//}. This has the effect of updating the left operand with values from the right operand. An example is shown in listing~\ref{lst:update}.
218232
219−\begin{Listing}
233+\begin{figure}
220234 \begin{minipage}{\textwidth}
221235 \begin{verbatim}
222−{x = {a = 1;}; y = 2;} // {x = "hello"; z = 1.5;}
236+{x = {a = 1;}; y = 2;}
237+ // {x = "hello"; z = 1.5;}
223238
224239{ x = "hello"; y = 2; z = 1.5; }
225240 \end{verbatim}
226241 \end{minipage}
227242 \caption{Nix Expression Language attribute set updates.}
228243 \label{lst:update}
229−\end{Listing}
244+\end{figure}
230245
231246\subsection{Recursive attribute sets} \label{sec:recAttrSet}
232247
233248While 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.
234249
235−\begin{Listing}
250+\begin{figure}
236251 \begin{minipage}{\textwidth}
237252 \begin{verbatim}
238253rec {
@@ -245,13 +260,13 @@ rec {
245260 \end{minipage}
246261 \caption{Nix Expression Language recursive attribute set literals.}
247262 \label{lst:recAttrSet}
248−\end{Listing}
263+\end{figure}
249264
250265\subsection{Let expressions} \label{sec:let}
251266
252267A \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}.
253268
254−\begin{Listing}
269+\begin{figure}
255270 \begin{minipage}{\textwidth}
256271 \begin{verbatim}
257272let
@@ -262,13 +277,13 @@ in d
262277 \end{minipage}
263278 \caption{Nix Expression Language \emph{let} expression literals.}
264279 \label{lst:let}
265−\end{Listing}
280+\end{figure}
266281
267282\subsection{With expression}
268283
269284\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}.
270285
271−\begin{Listing}
286+\begin{figure}
272287 \begin{minipage}{\textwidth}
273288 \begin{verbatim}
274289let
@@ -279,7 +294,7 @@ in d
279294 \end{minipage}
280295 \caption{Nix Expression Language \emph{with} expression literals.}
281296 \label{lst:with}
282−\end{Listing}
297+\end{figure}
283298
284299\section{Existing typecheckers}
285300
@@ -413,7 +428,7 @@ Of course, since \emph{attribute sets} are used as structures, their internal st
413428
414429This leads to a non-trivial typechecking case where modifying a structure leads to the resulting type depending on the type of the input structure as shown in listing~\ref{lst:update_ex}. The listing shows a lambda expression which receives an \emph{attribute set} as input, and updates the field \texttt{a} with the value of \texttt{1}. It quickly becomes problematic to derive a type for this expression if we decide to track fields at the type level: we can say that the lambda takes a value of type \texttt{\{\}} and returns a value of type \texttt{\{a = Integer;\}} (type of functions will later be written as \texttt{<input type> -> <output type>}). This might seem a natural type to derive, however it is obviously not correct. Calling it with a values of type \texttt{\{b = String;\}} and \texttt{\{b = Float; a = Bool;\}} would both be very much valid, and would both produce different resulting types: \texttt{\{a = Integer; b = String;\}} and \texttt{\{a = Integer; b = Float;\}}. As stated above, the output type of a lambda expression like this depends on the input type.
415430
416−\begin{Listing}
431+\begin{figure}
417432 \begin{minipage}{\textwidth}
418433 \begin{verbatim}
419434x: x // {a = 1;}
@@ -421,7 +436,7 @@ x: x // {a = 1;}
421436 \end{minipage}
422437 \caption{A lambda expression which updates an input set.}
423438 \label{lst:update_ex}
424−\end{Listing}
439+\end{figure}
425440
426441This problem is widely known as \emph{row polymorphism}~\cite{wand1991type} – the term \emph{row} refers to a single key-value type pair. Thus, \emph{row polymorphism} is the polymorphism of key-value pairs. This fields has already received some research attention: a recent paper on the topic was written by Morris and McKinna~\cite{morris2019abstracting}. In the paper the authors introduce the \emph{Rose}\footnote{The name is a pun on ``rows'' referring to row polymorphism.} programming language which supports \emph{row polymorphism}.
427442
@@ -563,9 +578,9 @@ Even though the developed type checker will need to check code for an existing d
563578
564579\newpage
565580
566−\bibliographystyle{gost2008}
581+\bibliographystyle{IEEEtran}
567582\bibliography{bibl}
568583
569−\registrationList
584+% \registrationList
570585
571586\end{document}