be81c19...master · tix

git.iko.soy/tix

docs/paper.lhs+47−47

since splitsnapshots

@@ -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}

@@ -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,29 +1006,29 @@ 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.

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

1014

1015\subsection{Evaluating nixpkgs}

1016

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

1018

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.

1020

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.

1022

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

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.

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

1032

1033The 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

@@ -1036,7 +1036,7 @@ The function \texttt{getScriptInterpreters} takes a single ``package'' structure

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.

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

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

1042

@@ -1065,18 +1065,18 @@ in getScriptInterpreters 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:

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}

1071getScriptInterpreters =

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.

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:

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}

@@ -1091,7 +1091,7 @@ In listing~\ref{lst:haskellPackages} we defined a function \texttt{haskellPackag

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.

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

1096The 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

@@ -1123,9 +1123,9 @@ in [

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.

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.

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

1130\section{Possible improvements}

1131

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

1139

1140\begin{enumerate}

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

1142− \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

1143\end{enumerate}

1144

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.

1146

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

1148

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.

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.

1150

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:

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:

1152

1153\begin{equation}

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

1155\end{equation}

1156

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

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

1158

1159\begin{equation}

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

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

1166

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.

1168

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

1170

1171\subsubsection{Limitations}

1172

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

1174

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.

1176

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

1182

1183\begin{enumerate}

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

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.

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.

1186\end{enumerate}

1187

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

1189

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.

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.

1191

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:

1193

@@ -1203,7 +1203,7 @@ where $\beta$ can be the type $\alpha$. With this predicate, our ``String or Num

1203

1204\section*{Conclusion}

1205

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 code base. We have also outlined further practical improvements to our implementation which could improve the developer experience.

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.

1207

1208\newpage

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.