@@ -0,0 +1,288 @@
1+\documentclass[12pt]{article}
2+
3+\usepackage{xcolor}
4+\usepackage[hidelinks]{hyperref}
5+
6+\newcommand{\todo}{\addcontentsline{toc}{subsection}{{\color{red}\textbf{TODO}}}{\LARGE\color{red}\textbf{TODO}}}
7+
8+\newcounter{req}
9+
10+\newcommand{\req}[1][]{\refstepcounter{req}\label{req:#1}\paragraph{\fbox{\textsf{\textsc{REQ}-\thereq}}}}
11+\newcommand{\refreq}[1]{\hyperref[req:#1]{\fbox{\textsf{REQ-\ref*{req:#1}}}}}
12+
13+\title{Technical Specification for the Language Server for the Nix Expression Language}
14+\author{Kostyuchenko Ilya}
15+\date{}
16+
17+\begin{document}
18+
19+\maketitle
20+
21+\newpage
22+
23+\tableofcontents
24+
25+\newpage
26+
27+\section{Purpose}
28+
29+The purpose of Tix is to simplify development in the Nix expression language.
30+
31+\section{Scope}
32+
33+The project consists of developing the following components:
34+
35+\paragraph{The Tix type checker} is a program which is designed to statically analyze the given Nix expression language source code and deduce the types of subexpressions used within while detecting some errors made by the programmer (type mismatch errors, which usually arise due to programming mistakes).
36+
37+\paragraph{The Tix language server} is a program which implements the Language Server Protocol and is used to integrate the Tix type checker with existing code editors to aid with development.
38+
39+\section{Product perspective}
40+
41+\subsection{System interfaces}
42+
43+The application runs on the latest versions of macOS and Linux.
44+
45+\subsection{User interfaces}
46+
47+The application does not provide a user interface.
48+
49+\subsection{Hardware interfaces}
50+
51+The application does not provide a hardware interface.
52+
53+\subsection{Software interfaces}
54+
55+The application allows interactions through the Language Server Protocol.
56+
57+\subsection{Communications interfaces}
58+
59+The application communicates with the code editor process through the Language Server Protocol using JSON-RPC requests. These requests can be over the network or local to the machine โ however, the user decides to set it up.
60+
61+\subsection{Memory}
62+
63+The memory required to run the system depends on the size of the project being processed. Typical projects should are processed within a 2 GB memory limit.
64+
65+\subsection{Operations}
66+
67+The application supports the following operations initiated by the code editor:
68+
69+\begin{enumerate}
70+ \item Typecheck the current file and report errors
71+ \item Go to the definition of a variable
72+ \item Identify the type of a selected expression expression
73+\end{enumerate}
74+
75+\subsection{Site adaptation requirements}
76+
77+No site adaptations are required.
78+
79+\subsection{Interfaces with services}
80+
81+No interaction with services in performed.
82+
83+\section{Product functions}
84+
85+The application provides the following functionality to the user:
86+
87+\begin{enumerate}
88+ \item While the user is editing a Nix expression language file the application will indicate potentially incorrect subexpressions based on type mismatches
89+ \item While the user is exploring a Nix expression language project the application will provide:
90+ \begin{enumerate}
91+ \item type information for subexpressions the user is inspecting
92+ \item definitions of variables a user is inspecting
93+ \end{enumerate}
94+\end{enumerate}
95+
96+\section{User characteristics}
97+
98+The user of the application will need intermediate technical skills to set up the application to work with their text editor of choice. More precisely, the user will need to have the following (approximate and incomplete) list of skills:
99+
100+\begin{enumerate}
101+ \item Understand on a high level what a language server is and its role in code editing
102+ \item Be familiar with the repositories of packages for their text editor of choice
103+ \item Be able to perform intermediate configuration of their text editor of choice and installed packages
104+ \item Have basic server administration skills if they are planning to run the server remotely
105+\end{enumerate}
106+
107+\section{Limitations}
108+
109+\subsection{Interface to other applications}
110+
111+The integration with the text editor of choice should be compatible with version 3.15 of the Language Server Protocol.
112+
113+\subsection{Criticality of the application}
114+
115+The software should not be used for critical applications as it is not capable of eliminating all runtime errors, or even eliminating all runtime type errors due to the dynamic nature of the underlying Nix expression language\footnote{Type systems inherently restrict some valid programs, and some expressions might not be well-typed, but execute without errors.}.
116+
117+\section{Assumptions and dependencies}
118+
119+The contents of this document assume the following:
120+
121+\begin{enumerate}
122+ \item The application will be used on a UNIX-like system that is supported by the Glasgow Haskell Compiler.
123+ \item All dependencies of the files being processed should be locally downloaded by Nix.
124+\end{enumerate}
125+
126+\section{Apportioning of requirements}
127+
128+The application is a self-contained executable file that, when executed, functions as a standalone language server. The only requirement that the application externally imposes is the requirement to set up the language sever to function with the desired text editor. There already exist numerous implementation for language server support for many text editors.
129+
130+\section{Specified requirements}
131+
132+\req[restrictons] The system should perform all static program analysis (instances of such analysis link to this requirement) under the following conditions:
133+\begin{enumerate}
134+ \item it is possible to perform analysis without (partially) evaluating expressions
135+ \item all input data linked to from the expressions being analyzed is locally downloaded by Nix
136+\end{enumerate}
137+
138+\req[typechecking] The system should perform type checking for expression where under conditions from \refreq{restrictons}.
139+
140+\req The system should analyze conditional statements where the condition consists only of type checks and boolean operators built into the Nix expression language.
141+
142+\req The system should analyze the types and presence of attributes in attribute sets under conditions from \refreq{restrictons}.
143+
144+\req The system should report encountered typechecking errors through means defined by the Language Server Protocol.
145+
146+\req The system should provide the location of definitions for all locally used terms under conditions from \refreq{restrictons}.
147+
148+\req The system should report the use of undefined terms through means defined by the Language Server Protocol under conditions from \refreq{restrictons}.
149+
150+\req The system should report the types of requested expressions through means defined by the Language Server Protocol if the type of the requested expression is unambiguously inferable during typechecking (\refreq{typechecking}).
151+
152+\req The system should provide code completions suggestions from the variables currently in scope and expressions built into the language under conditions from \refreq{restrictons}.
153+
154+\req The system should provide a way for the programmer to explicitly annotate types of expressions which will influence type checking.
155+
156+\section{Usability requirements}
157+
158+\req The system should be able to process expressions using the nixpkgs repository.
159+
160+\req The system should never fail in unrecoverable ways in external imported expressions โ if there are type errors in external code the system should resolve the errors automatically.
161+
162+\section{Performance requirements}
163+
164+\req The system should process incoming requests within 1 second (the system should formulate a response, not necessarily finish performing the requested action).
165+
166+\req The system should process incoming requests from a single client.
167+
168+\section{External interfaces}
169+
170+The only external interface of the system is the Language Server Protocol.
171+
172+\paragraph{The purpose} of this interface is to provide easy interoperability with a wide range of potential code editors a user might want to use\footnote{\url{https://microsoft.github.io/language-server-protocol/implementors/tools/}}.
173+
174+\paragraph{The source of input} is the code editor the user uses sending requesting information about the semantics of the file currently being edited in response to the actions the user is taking while browsing or editing source code in the Nix expression language.
175+
176+\paragraph{The destination of the input} is the code editor the user is using which has requested information about the source code.
177+
178+\paragraph{Data and command formats} are defined by the Language Server Protocol\footnote{\url{https://microsoft.github.io/language-server-protocol/specifications/specification-current/}}.
179+
180+\section{Functions}
181+
182+The fundamental functions of the system are queries: get the type of an expression, get the definition of a variable, get code completion. All of the responses to the queries can be generated from an \emph{analysis context} which is generated from the current file the user is viewing and any other files it imports.
183+
184+If the context \emph{analysis context} is already generated then the responses are formulated as follows. If the \emph{analysis context} is not present, then it is generated prior to processing the request.
185+
186+\subsection{Generating the type of an expression}
187+
188+\begin{enumerate}
189+ \item the system queries the expression at the requested position in the source code from the \emph{analysis context}
190+ \item the system queries the type of the expression from the \emph{analysis context}
191+ \item the system returns the type
192+\end{enumerate}
193+
194+\subsection{Generating the definition of a variable}
195+
196+\begin{enumerate}
197+ \item the system queries the expression at the requested position in the source code from the \emph{analysis context}
198+ \item the system asserts that the expression is a variable reference
199+ \item the system queries the definition of the given variable reference from the \emph{analysis context}
200+ \item the system returns the definition
201+\end{enumerate}
202+
203+\subsection{Generating completions}
204+
205+\begin{enumerate}
206+ \item the system queries the variables in scope at the requested position in the source code from the \emph{analysis context}
207+ \item the system formulates a list of possible completions
208+ \item the system filters the list of possible completions based on the prefix already typed by the user
209+ \item the system returns the list of filtered possible completions
210+\end{enumerate}
211+
212+\subsection{Generating the analysis context}
213+
214+\begin{enumerate}
215+ \item the current file is parsed
216+ \item dependencies are gathered from the current file and the analysis context is recursively generated for all dependencies
217+ \item the current file is typechecked
218+ \begin{enumerate}
219+ \item type constraints are recursively generated for all subexpressions
220+ \item encountered variable definitions are gathered
221+ \item encountered variable references are gathered
222+ \item undefined variable definitions are gathered
223+ \item type constraints are generated for the given top-level expression
224+ \item type constraints are sequentially solved. If a typing error is encountered, the error is gathered with other errors and the problematic type is replaced with a polymorphic type to allow further typechecking
225+ \end{enumerate}
226+ \item all errors gathered during typechecking are reported to the user through means defined by the Language Server Protocol
227+ \item all analysis contexts are merged into a single analysis context
228+ \item the resulting analysis context is the returned
229+\end{enumerate}
230+
231+\subsection{Error handling}
232+
233+If the system encounters a typing error in the user's code, then the error is returned to the user through means defined in the Language Serer Protocol.
234+
235+If the system encounters an internal (as opposed to a user error) the error is written to the standard error output.
236+
237+\section{Design constraints}
238+
239+The main design constraint is the fact that the Nix expression language is a dynamic language without an underlying static type system. This implies that there will be correct programs that will be ill-typed. The system should be designed in such a way as to gracefully handle such situations.
240+
241+\section{Software system attributes}
242+
243+\subsection{Reliability}
244+
245+\begin{enumerate}
246+ \item The system should automatically recover from any user error after the user resolves the error in code.
247+ \item The system should not enter unrecoverable states.
248+\end{enumerate}
249+
250+\subsection{Maintainability}
251+
252+The system should utilize free monad algebraic effects for managing side-effects as they improve maintainability by decoupling implementation from abstraction.
253+
254+\subsection{Portability}
255+
256+\begin{enumerate}
257+ \item The system should not contain host-dependant code
258+ \item The system should be written in the Haskell programming language which is not host-dependent
259+ \item The system should be compiled with the Glasgow Haskell Compiler as it supports a wide range of platforms
260+\end{enumerate}
261+
262+\section{Verification}
263+
264+The following approaches and methods are planned to be employed to qualify the software:
265+
266+\begin{enumerate}
267+ \item Automated hand-written unit-tests
268+ \item Automated randomly generated property tests
269+ \item Manual testing
270+\end{enumerate}
271+
272+\section{Supporting information}
273+
274+\subsection{Nix}
275+
276+Nix is a powerful package manager for Linux and other Unix systems that makes package management reliable and reproducible.\footnote{Taken from \url{https://nixos.org}}.
277+
278+\subsection{Nix expression language}
279+
280+The Nix expression language is a purely functional dynamic strictly typed programming language used for configuration in the Nix package manager. It does not support defining custom types โ all types are defined within the interpreter. The main purpose of the language is to produce \emph{derivation} โ a description of how to build an artifact\footnote{\url{https://nixos.org/manual/nix/stable/\#ssec-derivation}}.
281+
282+\subsection{The problem to be solved}
283+
284+When working with the Nix expression language it is often the case that imported expressions (nixpkgs) are quite large, and it is not obvious what needs to be called with what arguments. It is often necessary to inspect the source code of imported files to grok how it should be used and if the current use is correct.
285+
286+This project aims to lighten the burden of development in the Nix expression language by providing some level of machine-generated introspection into the imported expressions and provide some level of verification of the correctness of the implementation.
287+
288+\end{document}