@@ -0,0 +1,405 @@
1+build-lists: true
2+slidenumbers: true
3+footer: Kostyuchenko Ilya, Static analyzer for the Nix Expression Language
4+
5+[.header: alignment(center), Avenir Next]
6+
7+
8+## Static analyzer for the Nix Expression Language
9+
10+### Статический анализатор для Nix Expression Language
11+
12+<br>
13+<br>
14+
15+_Author:_ Kostyuchenko Ilya
16+
17+_Supervisor:_ Victor Kuliamin, Associate Professor, PhD
18+
19+---
20+
21+> Nix is a powerful package manager that makes package management reliable and reproducible.
22+-- [nixos.org](https://nixos.org)
23+
24+---
25+
26+[.build-lists: false]
27+
28+# Nix
29+
30+- Package manager
31+- Build system*
32+- Ad hoc development environments
33+- Easy (cross-community) dependency management
34+- Reproducible builds
35+- *And much more: NixOS, NixOps, Build Caching, Docker ...*
36+
37+---
38+
39+[.build-lists: false]
40+
41+# Nix Expression Language
42+
43+[.column]
44+
45+- Purely functional
46+- Lazy
47+- **Strict, but not static typing**
48+
49+[.column]
50+
51+```nix
52+let pkgs = import ./nixpkgs {};
53+in derivation {
54+ name = "simple";
55+ builder = "${pkgs.bash}/bin/bash";
56+ args = [ ./simple_builder.sh ];
57+ gcc = pkgs.gcc;
58+ coreutils = pkgs.coreutils;
59+ src = ./simple.c;
60+ system = builtins.currentSystem;
61+}
62+```
63+
64+---
65+
66+[.text: text-scale(0.75)]
67+
68+# Terms and definitions
69+
70+**Type system** – a logical system comprising a set of rules that assigns a property called a type to the various constructs of a computer program
71+
72+**Type checking** – the process of verifying and enforcing the constraints of types.
73+
74+**Hindley–Milner type system** – a classical type system for the lambda calculus with parametric polymorphism.
75+
76+**Parametric polymorphism** – a type of polymorphism where types are specified by abstract symbols that can represent any type.
77+
78+**Row polymorphism** – a kind of polymorphism that allows one to write programs that are polymorphic on record field types.
79+
80+---
81+
82+# Relevance
83+
84+The Nix ecosystem is slowly becoming popular.
85+
86+The central repository contains more than 60000 packages.
87+
88+There is a need to make writing Nix expressions less error-prone.
89+
90+
91+
92+---
93+
94+# Relevance
95+
96+Nix Expression Language: **Strict, but not static typing**.
97+
98+Adding static typing would:
99+
100+- Increase reliability of code
101+- Lower costs of development (resolving issue earlier is cheaper)
102+
103+_The typechecker should help find issues in existing code_
104+
105+---
106+
107+# The goal
108+
109+1. Develop a type static system for the existing Nix expression language
110+2. Develop a type checker for this type system
111+
112+---
113+
114+# Existing typecheckers
115+
116+- github.com/regnat/ptyx – Abandoned and incomplete.
117+- github.com/regnat/tix – An older version of ptyx. Abandoned, terribly incomplete.
118+- github.com/haskell-nix/hnix – has a module with a type checker. Is very experimental and is not used.
119+
120+---
121+
122+# Existing approaches
123+
124+Type systems for functional languages is an actively researched field.
125+
126+The Hindley–Milner type system_[1]_ is a simple, but well-studied type system for a very simple language. It is fully decidable, does not require annotations. It is the basis for many real-world type systems.
127+
128+---
129+
130+# Functional requirements
131+
132+- The system should perform type checking on expression.
133+
134+- The system should analyze the types and presence of attributes in attribute sets.
135+
136+- The system should report encountered typechecking.
137+
138+- The system should report the use of undefined terms.
139+
140+- The system should report the resulting types of expressions to the user.
141+
142+---
143+
144+[.text: text-scale(0.85)]
145+
146+# Methods and algorithms
147+
148+The type system will be heavily influenced by the Hindley–Milner_[1]_ type system.
149+
150+The type system will implement parametric polymorphism to support code that does not require a specific type.
151+
152+The type system will implement arbitrary-ranked polymorphism_[3]_ with deep instantiation to disambiguate types in existing untyped code.
153+
154+The type system will implement row polymorphism to work with attribute sets.
155+
156+---
157+
158+[.build-lists: false]
159+
160+# Used tools
161+
162+1. Haskell
163+2. Visual Studio Code
164+3. Haskell Language Server
165+4. Haskell Stack
166+
167+---
168+
169+# Implementation
170+
171+The typechecker is implemented in a two-step architecture:
172+
173+1. Inferring the types of terms and collecting constraints
174+2. Solving the collected constraints
175+
176+---
177+
178+# Current results
179+
180+A typechecker executable that successfully typechecks _most_ of the selected files from _nixpkgs_.
181+
182+The typechecker currently has some support for all language constructs.
183+
184+
185+
186+---
187+
188+[.build-lists: false]
189+
190+# Current results
191+
192+## Paper status
193+
194+1. Nix Expression Language (80%)
195+2. Existing typecheckers (100%)
196+3. Existing approaches (100%)
197+4. Architecture (20%)
198+5. Implementation (0%)
199+6. Conclusion (60%)
200+
201+
202+
203+---
204+
205+# What is left
206+
207+- Better type rendering (predicates)
208+- Subsumption
209+- A lot of minor big fixes in type inference
210+- Add type information about built-in functions
211+
212+---
213+
214+# Potential future developments
215+
216+- Add support for user-supplied type annotations.
217+ - Fork parser
218+ - Bidirectional type inference_[4]_
219+- Type holes
220+- Language Server Integration
221+
222+---
223+
224+[.build-lists: false]
225+[.text: text-scale(0.7)]
226+
227+# References
228+
229+1. Damas L., Milner R. Principal type-schemes for functional programs //Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. – 1982. – С. 207-212.
230+2. Jones S. P. et al. Practical type inference for arbitrary-rank types //Journal of functional programming. – 2007. – Т. 17. – №. 1. – С. 1-82. MLA
231+3. Stuckey P. J., Sulzmann M., Wazny J. Improved inference for checking type annotations //arXiv preprint cs/0507036. – 2005. MLA
232+
233+---
234+
235+# Demonstration
236+
237+---
238+
239+## Parametric polymorphism
240+
241+```nix
242+let f = x: y: { a = x; b = y + 1;}; in f
243+```
244+
245+```
246+∀ α. α -> Integer -> {a = α; b = Integer;}
247+```
248+
249+---
250+
251+## Parametric polymorphism
252+
253+```nix
254+let f = x: y: { a = x; b = y + 1;}; in f
255+```
256+
257+```
258+∀ α. α -> Integer -> {a = α; b = Integer;}
259+```
260+
261+<br>
262+
263+```nix
264+let f = x: y: { a = x; b = y + 1;}; in f "hello" 42
265+```
266+
267+```
268+{a = String; b = Integer;}
269+```
270+
271+---
272+
273+## Row-polymorphism with _attribute sets_
274+
275+```nix
276+let f = x: x.a; in f
277+```
278+
279+```
280+∀ α β. (α.a = β) => α -> β
281+```
282+
283+---
284+
285+
286+
287+## Row-polymorphism with _attribute sets_
288+
289+```nix
290+let f = x: x.a; in f
291+```
292+
293+```
294+∀ α β. (α.a = β) => α -> β
295+```
296+
297+<br>
298+
299+```nix
300+let f = x: x.a; in f {a = 1; b = "hello";}
301+```
302+
303+```
304+Integer
305+```
306+
307+---
308+
309+## Row-polymorphism with _attribute sets_
310+
311+```nix
312+let f = x: x.a; in f
313+```
314+
315+```
316+∀ α β. (α.a = β) => α -> β
317+```
318+
319+<br>
320+
321+```nix
322+let f = x: x.a; in f {a = "1"; b = "hello";}
323+```
324+
325+```
326+String
327+```
328+
329+---
330+
331+## Row-polymorphism with _attribute sets_
332+
333+```nix
334+let f = x: x.a; in f
335+```
336+
337+```
338+∀ α β. (α.a = β) => α -> β
339+```
340+
341+<br>
342+
343+```nix
344+let f = x: x.a; in f {b = "hello";}
345+```
346+
347+```
348+Error: key "a" NotPresent in { b = String; }
349+```
350+
351+---
352+
353+## Row-polymorphism with _attribute sets_
354+
355+```nix
356+let f = x: x // {a = 69;}; in f
357+```
358+
359+```
360+∀ α β. (α // {a = Integer;} ~ β) => α -> β
361+```
362+
363+---
364+
365+## Row-polymorphism with _attribute sets_
366+
367+```nix
368+let f = x: x // {a = 69;}; in f
369+```
370+
371+```
372+∀ α β. (α // {a = Integer;} ~ β) => α -> β
373+```
374+
375+<br>
376+
377+```nix
378+let f = x: x // {a = 69;}; in f {a = "hello"; b = "world";}
379+```
380+
381+```
382+{a = Integer; b = String;}
383+```
384+
385+---
386+
387+## Row-polymorphism with _attribute sets_
388+
389+```nix
390+let f = x: x // {a = 69;}; in f
391+```
392+
393+```
394+∀ α β. (α // {a = Integer;} ~ β) => α -> β
395+```
396+
397+<br>
398+
399+```nix
400+let f = x: x // {a = 69;}; in f {}
401+```
402+
403+```
404+{a = Integer;}
405+```