72fbe14..master · tix · git.iko.soy

git.iko.soy/tix

docs/paper.lhs+152−45

@@ -68,7 +68,7 @@

68\pagestyle{plain}

70\begin{abstract}

71− 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.

71+ 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 pretty 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.

72\end{abstract}

74% \begin{otherlanguage}{russian}

@@ -87,11 +87,11 @@

88\section*{Introduction}

90−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.

90+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 manually install additional libraries and tools.

92Such 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.

94−This problem is partially solved by so-called virtual environment 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. These tools can generally be split into one of two categories:

94+So-called virtual environment tools partially solve this problem. A virtual environment is a way of restricting and customizing the available external tools (usually compilers) with the ability to switch between them dynamically. These tools can generally be split into one of two categories:

96\begin{enumerate}

97 \item \emph{language-specific tools} which simplify installing and switching between different versions of some tools (usually compilers). Examples of such tools are:

@@ -109,7 +109,7 @@ This problem is partially solved by so-called virtual environment tools. A virtu

109 \end{enumerate}

110\end{enumerate}

111

112−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}.

112+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}.

113

114Secondly, 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.

115

@@ -127,13 +127,13 @@ Refactoring existing code is also tricky since the generated expressions are onl

127

128A widespread tool for easing development and alleviate the aforementioned problems in other languages is static type checking -- the process of analyzing the types of expressions and detecting type errors in programs without evaluating them.

129

130−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).

130+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).

131

132The 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.

133

134\section{Nix Expression Language}

135

136−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.

136+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.

137

138\subsection{Atomic types}

139

@@ -158,7 +158,7 @@ Atomic types are described in table~\ref{tab:atomicTypes}.

158

159\subsubsection{Double quoted string literals}

160

161−Double quoted string literals are string literals just like in many other programming languages. It can contain esaped newline character literals \texttt{\textbackslash n} which will be preserved as shown in figure~\ref{lst:newlineString}.

161+Double quoted string literals are string literals, just like in many other programming languages. It can contain escaped newline character literals \texttt{\textbackslash n} which will be preserved as shown in figure~\ref{lst:newlineString}.

162

163\begin{figure}

164 \begin{minipage}{\textwidth}

@@ -172,7 +172,7 @@ Double quoted string literals are string literals just like in many other progra

172

173\subsubsection{Multiline string literals}

174

175−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 figure~\ref{lst:multilineString}.

175+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 figure~\ref{lst:multilineString}.

176

177\begin{figure}

178 \begin{minipage}{\textwidth}

@@ -206,7 +206,7 @@ Palnet''

206

207\subsection{Lists}

208

209−Nix supports 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 figure~\ref{lst:list}.

209+Nix supports 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 figure~\ref{lst:list}.

210

211\begin{figure}

212 \begin{minipage}{\textwidth}

@@ -236,7 +236,7 @@ An attribute set is internally implemented as a hashmap with strings as keys whe

236 \label{lst:attrSet}

237\end{figure}

238

239−Fields (keys) of an attribute set can be accessed through the \emph{dot} (\texttt{.}) operator as shown in figure~\ref{lst:attrSetAccess}. Accessing an absent field yields a runtime error.

239+Fields (keys) of an attribute set can be accessed through the \emph{dot} (\texttt{.}) operator, as shown in figure~\ref{lst:attrSetAccess}. Accessing an absent field yields a runtime error.

240

241\begin{figure}

242 \begin{minipage}{\textwidth}

@@ -271,7 +271,7 @@ There is a binary \emph{update} operator that takes two \emph{attribute sets} as

271

272\subsection{Recursive attribute sets} \label{sec:recAttrSet}

273

274−While ordinary \emph{attribute sets} 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 available in the scopes of the attribute set values. An example \emph{recursive attribute set} is given in figure~\ref{lst:recAttrSet}. Note that it is syntactically distinguished form normal \emph{attribute set} literals by the \texttt{rec} key word at the beginning.

274+While ordinary \emph{attribute sets} 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 available in the scopes of the attribute set values. An example \emph{recursive attribute set} is given in figure~\ref{lst:recAttrSet}. Note that it is syntactically distinguished from normal \emph{attribute set} literals by the \texttt{rec} keyword at the beginning.

275

276\begin{figure}

277 \begin{minipage}{\textwidth}

@@ -307,7 +307,7 @@ in d

307

308\subsection{With expression} \label{sec:withExp}

309

310−\emph{With expressions} are a way of bringing 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 figure~\ref{lst:with}.

310+\emph{With expressions} are a way of bringing 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 described 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 figure~\ref{lst:with}.

311

312\begin{figure}

313 \begin{minipage}{\textwidth}

@@ -322,7 +322,7 @@ in d

322 \label{lst:with}

323\end{figure}

324

325−\section{Existing typecheckers}

325+\section{Existing typecheckers implementations}

326

327In 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 the implementations are.

328

@@ -345,7 +345,7 @@ haskell-nix/hnix\footnote{\url{https://github.com/haskell-nix/hnix}} is primaril

345\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.

346

347

348−\section{Existing Approaches}

348+\section{Existing type system research}

349

350In this section we will explore existing techniques used to develop typecheckers, and explore how they can be applicable to our implementation.

351

@@ -393,9 +393,9 @@ There has been some research conducted in the field of type systems with row-pol

393

394% 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.

395

396−\section{Type system}

396+\section{Our Nix type system}

397

398−As mentioned above, we have opted to use the Damas-Milner type system as a basis for our implementation. Our goal is not to just add types for the sake of types, but give additional reassurance to the developer, and reject as many potentially ``invalid'' programs as possible. If the developed typechecker processes a program without errors, then the program should have no type errors during execution.

398+As mentioned above, we have opted to use the Damas-Milner type system as a basis for our implementation. Our goal is not just to add types for the sake of types, but give additional reassurance to the developer, and reject as many potentially ``invalid'' programs as possible. If the developed typechecker processes a program without errors, then the program should have no type errors during execution.

399

400\subsection{Polymorphism} \label{sec:polymorphism}

401

@@ -568,7 +568,7 @@ The term \texttt{x: y: x // y} would yield the following type:

568 \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma

569\end{equation}

570

571−\subsection{Atmoic types}

571+\subsection{Atomic types}

572

573Nix is a dynamic language, and as such, allows dynamic coercions between certain types. This means that we can not use the dynamic types from the interpreter to perform static type checking -- if we did that we would reject \emph{a lot} of valid programs.\footnote{``Valid'' not just in the sense that they would not produce runtime errors, but ``valid'' in the sense that the programmer would judge the program as being ``correct''.}

574

@@ -883,7 +883,7 @@ instance Semigroup Substitution where

883

884This means that the order of composition does no longer matter, and applying the composition of substitutions yields more information than applying them sequentially.

885

886−Another consequence of the decision to delay substitutions is that now the role of the |infer| step of typechecking only does the following tree things:

886+Another consequence of the decision to delay substitutions is that now the role of the |infer| step of typechecking only does the following three things:

887

888\begin{enumerate}

889 \item returns a type variable that represents the type of the expression being inferred

@@ -893,7 +893,7 @@ Another consequence of the decision to delay substitutions is that now the role

893

894\subsection{Typing context}

895

896−The typing context in our implementation in essence consists of two distinct data structures:

896+The typing context in our implementation, in essence, consists of two distinct data structures:

897

898\begin{enumerate}

899 \item the types of variables currently in scope

@@ -902,9 +902,9 @@ The typing context in our implementation in essence consists of two distinct dat

902

903\subsubsection{Variables in scope}

904

905−Note that in practice the ``variables in scope'' data structure only needs to contain type variables since we apply substitutions as late as possible.

905+Note that in practice, the ``variables in scope'' data structure only needs to contain type variables since we apply substitutions as late as possible.

906

907−In actual fact, due to the heuristics described in section~\ref{sec:withExprType} the types of variables in scope can not be represented as static data structure, but rather is implemented as a scoped effect\footnote{Effects in our case are implemented using the \emph{freer-simple} library: \url{https://github.com/lexi-lambda/freer-simple}}:

907+In actual fact, due to the heuristics described in section~\ref{sec:withExprType}, the types of variables in scope can not be represented as a static data structure but rather is implemented as a scoped effect\footnote{Effects in our case are implemented using the \emph{freer-simple} library: \url{https://github.com/lexi-lambda/freer-simple}}:

908

909\begin{code}

910data VariableMapEff x where

@@ -918,13 +918,13 @@ lookupVar

918lookupVar = send . LookupVariable

919\end{code}

920

921−This allows us to dynamically redefine what it means to lookup a variable in terms of its implementation in the outer context.

921+This allows us to dynamically redefine what it means to look up a variable in terms of its implementation in the outer context.

922

923\subsubsection{Predicates}

924

925−Predicates can, on the other hand, be stored as a static data structure. The only non-standard behavior is that the set of predicates needs to be queried and manipulated based on the types that they contain, rather than on the predicates themselves.

925+Predicates can, on the other hand, be stored as a static data structure. The only non-standard behavior is that the set of predicates needs to be queried and manipulated based on the types that they contain rather than on the predicates themselves.

926

927−For this reason we have developed a data structure we call ``multi-keyed map''.

927+For this reason, we have developed a data structure we call ``multi-keyed map''.

928

929\begin{code}

930class (Ord (Key t), Ord t) => Keyable t where

@@ -938,8 +938,8 @@ data MultiKeyedMap t = MultiKeyedMap

938The data structure is the product of two other data structures:

939

940\begin{enumerate}

941− \item A map, mapping possible keys of the stored |t| to a set of values the contain the given key

941+ \item A map, mapping possible keys of the stored |t| to a set of values that contain the given key

942− \item A set which contains the values that don't contain any keys

942+ \item A set that contains the values that don't contain any keys

943\end{enumerate}

944

945The |Keyable| typeclass is used to extract the keys from the values that need to be stored.

@@ -994,11 +994,11 @@ An observation we can make is the following: it only makes sense to close over t

994 \item are used in an outer lexical scope (environment)

995\end{enumerate}

996

997−This greatly simplifies implementing the typing rule~\ref{eq:letGeneralization} since instead of having to calculate a set of free type variables of the whole context, we only need to obtain a predicate which identifies if a type variable was introduced during the inference of an expression. This is made even easier if type variables are internally represented as integers, as they often are.

997+This greatly simplifies implementing the typing rule~\ref{eq:letGeneralization} since instead of having to calculate a set of free type variables of the whole context, we only need to obtain a predicate that identifies if a type variable was introduced during the inference of an expression. This is made even easier if type variables are internally represented as integers, as they often are.

998

999−In our case this is complicated by the fact that we need to introduce type variables which are fields of an \emph{attribute set} from an outer lexical scope. This is problematic because while the type variable can be defined during inference, it is actually logically defined at the same position as the initial \emph{attribute set}; it has the same lexical scope as the \emph{attribute set}. So, the lexical scope of a type variable can not be derived from the inference context of an expression.

999+In our case, this is complicated by the fact that we need to introduce type variables which are fields of an \emph{attribute set} from an outer lexical scope. This is problematic because while the type variable can be defined during inference, it is actually logically defined at the same position as the initial \emph{attribute set}; it has the same lexical scope as the \emph{attribute set}. So, the lexical scope of a type variable can not be derived from the inference context of an expression.

1000

1001−A solution we came up with is to have two ways a type variable can be constructed -- as an ordinary type variable backed by a single integer, or as a sub-type variable which has the same lexical scope as another type variable:

1001+A solution we came up with is to have two ways a type variable can be constructed -- as an ordinary type variable backed by a single integer or as a sub-type variable that has the same lexical scope as another type variable:

1002

1003\begin{code}

1004data TypeVariable

@@ -1006,17 +1006,126 @@ data TypeVariable

1006 | SubTypeVariable Int Int

1007\end{code}

1008

1009−This way, when applying a predicate to check the lexical scope of a type variable we can always restrict ourselves to the first integer.

1009+This way, when applying a predicate to check the lexical scope of a type variable, we can always restrict ourselves to the first integer.

1010

1011\section{Evaluation of our implementation}

1012

1013+In this section, we will examine how our implementation of the typechecker behaves on real input.

1014+

1015+\subsection{Evaluating nixpkgs}

1016+

1013−To evaluate our typechecker implementation~\cite{github-source} we collected \emph{Nix} source files from the larges \emph{Nix} package repository – \emph{nixpkgs}\footnote{\url{https://github.com/NixOS/nixpkgs}}. Due to our current implementation not supporting file imports (file imports are the responsibility of the system calling the typechecker, not the type checker itself) the files were filtered down to those that do not contain import statements.

1017+To evaluate our typechecker implementation~\cite{github-source}, we collected \emph{Nix} source files from the largest \emph{Nix} package repository – \emph{nixpkgs}\footnote{\url{https://github.com/NixOS/nixpkgs}}. Due to our current implementation not supporting file imports (file imports are the responsibility of the system calling the typechecker, not the type checker itself), the files were filtered down to those that do not contain import statements.

1014

1018

1015Running our typechecker on the test set of \emph{Nix} source files results in \emph{1963} out of \emph{2948} (67\%) typechecking with no type errors.

1019Running our typechecker on the test set of \emph{Nix} source files results in \emph{1963} out of \emph{2948} (67\%) typechecking with no type errors.

1016

1020

1017We believe this is a very good result since the files were not prepared in any way and were taken as-is from the package repository. Furthermore, it is important to note that rejecting a portion of ``valid'' programs is an unavoidable property of static typecheckers.

1021We believe this is a very good result since the files were not prepared in any way and were taken as-is from the package repository. Furthermore, it is important to note that rejecting a portion of ``valid'' programs is an unavoidable property of static typecheckers.

1018

1022

1019−We would also like to point out that even in those cases, when type errors were encountered during typechecking, the typechecker still produces output types which can be useful to the developer and can be used for further typechecking of larger expressions (though, providing less guarantees).

1023+We would also like to point out that even in those cases when type errors were encountered during typechecking, the typechecker still produces output types that can be useful to the developer and can be used for further typechecking of larger expressions (though providing fewer guarantees).

1024+

1025+\subsection{Evaluating common expressions}

1026+

1027+We will now examine a few language constructs to see how our typechecker handles them and what errors it can detect.

1028+

1029+\subsubsection{Script interpreters}

1030+

1031+In listing~\ref{lst:interpreters} we present a sample script that demonstrates our type inference algorithm.

1032+

1033+The function \texttt{getScriptInterpreters} takes a single ``package'' structure and returns a list of interpreters used in the scripts of the package. Out type inference algorithm correctly infers the following type of the function:

1034+

1035+\begin{equation}

1036+ \forall \alpha \beta \gamma. \; (\alpha. \text{scripts} = [\beta], \beta. \text{interpreter} = \gamma) \Rightarrow \alpha \rightarrow [\gamma]

1037+\end{equation}

1038+

1039+The constant \texttt{package} contains a sample ``package'' structure with three scripts. In real code, the structure would be a lot more complex, but it is simplified for brevity.

1040+

1041+The result of the whole expression (applying \texttt{getScriptInterpreters} to \texttt{package}) is correctly inferred by our type checker to have the type:

1042+

1043+\begin{equation}

1044+ [\text{String}]

1045+\end{equation}

1046+

1047+\begin{figure}

1048+ \begin{minipage}{\textwidth}

1049+ \begin{verbatim}

1050+let getScriptInterpreters = x:

1051+ builtins.map

1052+ (y: y.interpreter)

1053+ x.scripts;

1054+ package = {

1055+ scripts = [

1056+ {interpreter = "bash";}

1057+ {interpreter = "zsh";}

1058+ {interpreter = "fish";}

1059+ ];

1060+ };

1061+in getScriptInterpreters package

1062+\end{verbatim}

1063+ \end{minipage}

1064+ \caption{A sample nix program which gathers all interpreters used by a script in a package.}

1065+ \label{lst:interpreters}

1066+\end{figure}

1067+

1068+If a programmer makes a certain class of mistakes when developing the program, our typechecker would report an error. For example, the programmer might forget to access the ``scripts'' field of the package and pass the whole package by accident:

1069+

1070+\begin{verbatim}

1071+getScriptInterpreters =

1072+ x: builtins.map (y: y.interpreter) x;

1073+\end{verbatim}

1074+

1075+In that case, when evaluating the whole expression from listing~\ref{lst:interpreters}, he would receive the following error from the typechecker: ``could not match list with type \texttt{\{scripts = [{interpreter = String;}]\}}''. This error is a result of trying to \texttt{map} over an attribute set.

1076+

1077+\subsubsection{Haskell packages}

1078+

1079+In listing~\ref{lst:haskellPackages}, we defined a function \texttt{haskellPackage} that takes parameters for a Haskell package and returns a configuration that might describe how to build the package. Out tool correctly infers the type of the function:

1080+

1081+\begin{equation}

1082+ \begin{aligned}

1083+ \forall \alpha \beta. \; &

1084+ \\ ( & \alpha \optDot \text{compilerFlags} = [\text{String}],

1085+ \\ & \alpha \optDot \text{compilerVersion} = \text{String},

1086+ \\ & \alpha.\text{src} = \beta)

1087+ \\ \Rightarrow & \alpha

1088+ \\ \rightarrow & \{ \text{compiler} = \text{String};

1089+ \\ & \text{compilerFlags} = [\text{String}];

1090+ \\ & \text{src} = \beta; \}

1091+ \end{aligned}

1092+\end{equation}

1093+

1094+By the derived type of the function, we can clearly see that the \texttt{compilerFlags} and \texttt{compilerVersion} fields of the input attribute set are optional.

1095+

1096+The result of the whole expression is a list of applications of the \texttt{haskellPackage} function to multiple configurations. Ou implementation correctly infers the following type:

1097+

1098+\begin{equation}

1099+ [{\text{compiler} = \text{String}; \text{compilerFlags} = [\text{String}]; \text{src} = \text{String};}]

1100+\end{equation}

1101+

1102+\begin{figure}

1103+ \begin{minipage}{\textwidth}

1104+ \begin{verbatim}

1105+let haskellPackage = x: {

1106+ compiler = "ghc" + (x.compilerVersion or "900");

1107+ inherit (x) src;

1108+ compilerFlags = x.compilerFlags or ["-O3" "-j"];

1109+};

1110+in [

1111+ (haskellPackage {

1112+ src = ./project-m36;

1113+ compilerVersion = "865";

1114+ })

1115+ (haskellPackage {

1116+ src = ./pandoc;

1117+ compilerFlags = ["-static"];

1118+ })

1119+]

1120+ \end{verbatim}

1121+ \end{minipage}

1122+ \caption{A sample nix program which defined several haskell packages..}

1123+ \label{lst:haskellPackages}

1124+\end{figure}

1125+

1126+A mistake that is easy to make here is to forget to quote the \texttt{compilerVersion} field, leading to the type being `Number' instead of `String'. In that case, our implementation will convey exactly that in an error.

1127+

1128+Another common mistake is specifying the \texttt{compilerFlags} field as a single `String' instead of a list. In that case, our implementation will emit an appropriate error without the need to execute the expression.

1020

1129

1021\section{Possible improvements}

1130\section{Possible improvements}

1022

1131

@@ -1030,22 +1139,22 @@ The technique is based on the fact that a type variable by itself can only conve

1030

1139

1031\begin{enumerate}

1140\begin{enumerate}

1032 \item positional information -- a specific position in a type

1141 \item positional information -- a specific position in a type

1033− \item identity information -- the type variable is equivalent to other type variable with the same name within the scope where it is declared

1142+ \item identity information -- the type variable is equivalent to other type variables with the same name within the scope where it is declared

1034\end{enumerate}

1143\end{enumerate}

1035

1144

1036Note that all of what follows is only concerned with syntactic constructs. It does in no way alter the semantic of the predicates described above.

1145Note that all of what follows is only concerned with syntactic constructs. It does in no way alter the semantic of the predicates described above.

1037

1146

1038−We 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}.

1147+We would like to point out that all of the predicates have an operand which is the ``result'' of the predicate -- a single type variable that 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}.

1039

1148

1040−The observation we need to make is that \emph{referential transparency}\footnote{\url{https://en.wikipedia.org/wiki/Referential_transparency}} is a 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.

1149+The observation we need to make is that \emph{referential transparency}\footnote{\url{https://en.wikipedia.org/wiki/Referential_transparency}} is a 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.

1041

1150

1042−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:

1151+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:

1043

1152

1044\begin{equation}

1153\begin{equation}

1045 \forall \alpha. \; \alpha \rightarrow \alpha.\text{y}

1154 \forall \alpha. \; \alpha \rightarrow \alpha.\text{y}

1046\end{equation}

1155\end{equation}

1047

1156

1048−When applied to the type~\ref{eq:updatePredExample} it yields:

1157+When applied to the type~\ref{eq:updatePredExample}, it yields:

1049

1158

1050\begin{equation}

1159\begin{equation}

1051 \forall \alpha \beta. \; \alpha \rightarrow \beta \rightarrow (\alpha \update \beta)

1160 \forall \alpha \beta. \; \alpha \rightarrow \beta \rightarrow (\alpha \update \beta)

@@ -1057,11 +1166,11 @@ We believe the derived types above are a lot easier to understand than their ini

1057

1166

1058For 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.

1167For 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.

1059

1168

1060−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.

1169+The 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.

1061

1170

1062\subsubsection{Limitations}

1171\subsubsection{Limitations}

1063

1172

1064−The technique is not in applicable if the ``result'' of a predicate is not a type variable like in type \ref{eq:optFieldPredExample2}.

1173+The technique is not applicable if the ``result'' of a predicate is not a type variable like in type \ref{eq:optFieldPredExample2}.

1065

1174

1066Another 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.

1175Another 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.

1067

1176

@@ -1073,12 +1182,12 @@ Some information that might be useful as type hints:

1073

1182

1074\begin{enumerate}

1183\begin{enumerate}

1075 \item The dynamic type of strings (URI, Path, etc.) – useful information for the programmer

1184 \item The dynamic type of strings (URI, Path, etc.) – useful information for the programmer

1076− \item Programmer-supplied annotations. When writing nix expressions it is common practice to have a program in some other programming language embedded in Nix as a string literal. It would be useful to propagate information about the underlying programming language to aid IDEs -- they could enable special syntax highlighting and linting based on the programming language.

1185+ \item Programmer-supplied annotations. When writing nix expressions, it is common practice to have a program in some other programming language embedded in Nix as a string literal. It would be useful to propagate information about the underlying programming language to aid IDEs -- they could enable special syntax highlighting and linting based on the programming language.

1077\end{enumerate}

1186\end{enumerate}

1078

1187

1079\subsection{Sum types} \label{sec:sumTypes}

1188\subsection{Sum types} \label{sec:sumTypes}

1080

1189

1081−In our static type system we introduced a ``special case'' for the \emph{addition operator} as it could be applied to a number of different types.

1190+In our static type system, we introduced a ``special case'' for the \emph{addition operator} as it could be applied to a number of different types.

1082

1191

1083The idea of this improvement is to generalize the case and allow the type system to handle arbitrary sums of arbitrary types. This can be implemented as a predicate stating that a type variable can be a certain type:

1192The idea of this improvement is to generalize the case and allow the type system to handle arbitrary sums of arbitrary types. This can be implemented as a predicate stating that a type variable can be a certain type:

1084

1193

@@ -1092,11 +1201,9 @@ where $\beta$ can be the type $\alpha$. With this predicate, our ``String or Num

1092 \strOrNum \sim \alpha = (\text{String} \lessdot \alpha, \text{Number} \lessdot \alpha)

1201 \strOrNum \sim \alpha = (\text{String} \lessdot \alpha, \text{Number} \lessdot \alpha)

1093\end{equation}

1202\end{equation}

1094

1203

1095−\section{Conclusion}

1204+\section*{Conclusion}

1096−

1097−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.

1098

1205

1099−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.

1206+In this paper, we have examined the existing approaches which have been used in developing type systems for functional programming languages. We have then adapted the existing approaches and developed a new static type system for the Nix Expression Language. We have also developed a preliminary implementation of our type system, which we tested on an existing codebase. We have also outlined further practical improvements to our implementation, which could improve the developer experience.

1100

1207

1101\newpage

1208\newpage

1102

1209

docs/pres_2/img/ter.png

Binary file not shown.

docs/pres_2/pres.md+52−52

@@ -20,8 +20,9 @@ _Supervisor:_ Victor Kuliamin, Associate Professor, PhD

21---

23−> Nix is a powerful package manager that makes package management reliable and reproducible.

23+## Nix is a powerful package manager that makes package management reliable and reproducible.

24+

24−-- [nixos.org](https://nixos.org)

25+#### – [nixos.org](https://nixos.org)

26---

27---

@@ -65,10 +66,12 @@ in derivation {

66---

67---

68−[.text: text-scale(0.75)]

69+[.text: text-scale(0.55)]

70# Terms and definitions

71# Terms and definitions

73+**Type** – an attribute of data which tells the compiler or interpreter how the programmer intends to use the data

74+

72**Type system** – a logical system comprising a set of rules that assigns a property called a type to the various constructs of a computer program

75**Type system** – a logical system comprising a set of rules that assigns a property called a type to the various constructs of a computer program

74**Type checking** – the process of verifying and enforcing the constraints of types.

77**Type checking** – the process of verifying and enforcing the constraints of types.

@@ -102,14 +105,14 @@ Adding static typing would:

102- Increase reliability of code

105- Increase reliability of code

103- Lower costs of development (resolving issue earlier is cheaper)

106- Lower costs of development (resolving issue earlier is cheaper)

104

107

105−_The typechecker should help find issues in existing code_

108+

106

109

107---

110---

108

111

109# The goal

112# The goal

110

113

111−1. Develop a type static system for the existing Nix expression language

114+1. Develop a static type system for the existing Nix expression language

112−2. Develop a type checker for this type system

115+2. Develop a type checker for this static type system

113

116

114---

117---

115

118

@@ -129,31 +132,48 @@ The Hindley–Milner type system_[1]_ is a simple, but well-studied type system

129

132

130---

133---

131

134

132−# Functional requirements

135+# Methods and algorithms

133

136

134−- The system should perform type checking on expression.

137+The developed type system is heavily influenced by the Hindley–Milner_[1]_ type system.

135

138

136−- The system should analyze the types and presence of attributes in attribute sets.

137

139

138−- The system should report encountered typechecking.

140+---

139

141

140−- The system should report the use of undefined terms.

142+# Methods and algorithms

141

143

142−- The system should report the resulting types of expressions to the user.

144+The developed type system supports parametric polymorphism to support code that does not require a specific type.

143

145

144−---

146+```nix

147+x: y: x ++ y

148+```

145

149

146−[.text: text-scale(0.85)]

150+```

151+∀ α. [α] -> [α] -> [α]

152+```

153+

154+---

147

155

148# Methods and algorithms

156# Methods and algorithms

149

157

150−The type system will be heavily influenced by the Hindley–Milner_[1]_ type system.

158+The developed type system implements row polymorphism to work with attribute sets.

159+

160+```nix

161+x: x.v + 69

162+```

163+

164+```

165+∀ α. (α.v = Number) => α -> Number

166+```

151

167

152−The type system will implement parametric polymorphism to support code that does not require a specific type.

168+<br />

153

169

154−The type system will implement arbitrary-ranked polymorphism_[3]_ with deep instantiation to disambiguate types in existing untyped code.

170+```nix

171+x: x // {v = "hello";}

172+```

155

173

156−The type system will implement row polymorphism to work with attribute sets.

174+```

175+∀ α β. (α // {v = String;} ~ β) => α -> β

176+```

157

177

158---

178---

159

179

@@ -177,49 +197,28 @@ The typechecker is implemented in a two-step architecture:

177

197

178---

198---

179

199

180−# Current results

200+# Results

181

201

182−A typechecker executable that successfully typechecks _most_ of the selected files from _nixpkgs_.

202+- Theoretical

203+ - A static type system for the Nix Expression Language

183

204

184−The typechecker currently has some support for all language constructs.

205+- Practical

185

206

186−![.right .fit](img/ter.png)

207+ - A typechecker executable that successfully typechecks _most_ of the selected files from _nixpkgs_.

187−

188−---

189

208

190−[.build-lists: false]

209+ - The typechecker supports all language constructs.

191

210

192−# Current results

193−

194−## Paper status

195−

196−1. Nix Expression Language (80%)

197−2. Existing typecheckers (100%)

198−3. Existing approaches (100%)

199−4. Architecture (20%)

200−5. Implementation (0%)

201−6. Conclusion (60%)

202−

203−![.right .fit](img/paper.png)

211+![.right .fit](img/ter.png)

204−

205−---

206−

207−# What is left

208−

209−- Better type rendering (predicates)

210−- Subsumption

211−- A lot of minor big fixes in type inference

212−- Add type information about built-in functions

213

212

214---

213---

215

214

216# Potential future developments

215# Potential future developments

217

216

218- Add support for user-supplied type annotations.

217- Add support for user-supplied type annotations.

219− - Fork parser

220− - Bidirectional type inference_[4]_

221- Type holes

218- Type holes

222- Language Server Integration

219- Language Server Integration

220+- Better type rendering

221+- Sum types

223

222

224---

223---

225

224

@@ -228,9 +227,10 @@ The typechecker currently has some support for all language constructs.

228

227

229# References

228# References

230

229

231−1. Damas L., Milner R. Principal type-schemes for functional programs //Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. – 1982. – С. 207-212.

230+1. L. Damas and R. Milner, “Principal type-schemes for functional pro- grams,” in Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1982, pp. 207–212.

232−2. Jones S. P. et al. Practical type inference for arbitrary-rank types //Journal of functional programming. – 2007. – Т. 17. – №. 1. – С. 1-82. MLA

231+2. E. Dolstra and A. Loh, “Nixos: A purely functional linux distribution,” in Proceedings of the 13th ACM SIGPLAN international conference on Functional programming, 2008, pp. 367–378.

233−3. Stuckey P. J., Sulzmann M., Wazny J. Improved inference for checking type annotations //arXiv preprint cs/0507036. – 2005. MLA

232+3. J. G. Morris and J. McKinna, “Abstracting extensible data types: or, rows by any other name,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 1–28, 2019.

233+4. D. Leijen, “Extensible records with scoped labels.” Trends in Functional Programming, vol. 6, pp. 179–194, 2005.

234

235---

236

@@ -347,7 +347,7 @@ let f = x: x.a; in f {b = "hello";}

347```

348

349```

350−Error: key "a" NotPresent in { b = String; }

350+Error: key "a" not present in { b = String; }

351```

352

353---

paper.pdfnew file

Binary file not shown.