@@ -91,7 +91,7 @@ Today developing software is riddled with large amounts of complexity -- newer s
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 environments 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. The tools can generally be split into one of two categories:
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:
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:
@@ -121,11 +121,11 @@ Using a fully-fledged programming language allows the users to reuse common defi
121121
122122Nix Expression Language is a dynamic, lazy, purely functional programming language. The purely functional nature of the language aids in build reproducibility guarantees that Nix aims to provide.
123123
124−Even considering the tremendous benefits that using a programming language for build configuration brings, the dynamic nature of the language often still makes it challenging to understand and reuse existing code. This is in part due to the large amounts of code required to describe real-world systems in all of their complexity fully.\footnote{The standard Nix package repository |nixpkgs| contains 2 million lines of code.}
124+Even considering the tremendous benefits that using a programming language for build configuration brings, the dynamic nature of the language often still makes it challenging to understand and reuse existing code. This is in part due to the large amounts of code required to describe real-world systems in all of their complexity.\footnote{The standard Nix package repository |nixpkgs| contains 2 million lines of code.}
125125
126126Refactoring existing code is also tricky since the generated expressions are only really checked for correctness\footnote{Here, ``correctness'' is used to mean the absence of evaluation-time errors.} at their evaluation time, and the evaluation time of expressions is difficult to predict due to the lazy nature of the language.
127127
128−Static type checking is the process of analyzing the types of expressions and detecting type errors in programs without evaluating them.
128+A 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
130130Even 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
@@ -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{\\n} which will be preserved as shown in listing~\ref{lst:newlineString}.
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}.
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 listing~\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}
@@ -190,7 +190,7 @@ Palnet''
190190
191191% \subsubsection{String interpolation}
192192
193−% The Nix Expression Language also allows for arbitrary expressions of the language to be interpolated in string using the following syntax: \texttt{\$\{ <expression> \}} where \texttt{<expression>} is a Nix expression.An example of string interpolation is show in listing~\ref{lst:stringInterpolation}.
193+% The Nix Expression Language also allows for arbitrary expressions of the language to be interpolated in string using the following syntax: \texttt{\$\{ <expression> \}} where \texttt{<expression>} is a Nix expression.An example of string interpolation is show in figure~\ref{lst:stringInterpolation}.
194194
195195% \begin{figure}
196196% \begin{minipage}{\textwidth}
@@ -206,7 +206,7 @@ Palnet''
206206
207207\subsection{Lists}
208208
209−Nix support 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 listing~\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}
@@ -220,7 +220,7 @@ Nix support a list type. List literals are enclosed by square brackets \texttt{[
220220
221221\subsection{Attribute sets} \label{sec:attrSet}
222222
223−An attribute set is internally implemented as a hashmap with strings as keys where values can be arbitrary expressions. An example attribute set literal is shown in listing~\ref{lst:attrSet}.
223+An attribute set is internally implemented as a hashmap with strings as keys where values can be arbitrary expressions. An example attribute set literal is shown in figure~\ref{lst:attrSet}.
224224
225225\begin{figure}
226226 \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 listing~\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}
@@ -254,7 +254,7 @@ Fields (keys) of an attribute set can be accessed through the \emph{dot} (\textt
254254
255255\subsection{Attribute set updates} \label{sec:update}
256256
257−There is a binary \emph{update} operator that takes two \emph{attribute sets} as operands and ``merges'' them in a shallow manner, preferring values from the right operand. The operator is written as two forward slashes \texttt{//}. This has the effect of updating the left operand with values from the right operand. An example is shown in listing~\ref{lst:update}.
257+There is a binary \emph{update} operator that takes two \emph{attribute sets} as operands and ``merges'' them in a shallow manner, preferring values from the right operand. The operator is written as two forward slashes \texttt{//}. This has the effect of updating the left operand with values from the right operand. An example is shown in figure~\ref{lst:update}.
258258
259259\begin{figure}
260260 \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} from 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 essentially available in scope of the attribute set values. An example of \emph{recursive attribute set} are given in listing~\ref{lst:recAttrSet}. Note that it is syntactically distiguished 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 form normal \emph{attribute set} literals by the \texttt{rec} key word at the beginning.
275275
276276\begin{figure}
277277 \begin{minipage}{\textwidth}
@@ -290,7 +290,7 @@ rec {
290290
291291\subsection{Let expressions} \label{sec:let}
292292
293−A \emph{let expression} has two parts: the \emph{declarations} and the \emph{body}. The format can be roughly described like so: \texttt{let <definitions> in <body>}. A \emph{let expression} allows us to define values in the \emph{declarations} that can be reused in the \emph{body} of the expression. Just like \emph{recursive attribute sets} from section~\ref{sec:recAttrSet} all declared values are available in scope in the defined expressions. An example of \emph{let expressions} is available in listing~\ref{lst:let}.
293+A \emph{let expression} has two parts: \emph{declarations} and the \emph{body}. The format can be roughly described like so: \texttt{let <definitions> in <body>}. A \emph{let expression} allows us to define values in the \emph{declarations} that can be reused in the \emph{body} of the expression. Just like \emph{recursive attribute sets} from section~\ref{sec:recAttrSet} all declared values are available in scope in the defined expressions. An example of \emph{let expressions} is available in figure~\ref{lst:let}.
294294
295295\begin{figure}
296296 \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 to bring 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 listing~\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 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}.
311311
312312\begin{figure}
313313 \begin{minipage}{\textwidth}
@@ -324,29 +324,31 @@ in d
324324
325325\section{Existing typecheckers}
326326
327−In 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 are the implementations.
327+In 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
329329\subsection{regnat/tix} \label{sec:regnat/tix}
330330
331−regnat/tix\footnote{\url{https://github.com/regnat/tix}} is an implementation of typechecker for the \emph{Nix Expression Language} implemented in \emph{OCaml}\footnote{\url{https://ocaml.org}}. The type checker itself is implemented on a different much simpler language named \emph{Nix Light}. To typecheck a normal \emph{Nix} program(expression) the program need to be first converted to an equivalent \emph{Nix Light} program. The type checker has a row-polymorphism-inspired feature: records are represented as a product of one-row types. In \emph{Nix Light} lists are represented as a single-liked heterogeneous list. The type system does not have support for parametric polymorphism in favour of a gradual typing paradigm.
331+regnat/tix\footnote{\url{https://github.com/regnat/tix}} is an implementation of a typechecker for the \emph{Nix Expression Language} implemented in \emph{OCaml}\footnote{\url{https://ocaml.org}}. The type checker itself is implemented on a different much simpler language named \emph{Nix Light}. To typecheck a normal \emph{Nix} program(expression) the program need to be first converted to an equivalent \emph{Nix Light} program. The type checker has a row-polymorphism-inspired feature: records are represented as a product of one-row types. In \emph{Nix Light} lists are represented as a single-linked heterogeneous list. The type system does not have support for parametric polymorphism in favour of a gradual typing paradigm.
332332
333333\parr{Status} The last commit was published in 2017 and the project is now abandoned in favour of regnat/ptyx which we examin in section~\ref{sec:regnat/ptyx}.
334334
335335\subsection{regnat/ptyx} \label{sec:regnat/ptyx}
336336
337−regnat/ptyx\footnote{\url{https://github.com/regnat/ptyx}} is in essence a reimplementation of regnat/tix in Haskell\footnote{\url{https://www.haskell.org}} which we examined in section~\ref{sec:regnat/tix}. The basic ideas and techniques are the same. In fact, so much so, that the simpler language is also called \emph{Nix Light} and \emph{Nix} expression are also converted to it before type checking. There is still no support for parametric polymorphism.
337+regnat/ptyx\footnote{\url{https://github.com/regnat/ptyx}} is in essence a reimplementation of regnat/tix in Haskell\footnote{\url{https://www.haskell.org}} which we examined in section~\ref{sec:regnat/tix}. The basic ideas and techniques are the same. In fact, so much so, that the simpler language is also called \emph{Nix Light} and \emph{Nix} expressions are also converted to it before type checking. There is still no support for parametric polymorphism.
338338
339339\parr{Status} The last commit was published in 2018. Unsupported language features include lists and attribute sets.
340340
341341\subsection{haskell-nix/hnix}
342342
343−haskell-nix/hnix\footnote{\url{https://github.com/haskell-nix/hnix}} is primarily not a typechecker, but rather the goal of the project is to fully reimplement the \emph{Nix Expression Language} interpreter in \emph{Haskell}. There is, however a number of modules dedicated to a typechecker implementation which was migrated into the project. Contrary to how it may seem, the typechecker is not integrated with the rest of the project in any significant way. The type system itself is based on the Hindley-Milner type system. However, the type system was not extended with additional features to better support the dynamic nature of \emph{Nix}. For instance, there is no support for row-polymorphism which greatly impedes typechecking any code that interacts with \emph{attribute sets} in any way.
343+haskell-nix/hnix\footnote{\url{https://github.com/haskell-nix/hnix}} is primarily not a typechecker, but rather the goal of the project is to fully reimplement the \emph{Nix Expression Language} interpreter in \emph{Haskell}. There is, however, a number of modules dedicated to a typechecker implementation which was migrated into the project. Contrary to how it may seem, the typechecker is not integrated with the rest of the project in any significant way. The type system itself is based on the Hindley-Milner type system. However, the type system was not extended with additional features to better support the dynamic nature of \emph{Nix}. For instance, there is no support for row-polymorphism which greatly impedes typechecking code that interacts with \emph{attribute sets} in any way.
344344
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
348348\section{Existing Approaches}
349349
350+In this section we will explore existing techniques used to develop typecheckers, and explore how they can be applicable to our implementation.
351+
350352\subsection{Type System Approach}
351353
352354There has been much research done in the field of type systems for functional programming languages. The most notable contribution was the introduction of the Damas-Milner\footnote{The Damas-Milner type system is sometimes referred to as the Hindley–Milner type system.} type system and the W inference algorithm~\cite{damas1982principal}, which was later proven to be sound and complete~\cite{vaughanproof}.
@@ -375,7 +377,7 @@ In some cases, this approach will likely yield too little information to be usef
375377
376378The original W inference algorithm is a single-stage inference algorithm, meaning that it attempts to satisfy type constraints as soon as it encounters them. A consequence of this is that errors are reported as soon as they are encountered. Often, the information available about the program at the time the error had occurred is very limited due to not all of the program being processed. This leads to poor error reporting.
377379
378−In contrast to the single-stage algorithm, the two-stage algorithm~\cite{jones2005practical,serrano2016type} collects the type constraints as the first stage of type checking and solves the collected constraints as a second step. This leads to most errors occurring during the second stage when all available type information has already been collected. As a result, better type errors are produced. This is the preferable approach for our goals.
380+In contrast to the single-stage algorithm, the two-stage algorithm~\cite{jones2005practical,serrano2016type} collects the type constraints as the first stage of type checking and solves the collected constraints as a second step. This leads to most errors occurring during the second stage when all available type information has already been collected. As a result, better type errors are produced. This is the more preferable approach for our goals.
379381
380382\subsection{Row-Polymorphism}
381383
@@ -383,13 +385,13 @@ One of the language-level constructs in the Nix Expression Language is the ``att
383385
384386There has been some research conducted in the field of type systems with row-polymorphic records~\cite{morris2019abstracting,leijen2005extensible}. The approach that should be taken in developing a static type checker for the Nix Expression Language is describing row-polymorphic attribute sets with a construct similar\footnote{The way it should be displayed to the user will be distinct, since, unlike in Haskell, the Nix Expression Language does not have constraints as a language construct.} to Haskell constraints~\cite{orchard2010haskell}.
385387
386−\subsection{Message Reporting}
388+% \subsection{Message Reporting}
387389
388−Displaying errors to the user is not as simple as it might initially seem. For the type checker to be as helpful as possible, error messages should display the encountered issues in the language contexts in which they had occurred. Ideally, the errors should point to the exact terms that are most likely problematic.
390+% Displaying errors to the user is not as simple as it might initially seem. For the type checker to be as helpful as possible, error messages should display the encountered issues in the language contexts in which they had occurred. Ideally, the errors should point to the exact terms that are most likely problematic.
389391
390−Even if all of the information necessary for detailed error messages is collected during type checking, displaying errors to the user is a problem that deserves its own research\footnote{This also relates to how types are laid out when displaying to the user even when no errors have occurred.}. The users might have different screen sizes. The error message should reflow all of the displayed text, code, and type annotations to accommodate the available space.
392+% Even if all of the information necessary for detailed error messages is collected during type checking, displaying errors to the user is a problem that deserves its own research\footnote{This also relates to how types are laid out when displaying to the user even when no errors have occurred.}. The users might have different screen sizes. The error message should reflow all of the displayed text, code, and type annotations to accommodate the available space.
391393
392−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.
393395
394396\section{Architecture}
395397
@@ -399,27 +401,28 @@ Hughes introduced a general-purpose algebraic pretty-printer~\cite{hughes1995des
399401
400402Developing a typechecker requires working with a large amount of non-trivial algorithms which influence each other in complex ways. A widespread way of dealing with such situations is introducing a common computational environment through which different parts of the program can interact (instead of ``manually'' passing state around). A well-established way of handling state in purely functional programming languages is the \emph{Monad} abstraction~\cite{moggi1988computational}.
401403
402−It is natural to want to abstract of the underlying monad – explicitly declare what features a function actually needs the monad to have. Furthermore, it is desireable to decompose the features of the a monad not only in function definitions, but also at the call site – it is desireable to be able to conjure up monads with desireable traits in an as-hoc manner. This has been achieved a while ago with \emph{monad transformers}~\cite{liang1995monad}.
404+It is natural to want to abstract the underlying monad – explicitly declare what features a function actually needs the monad to have. Furthermore, it is desireable to decompose the features of the a monad not only in function definitions, but also at the call site – it is desireable to be able to conjure up monads with desireable traits in an ad-hoc manner. This has been achieved a while ago with \emph{monad transformers}~\cite{liang1995monad}.
403405
404−A drawback of monad transformers is their somewhat rigid nature – every behavior a monad needs to have needs to be defined as a distinct transformer with appropriate instances. The instances need to only implement the desired behavior, but also explicitly ``pass through'' \emph{all} other effects that it might be used in combination with. This means that adding extra behavior leads to a large amount of boilerplate. Furthermore, monads themselves (monad transformers) are not in general composable, leading a whole other set of problems. In addition, it is cumbersome to locally change parts of the underlying implementation of a monad dynamically – it might be useful to tweak some behavior in only part of an algorithm, leaving the rest to the abstract implementation; monad transformers don't really have such capabilities.
406+A drawback of monad transformers is their somewhat rigid nature – every behavior a monad needs to have needs to be defined as a distinct transformer with appropriate instances. The instances need to not only implement the desired behavior, but also explicitly ``pass through'' \emph{all} other effects that it might be used in combination with. This means that adding extra behavior leads to a large amount of boilerplate. Furthermore, monads themselves (monad transformers) are not in general composable, leading to a whole other set of problems. In addition, it is cumbersome to locally change parts of the underlying implementation of a monad dynamically – it might be useful to tweak some behavior in only a part of an algorithm, leaving the rest to the abstract implementation; monad transformers don't really have such capabilities.
405407
406408\subsubsection{Free monad extensible effects}
407409
408−Recently a ne aprproach to effect systems has been getting more attention – \emph{free monads algebraic effects}~\cite{kiselyov2015freer, ploeg2014reflection, kiselyov2013extensible}. This approach solves the problems with monad transformers mentioned above. Rather than being transformers, effects are described as \emph{functors}. The composability problem is resolved due to functors being in general composable. Contrary to how monad transformers operate, effects (or their carriers) in \emph{free monads algebraic effects} (we will from now on refer to them as just \emph{algebraic effects}) don't have any particulare inrpretation of the effect associated with them. Effects are interpreted in an ad-hoc way at the call site. Furthermore this allows us to dynamically modify the behavior of effects without changing the types or implementations of functions we wish to change the behavior of. How we use \emph{algebraic effects} will be discussed in more detail in section~\ref{sec:implementation}.
410+Recently a new approach to effect systems has been getting more attention – \emph{free monads algebraic effects}~\cite{kiselyov2015freer, ploeg2014reflection, kiselyov2013extensible}. This approach solves the problems with monad transformers mentioned above. Rather than being transformers, effects are described as \emph{functors}. The composability problem is resolved due to functors being in general composable. Contrary to how monad transformers operate, effects (or their carriers) in \emph{free monads algebraic effects} (we will from now on refer to them as just \emph{algebraic effects}) don't have any particular interpretation of the effect associated with them. Effects are interpreted in an ad-hoc manner at the call site. Furthermore, this allows us to dynamically modify the behavior of effects without changing the types or implementations of functions we wish to change the behavior of.
411+% How we use \emph{algebraic effects} will be discussed in more detail in section~\ref{sec:implementation}.
409412
410413\section{Type system}
411414
412−As mentioned above, we have opted to use the Damas-Milner type system as a basis for our implementation. Our goal is not to just add types for the sake of types, but give additional reassurance to the developer, and reject as many potentially ``invalid'' programs as possible. If the developer typechecker processes a program without errors, then the program should have no type errors during execution.
415+As mentioned above, we have opted to use the Damas-Milner type system as a basis for our implementation. Our goal is not to just add types for the sake of types, but give additional reassurance to the developer, and reject as many potentially ``invalid'' programs as possible. If the developed typechecker processes a program without errors, then the program should have no type errors during execution.
413416
414417\subsection{Polymorphism} \label{sec:polymorphism}
415418
416−Dynamic languages have potenitally limitless polymorphism – you can pass anything of any type to any function and it can potentially work without errors – it is in principal possible to check the ``types'' of passed values at runtime. This leads to the fact that there is really no way to know which ``types'' are acceptable in which positions without executing the program.
419+Dynamic languages have potentially limitless polymorphism – you can pass anything of any type to any function and it can potentially work without errors – it is in principal possible to check the ``types'' of passed values at runtime. This leads to the fact that there is really no way to know which ``types'' are acceptable in which positions without executing the program.
417420
418421The Nix community, just like with any other language, has developed idiomatic ways of solving problems. Some of these idioms are heavily based on polymorphic behavior at runtime. We should strive to develop a type system which supports as much of idiomatic behavior as possible (and where not possible, similar behavior should be expressible within the type system).
419422
420423Parametric polymorphism has proven to strike a nice balance between strictness, expressiveness and type inference. We feel it will be most useful as a type system for \emph{Nix}.
421424
422−Inferring types with parametric polymorphism implies generalizing the inferred types at certain points in the program. Generalization is also known as ``closing over type variable'' – it can be though of as explicitly choosing a point where the variable is quantified over. Figure~\ref{fig:closing} is an example of closing for a type variable.
425+Inferring types with parametric polymorphism implies generalizing the inferred types at certain points in the syntax tree. Generalization is also known as ``closing over type variable'' – it can be though of as explicitly choosing a point where the variable is quantified over. Figure~\ref{fig:closing} is an example of closing over a type variable.
423426
424427Traditionally in languages similar to \emph{simply-typed lambda calculus} generalization is performed in \emph{let} declarations – so-called \emph{let-generalization}. \emph{Nix} has a very similar \emph{let} construct as discussed in section~\ref{sec:let} which is also a great point to perform type generalization.
425428
@@ -444,7 +447,7 @@ Recursive definitions pose a challenge for type inference without developer-supp
444447 \item The last implements a more complicated iteration-based type inference algorithm with a user-configurable number of iterations.~\cite{goldberg2000mercury} If the specified number of iterations is not enough to deduce the type of a recursive definition, it is rejected. The clear upside of this approach is that the inferred type (if it is given enough iterations and succeeds) is the principal (most general, most polymorphic) type of the expression.
445448\end{enumerate}
446449
447−While the last approach would allow us to in theory type more programs, we feel that tasking the user with configuring the typechecker would make the barrier to entry higher than it needs, and in practice the second approach would be useful enough (and faster), so that is the approach we chose to go with.
450+While the last approach would allow us to, in theory, type more programs, we feel that tasking the user with configuring the typechecker would make the barrier to entry higher than it needs to be, and in practice the second approach would be useful enough (and faster), so that is the approach we chose to go with.
448451
449452\subsection{Row polymorphism}
450453
@@ -452,7 +455,7 @@ Nix has first-class hashmaps with strings as keys called \emph{attribute sets} a
452455
453456Of course, since \emph{attribute sets} are used as structures, their internal structure (keys and types of values) has significance and should be tracked in types just like objects and structures are tracked in most statically typed programming languages. Even though it is in most cases implemented as a mechanism that allows the programmer to introduce new types which correspond to a static set of field names and types, and the type system is presented in terms of those types, this is not significantly different from tracking keys directly. In fact, the \emph{Go}\footnote{\url{https://golang.org}} programming language has a notion of \emph{protocols} which bridges the gap between the two paradigms.
454457
455−This leads to a non-trivial typechecking case where modifying a structure leads to the resulting type depending on the type of the input structure as shown in listing~\ref{lst:update_ex}. The listing shows a lambda expression which receives an \emph{attribute set} as input, and updates the field \texttt{a} with the value of \texttt{1}. It quickly becomes problematic to derive a type for this expression if we decide to track fields at the type level: we can say that the lambda takes a value of type \texttt{\{\}} and returns a value of type \texttt{\{a = Integer;\}} (type of functions will later be written as \texttt{<input type> -> <output type>}). This might seem a natural type to derive, however it is obviously not correct. Calling it with a values of type \texttt{\{b = String;\}} and \texttt{\{b = Float; a = Bool;\}} would both be very much valid, and would both produce different resulting types: \texttt{\{a = Integer; b = String;\}} and \texttt{\{a = Integer; b = Float;\}}. As stated above, the output type of a lambda expression like this depends on the input type.
458+This leads to a non-trivial typechecking case where modifying a structure leads to the resulting type depending on the type of the input structure as shown in figure~\ref{lst:update_ex}. The figure shows a lambda expression which receives an \emph{attribute set} as input, and updates the field \texttt{a} with the value of \texttt{1}. It quickly becomes problematic to derive a type for this expression if we decide to track fields at the type level: we can say that the lambda takes a value of type \texttt{\{\}} and returns a value of type \texttt{\{a = Integer;\}} (type of functions will later be written as \texttt{<input type> -> <output type>}). This might seem like a natural type to derive, however it is obviously not correct. Calling it with a values of type \texttt{\{b = String;\}} and \texttt{\{b = Float; a = Bool;\}} would both be very much valid, and would both produce different resulting types: \texttt{\{a = Integer; b = String;\}} and \texttt{\{a = Integer; b = Float;\}}. As stated above, the output type of a lambda expression like this depends on the input type.
456459
457460\begin{figure}
458461 \begin{minipage}{\textwidth}
@@ -493,7 +496,7 @@ The second predicate is:
493496where all rows from $\alpha$ are present in $\beta$. This predicate isn't strictly necessary, and can be expressed through predicate~\ref{eq:combination}:
494497
495498\begin{equation}
496− \alpha \clt \gamma = \exists \beta. \; \alpha \odot \beta \sim \gamma
499+ \alpha \clt \gamma = \exists \beta. \; \beta \odot \alpha \sim \gamma
497500\end{equation}
498501
499502Nevertheless, this predicate was still introduced as it closely matches the language term syntax and simplifies further processing of type.
@@ -527,7 +530,7 @@ The types of the other two expressions are not fully expressible with the predic
527530
528531When deciding how to model the four base row-related operations we decided to derive the predicates from the operations themselves. This would yield simpler types, and having simpler types for base operations leads to simpler types overall. Furthermore, the type system would in all likelihood be easier for Nix developers to use and understand if it is expressed in terms of familiar operations.
529532
530−We will not describe the row predicates we have chosen for Nix. Note the analogy with the enumeration from section~\ref{sec:nixRowPoly}.
533+We will now describe the row predicates we have chosen for Nix. Note the analogy with the enumeration from section~\ref{sec:nixRowPoly}.
531534
532535\newcommand{\update}{\mathbin{/\!\!/}}
533536\newcommand{\optDot}{.\!?}
@@ -540,7 +543,7 @@ We will not describe the row predicates we have chosen for Nix. Note the analogy
540543
541544The type $\alpha$ should be an attribute set and it should contain a field $x$ of the type $\beta$. This predicate arises from the use of the \emph{dot operator} (\texttt{.}) as discussed in section~\ref{sec:attrSet}. The syntax was chosen to be analogous to that of the Nix term syntax.
542545
543−The term \texttt{x: x.y} would field the following type:
546+The term \texttt{x: x.y} would yield the following type:
544547
545548\begin{equation} \label{eq:dotExample}
546549 \forall \alpha \beta. \; \alpha.\text{y} = \beta \Rightarrow \alpha \rightarrow \beta
@@ -554,7 +557,7 @@ The term \texttt{x: x.y} would field the following type:
554557
555558The type $\alpha$ should be an attribute set and if it contains the field $x$, then the type of the field should be $\beta$. This predicate arises from the combination of the \emph{dot operator} (\texttt{.}) and the \emph{or operator} (\texttt{or}) which is used to supply a fallback value if the attribute set does not contain the required field. The syntax was chosen to be analogous to that of the Nix term syntax.
556559
557−The term \texttt{x: x.y or 1} would field the following type:
560+The term \texttt{x: x.y or 1} would yield the following type:
558561
559562\begin{equation} \label{eq:optFieldPredExample}
560563 \forall \alpha. \; \alpha \optDot \text{y} = \text{Number} \Rightarrow \alpha \rightarrow \text{Number}
@@ -562,7 +565,7 @@ The term \texttt{x: x.y or 1} would field the following type:
562565
563566This predicate also arises from the use of the \emph{attribute set field presence check operator} (\texttt{?}). In that case the
564567
565−The term \texttt{x: x ? y} would field the following type:
568+The term \texttt{x: x ? y} would yield the following type:
566569
567570\begin{equation} \label{eq:optFieldPredExample2}
568571 \forall \alpha \beta. \; \alpha \optDot \text{y} = \beta \Rightarrow \alpha \rightarrow \text{Bool}
@@ -574,9 +577,9 @@ The term \texttt{x: x ? y} would field the following type:
574577 \alpha \update \beta \sim \gamma
575578\end{equation}
576579
577−All $\alpha$, $\beta$ and $\gamma$ should be \emph{attribute sets}. The \emph{attribute set} $\gamma$ should contain all fields from both $\alpha$ and $\beta$, preferring the types from $\beta$ if they happen to overlap. That is, if $\alpha$ and $\beta$ both contain a field with the same name, then $\gamma$ should contain the same field with the type from $\beta$. This behaviour matches the way the \emph{update operator} (\texttt{//}) works as discussed in section~\ref{sec:update}.
580+All $\alpha$, $\beta$ and $\gamma$ should be \emph{attribute sets}. The \emph{attribute set} $\gamma$ should contain all fields from both $\alpha$ and $\beta$, preferring the types from $\beta$ if they happen to overlap. That is, if $\alpha$ and $\beta$ both contain a field with the same name, then $\gamma$ should contain the same field with the type from $\beta$. This behavior matches the way the \emph{update operator} (\texttt{//}) works as discussed in section~\ref{sec:update}.
578581
579−The term \texttt{x: y: x // y} would field the following type:
582+The term \texttt{x: y: x // y} would yield the following type:
580583
581584\begin{equation} \label{eq:updatePredExample}
582585 \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma
@@ -632,7 +635,7 @@ For this reason, we will have to define a smaller set of static types that will
632635
633636\subsection{Addition} \label{sec:addition}
634637
635−Among all operators, addition (\texttt{+}) has semantics that stand out from the rest: addition can be applied to wither two \texttt{Number} operands or two \texttt{String} operands. All other operands are monomorphic in that they can only be applied to two operands of a predefined type. In that sense addition in polymorphic.
638+Among all operators, addition (\texttt{+}) has semantics that stand out from the rest: addition can be applied to either two \texttt{Number} operands or two \texttt{String} operands. All other operands are monomorphic in that they can only be applied to two operands of a predefined type. In that sense addition in polymorphic.
636639
637640Since our current implementation does not support sum types (see section~\ref{sec:sumTypes} for more detail), it is non-trivial to encode the type of addition in our current type system. We wanted to encode the type without having to resort to extending the type system too much (without implementing sum types).
638641
@@ -650,7 +653,7 @@ With this predicate the type of the addition operator (\texttt{+}) now becomes:
650653
651654\subsection{Typing rules}
652655
653−What follows is a formal description of the developed type system. For brevity we have omitted rules for typing literal constant values described in tables \ref{tab:atomicTypes} and \ref{tbl:staticTypes}, and most operators described in table~\ref{tbl:allOperators} as these rules are trivial.
656+What follows is a formal description of the developed type system. For brevity we have omitted rules for typing literal constant values described in tables \ref{tab:atomicTypes} and \ref{tbl:staticTypes}, and most operators described in table~\ref{tbl:allOperators} as those rules are trivial.
654657
655658\subsubsection{Lists}
656659
@@ -686,7 +689,7 @@ Typing rules for both lambda abstraction definitions and application is common a
686689
687690\subsubsection{Addition}
688691
689−The rational for having a special case for the addition operator is layed out in section~\ref{sec:addition}:
692+The rationale for having a special case for the addition operator is layed out in section~\ref{sec:addition}:
690693
691694\begin{equation}
692695 \trfrac
@@ -784,8 +787,8 @@ With that we can define how those predicate are actually satisfied:
784787
785788\begin{equation}
786789 \trfrac
787− {\Gamma \vdash e.\text{x} = \tau}
788− {\Gamma \vdash (e \optDot \text{x}) = \tau}
790+ {\Gamma \vdash \tau_1.\text{x} = \tau_2}
791+ {\Gamma \vdash (\tau_1 \optDot \text{x}) = \tau_2}
789792\end{equation}
790793
791794where $(\text{x} = \tau) \in \xi$ denotes the presence of the \emph{row} $(\text{x} = \tau)$ in the \emph{set} $\xi$, and $\text{x} \notin \xi$ denotes the absence of a \emph{row} with the key `x' in the \emph{set} $\xi$.
@@ -810,7 +813,7 @@ The definition of the ``update'' predicate uses standard set comprehension notat
810813
811814\emph{with expressions} do, however, pose a particularly hard problem when implementing the type system – we can't always statically know the fields in $e_1$ -- it can be passed in as a function argument. This means that the typing environment of a function can depend on its argument. Implementing this in a wholistic manner would require our type system support a form of dependent types. That is not a direction we want to pursue -- introducing dependent types would greatly complicate the type system to a point where automated type inference would not practical and the type system would be a lot harder to work with.
812815
813−Instead, we opted to define a heuristic which in our testing was proven to cover most practical cases: when encountering a variable in the body of a with expression:
816+Instead, we opted to define a heuristic which in our testing was proven to cover most practical cases: when encountering a variable in the body of a \emph{with expression}:
814817
815818\begin{enumerate}
816819 \item if a variable was defined in the body of the with expression and is in scope, return that type
@@ -869,8 +872,8 @@ In our implementation the application of substitutions is delayed as much as pos
869872This choice has several implications. Firstly, we can never have conflicting ``keys'' in substitutions (which is not the case in other implementations). Using this information we can define stronger substitution composition:
870873
871874\begin{code}
872−newtype Substitution =
873− Substitution {unSubstitution :: Map TypeVariable NType}
875+newtype Substitution = Substitution
876+ {unSubstitution :: Map TypeVariable NType}
874877
875878instance Semigroup Substitution where
876879 a'@(Substitution a) <> b'@(Substitution b) =
@@ -901,14 +904,15 @@ The typing context in our implementation in essence consists of two distinct dat
901904
902905\subsubsection{Variables in scope}
903906
904−Note that in practice it only needs to contain type variables since we apply substitutions as late as possible.
907+Note that in practice the ``variables in scope'' data structure only needs to contain type variables since we apply substitutions as late as possible.
905908
906909In 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}}:
907910
908911\begin{code}
909912data VariableMapEff x where
910913 LookupVariable
911− :: VarName -> VariableMapEff (Maybe Scheme)
914+ :: VarName
915+ -> VariableMapEff (Maybe Scheme)
912916
913917lookupVar
914918 :: Member VariableMapEff eff
@@ -933,10 +937,10 @@ data MultiKeyedMap t = MultiKeyedMap
933937 (M.Map (Key t) (S.Set t)) (S.Set t)
934938\end{code}
935939
936−The data structure contains is the product of two other data structures:
940+The data structure is the product of two other data structures:
937941
938942\begin{enumerate}
939− \item A map, mapping possible keys of the stored |t| to a set of values the contains the given key
943+ \item A map, mapping possible keys of the stored |t| to a set of values the contain the given key
940944 \item A set which contains the values that don't contain any keys
941945\end{enumerate}
942946
@@ -952,7 +956,7 @@ instance (Ord (Key t), Ord t)
952956 (M.unionWith S.union x y) (x' <> y')
953957\end{code}
954958
955−Creating a singleton map from a single values is defined like this:
959+Creating a singleton map from a single values is defined like so:
956960
957961\begin{code}
958962singleton :: Keyable t => t -> MultiKeyedMap t
@@ -973,7 +977,7 @@ insert
973977insert t m = m <> singleton t
974978\end{code}
975979
976−Now we come to the lookup operation. Not that the algorithmic complexity of querying the predicates by a type they contain is now the cost of an ordinary map lookup -- $O(log(n))$ where $n$ is the number of values contained in the map (in our case thw number of all types referenced from within the predicates):
980+Now we come to the lookup operation. Note that the algorithmic complexity of querying the predicates by a type they contain is now the cost of an ordinary map lookup -- $O(log(n))$ where $n$ is the number of values contained in the map (in our case the number of all types referenced from within the predicates):
977981
978982\begin{code}
979983lookup
@@ -994,9 +998,9 @@ An observation we can make is the following: it only makes sense to close over t
994998
995999This 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.
9961000
997−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 is 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.
1001+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.
9981002
999−A solution we came up with is two 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:
1003+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:
10001004
10011005\begin{code}
10021006data TypeVariable
@@ -1039,7 +1043,7 @@ When applied to the type~\ref{eq:updatePredExample} it yields:
10391043 \forall \alpha \beta. \; \alpha \rightarrow \beta \rightarrow (\alpha \update \beta)
10401044\end{equation}
10411045
1042−We believe the derived type above are a lot easier to understand than their initial counterparts.
1046+We believe the derived types above are a lot easier to understand than their initial counterparts.
10431047
10441048\subsubsection{Implementation notes}
10451049
@@ -1074,7 +1078,7 @@ The idea of this improvement is to generalize the case and allow the type system
10741078 \alpha \lessdot \beta
10751079\end{equation}
10761080
1077−where $\beta$ can be the type $\alpha$. With this predicate, our ``String or Number'' predicate can be expressed as so:
1081+where $\beta$ can be the type $\alpha$. With this predicate, our ``String or Number'' predicate can be expressed like so:
10781082
10791083\begin{equation}
10801084 \strOrNum \sim \alpha = (\text{String} \lessdot \alpha, \text{Number} \lessdot \alpha)