@@ -322,7 +322,7 @@ in d
322 \label{lst:with}
322 \label{lst:with}
323\end{figure}
323\end{figure}
325−\section{Existing typecheckers}
325+\section{Existing typecheckers implementations}
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.
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.
@@ -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.
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.
348−\section{Existing Approaches}
348+\section{Existing type system research}
350In this section we will explore existing techniques used to develop typecheckers, and explore how they can be applicable to our implementation.
350In this section we will explore existing techniques used to develop typecheckers, and explore how they can be applicable to our implementation.
@@ -393,7 +393,7 @@ There has been some research conducted in the field of type systems with row-pol
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.
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.
396−\section{Type system}
396+\section{Our Nix type system}
398As 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.
398As 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.
@@ -1010,6 +1010,10 @@ This way, when applying a predicate to check the lexical scope of a type variabl
1011\section{Evaluation of our implementation}
1011\section{Evaluation of our implementation}
1013+In this section we will examine how our implementation of the typechecker behaves on real input.
1015+\subsection{Evaluating nixpkgs}
1013To 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.
1017To 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.
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.
@@ -1018,6 +1022,111 @@ We believe this is a very good result since the files were not prepared in any w
1019We 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).
1023We 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).
1025+\subsection{Evaluating common expressions}
1027+We will now examine a few language constructs to see how our typechecker handles them, and what errors it can detect.
1029+\subsubsection{Script interpreters}
1031+In listing~\ref{lst:interpreters} we present a sample script which demonstrates our type inference algorithm.
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:
1036+ \forall \alpha \beta \gamma. \; (\alpha. \text{scripts} = [\beta], \beta. \text{interpreter} = \gamma) \Rightarrow \alpha \rightarrow [\gamma]
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.
1041+The result of the whole expression (applying \texttt{getScriptInterpreters} to \texttt{package}) is correctly inferred by our type checker to have the type:
1048+ \begin{minipage}{\textwidth}
1050+let getScriptInterpreters = x:
1056+ {interpreter = "bash";}
1057+ {interpreter = "zsh";}
1058+ {interpreter = "fish";}
1061+in getScriptInterpreters package
1064+ \caption{A sample nix program which gathers all interpreters used by a script in a package.}
1065+ \label{lst:interpreters}
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:
1071+getScriptInterpreters =
1072+ x: builtins.map (y: y.interpreter) x;
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.
1077+\subsubsection{Haskell packages}
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:
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; \}
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.
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:
1099+ [{\text{compiler} = \text{String}; \text{compilerFlags} = [\text{String}]; \text{src} = \text{String};}]
1103+ \begin{minipage}{\textwidth}
1105+let haskellPackage = x: {
1106+ compiler = "ghc" + (x.compilerVersion or "900");
1108+ compilerFlags = x.compilerFlags or ["-O3" "-j"];
1112+ src = ./project-m36;
1113+ compilerVersion = "865";
1117+ compilerFlags = ["-static"];
1122+ \caption{A sample nix program which defined several haskell packages..}
1123+ \label{lst:haskellPackages}
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.
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.
1021\section{Possible improvements}
1130\section{Possible improvements}
1023\subsection{Making predicates more user-friendly}
1132\subsection{Making predicates more user-friendly}
@@ -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}
1095−\section{Conclusion}
1204+\section*{Conclusion}
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.
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.