@@ -322,7 +322,7 @@ in d
322322 \label{lst:with}
323323\end{figure}
324324
325−\section{Existing typecheckers}
325+\section{Existing typecheckers implementations}
326326
327327In 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.
328328
@@ -345,7 +345,7 @@ haskell-nix/hnix\footnote{\url{https://github.com/haskell-nix/hnix}} is primaril
345345\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.
346346
347347
348−\section{Existing Approaches}
348+\section{Existing type system research}
349349
350350In this section we will explore existing techniques used to develop typecheckers, and explore how they can be applicable to our implementation.
351351
@@ -393,7 +393,7 @@ There has been some research conducted in the field of type systems with row-pol
393393
394394% 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.
395395
396−\section{Type system}
396+\section{Our Nix type system}
397397
398398As 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.
399399
@@ -1010,6 +1010,10 @@ This way, when applying a predicate to check the lexical scope of a type variabl
10101010
10111011\section{Evaluation of our implementation}
10121012
1013+In this section we will examine how our implementation of the typechecker behaves on real input.
1014+
1015+\subsection{Evaluating nixpkgs}
1016+
10131017To 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.
10141018
10151019Running 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.
@@ -1018,6 +1022,111 @@ We believe this is a very good result since the files were not prepared in any w
10181022
10191023We 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).
10201024
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 which 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 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} which takes parameters for a haskell package and returns a configuration which 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 out 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.
1129+
10211130\section{Possible improvements}
10221131
10231132\subsection{Making predicates more user-friendly}
@@ -1092,11 +1201,9 @@ where $\beta$ can be the type $\alpha$. With this predicate, our ``String or Num
10921201 \strOrNum \sim \alpha = (\text{String} \lessdot \alpha, \text{Number} \lessdot \alpha)
10931202\end{equation}
10941203
1095−\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.
1204+\section*{Conclusion}
10981205
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 you type system which we tested on an existing code base. We have also outlined further practical improvements to our implementation which could improve the developer experience.
11001207
11011208\newpage
11021209