@@ -68,7 +68,7 @@
6868\pagestyle{plain}
6969
7070\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.
7272\end{abstract}
7373
7474% \begin{otherlanguage}{russian}
@@ -87,11 +87,11 @@
8787
8888\section*{Introduction}
8989
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.
9191
9292Such 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.
9393
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:
9595
9696\begin{enumerate}
9797 \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
109109 \end{enumerate}
110110\end{enumerate}
111111
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}.
113113
114114Secondly, 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.
115115
@@ -127,13 +127,13 @@ Refactoring existing code is also tricky since the generated expressions are onl
127127
128128A 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.
129129
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).
131131
132132The 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.
133133
134134\section{Nix Expression Language}
135135
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.
137137
138138\subsection{Atomic types}
139139
@@ -158,7 +158,7 @@ Atomic types are described in table~\ref{tab:atomicTypes}.
158158
159159\subsubsection{Double quoted string literals}
160160
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}.
162162
163163\begin{figure}
164164 \begin{minipage}{\textwidth}
@@ -172,7 +172,7 @@ Double quoted string literals are string literals just like in many other progra
172172
173173\subsubsection{Multiline string literals}
174174
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}.
176176
177177\begin{figure}
178178 \begin{minipage}{\textwidth}
@@ -206,7 +206,7 @@ Palnet''
206206
207207\subsection{Lists}
208208
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}.
210210
211211\begin{figure}
212212 \begin{minipage}{\textwidth}
@@ -236,7 +236,7 @@ An attribute set is internally implemented as a hashmap with strings as keys whe
236236 \label{lst:attrSet}
237237\end{figure}
238238
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.
240240
241241\begin{figure}
242242 \begin{minipage}{\textwidth}
@@ -271,7 +271,7 @@ There is a binary \emph{update} operator that takes two \emph{attribute sets} as
271271
272272\subsection{Recursive attribute sets} \label{sec:recAttrSet}
273273
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.
275275
276276\begin{figure}
277277 \begin{minipage}{\textwidth}
@@ -307,7 +307,7 @@ in d
307307
308308\subsection{With expression} \label{sec:withExp}
309309
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}.
311311
312312\begin{figure}
313313 \begin{minipage}{\textwidth}
@@ -883,7 +883,7 @@ instance Semigroup Substitution where
883883
884884This means that the order of composition does no longer matter, and applying the composition of substitutions yields more information than applying them sequentially.
885885
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:
887887
888888\begin{enumerate}
889889 \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
893893
894894\subsection{Typing context}
895895
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:
897897
898898\begin{enumerate}
899899 \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
902902
903903\subsubsection{Variables in scope}
904904
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.
906906
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}}:
908908
909909\begin{code}
910910data VariableMapEff x where
@@ -918,13 +918,13 @@ lookupVar
918918lookupVar = send . LookupVariable
919919\end{code}
920920
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.
922922
923923\subsubsection{Predicates}
924924
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.
926926
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''.
928928
929929\begin{code}
930930class (Ord (Key t), Ord t) => Keyable t where
@@ -938,8 +938,8 @@ data MultiKeyedMap t = MultiKeyedMap
938938The data structure is the product of two other data structures:
939939
940940\begin{enumerate}
941− \item A map, mapping possible keys of the stored |t| to a set of values the contain the given key
942− \item A set which contains the values that don't contain any keys
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 that contains the values that don't contain any keys
943943\end{enumerate}
944944
945945The |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
994994 \item are used in an outer lexical scope (environment)
995995\end{enumerate}
996996
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.
998998
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.
10001000
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:
10021002
10031003\begin{code}
10041004data TypeVariable
@@ -1006,29 +1006,29 @@ data TypeVariable
10061006 | SubTypeVariable Int Int
10071007\end{code}
10081008
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.
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.
1013+In this section, we will examine how our implementation of the typechecker behaves on real input.
10141014
10151015\subsection{Evaluating nixpkgs}
10161016
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.
10181018
10191019Running 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.
10201020
10211021We 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.
10221022
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).
10241024
10251025\subsection{Evaluating common expressions}
10261026
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.
10281028
10291029\subsubsection{Script interpreters}
10301030
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.
10321032
10331033The 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:
10341034
@@ -1036,7 +1036,7 @@ The function \texttt{getScriptInterpreters} takes a single ``package'' structure
10361036 \forall \alpha \beta \gamma. \; (\alpha. \text{scripts} = [\beta], \beta. \text{interpreter} = \gamma) \Rightarrow \alpha \rightarrow [\gamma]
10371037\end{equation}
10381038
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.
10401040
10411041The result of the whole expression (applying \texttt{getScriptInterpreters} to \texttt{package}) is correctly inferred by our type checker to have the type:
10421042
@@ -1065,18 +1065,18 @@ in getScriptInterpreters package
10651065 \label{lst:interpreters}
10661066\end{figure}
10671067
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:
10691069
10701070\begin{verbatim}
10711071getScriptInterpreters =
10721072 x: builtins.map (y: y.interpreter) x;
10731073\end{verbatim}
10741074
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.
10761076
10771077\subsubsection{Haskell packages}
10781078
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:
10801080
10811081\begin{equation}
10821082 \begin{aligned}
@@ -1091,7 +1091,7 @@ In listing~\ref{lst:haskellPackages} we defined a function \texttt{haskellPackag
10911091 \end{aligned}
10921092\end{equation}
10931093
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.
10951095
10961096The 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:
10971097
@@ -1123,9 +1123,9 @@ in [
11231123 \label{lst:haskellPackages}
11241124\end{figure}
11251125
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.
11271127
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.
11291129
11301130\section{Possible improvements}
11311131
@@ -1139,22 +1139,22 @@ The technique is based on the fact that a type variable by itself can only conve
11391139
11401140\begin{enumerate}
11411141 \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
11431143\end{enumerate}
11441144
11451145Note that all of what follows is only concerned with syntactic constructs. It does in no way alter the semantic of the predicates described above.
11461146
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}.
11481148
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.
11501150
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:
11521152
11531153\begin{equation}
11541154 \forall \alpha. \; \alpha \rightarrow \alpha.\text{y}
11551155\end{equation}
11561156
1157−When applied to the type~\ref{eq:updatePredExample} it yields:
1157+When applied to the type~\ref{eq:updatePredExample}, it yields:
11581158
11591159\begin{equation}
11601160 \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
11661166
11671167For 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.
11681168
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.
11701170
11711171\subsubsection{Limitations}
11721172
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}.
11741174
11751175Another 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.
11761176
@@ -1182,12 +1182,12 @@ Some information that might be useful as type hints:
11821182
11831183\begin{enumerate}
11841184 \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.
11861186\end{enumerate}
11871187
11881188\subsection{Sum types} \label{sec:sumTypes}
11891189
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.
11911191
11921192The 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:
11931193
@@ -1203,7 +1203,7 @@ where $\beta$ can be the type $\alpha$. With this predicate, our ``String or Num
12031203
12041204\section*{Conclusion}
12051205
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.
12071207
12081208\newpage
12091209