@@ -20,8 +20,9 @@ _Supervisor:_ Victor Kuliamin, Associate Professor, PhD
2020
2121---
2222
23−> Nix is a powerful package manager that makes package management reliable and reproducible.
24−-- [nixos.org](https://nixos.org)
23+## Nix is a powerful package manager that makes package management reliable and reproducible.
24+
25+#### – [nixos.org](https://nixos.org)
2526
2627---
2728
@@ -102,14 +103,14 @@ Adding static typing would:
102103- Increase reliability of code
103104- Lower costs of development (resolving issue earlier is cheaper)
104105
105−_The typechecker should help find issues in existing code_
106+<!-- _The typechecker should help find issues in existing code_ -->
106107
107108---
108109
109110# The goal
110111
111−1. Develop a type static system for the existing Nix expression language
112−2. Develop a type checker for this type system
112+1. Develop a static type system for the existing Nix expression language
113+2. Develop a type checker for this static type system
113114
114115---
115116
@@ -129,31 +130,48 @@ The Hindley–Milner type system_[1]_ is a simple, but well-studied type system
129130
130131---
131132
132−# Functional requirements
133+# Methods and algorithms
133134
134−- The system should perform type checking on expression.
135+The developed type system is heavily influenced by the Hindley–Milner_[1]_ type system.
135136
136−- The system should analyze the types and presence of attributes in attribute sets.
137137
138−- The system should report encountered typechecking.
138+---
139139
140−- The system should report the use of undefined terms.
140+# Methods and algorithms
141141
142−- The system should report the resulting types of expressions to the user.
142+The developed type system supports parametric polymorphism to support code that does not require a specific type.
143143
144−---
144+```nix
145+x: y: x ++ y
146+```
145147
146−[.text: text-scale(0.85)]
148+```
149+∀ α. [α] -> [α] -> [α]
150+```
151+
152+---
147153
148154# Methods and algorithms
149155
150−The type system will be heavily influenced by the Hindley–Milner_[1]_ type system.
156+The developed type system implements row polymorphism to work with attribute sets.
151157
152−The type system will implement parametric polymorphism to support code that does not require a specific type.
158+```nix
159+x: x.v + 69
160+```
153161
154−The type system will implement arbitrary-ranked polymorphism_[3]_ with deep instantiation to disambiguate types in existing untyped code.
162+```
163+∀ α. (α.v = Number) => α -> Number
164+```
155165
156−The type system will implement row polymorphism to work with attribute sets.
166+<br />
167+
168+```nix
169+x: x // {v = "hello";}
170+```
171+
172+```
173+∀ α β. (α // {v = String;} ~ β) => α -> β
174+```
157175
158176---
159177
@@ -177,49 +195,28 @@ The typechecker is implemented in a two-step architecture:
177195
178196---
179197
180−# Current results
181−
182−A typechecker executable that successfully typechecks _most_ of the selected files from _nixpkgs_.
183−
184−The typechecker currently has some support for all language constructs.
185−
186−
187−
188−---
189−
190−[.build-lists: false]
191−
192−# Current results
193−
194−## Paper status
198+# Results
195199
196−1. Nix Expression Language (80%)
197−2. Existing typecheckers (100%)
198−3. Existing approaches (100%)
199−4. Architecture (20%)
200−5. Implementation (0%)
201−6. Conclusion (60%)
200+- Theoretical
201+ - A static type system for the Nix Expression Language
202202
203−
203+- Practical
204204
205−---
205+ - A typechecker executable that successfully typechecks _most_ of the selected files from _nixpkgs_.
206206
207−# What is left
207+ - The typechecker supports all language constructs.
208208
209−- Better type rendering (predicates)
210−- Subsumption
211−- A lot of minor big fixes in type inference
212−- Add type information about built-in functions
209+
213210
214211---
215212
216213# Potential future developments
217214
218215- Add support for user-supplied type annotations.
219− - Fork parser
220− - Bidirectional type inference_[4]_
221216- Type holes
222217- Language Server Integration
218+- Better type rendering
219+- Sum types
223220
224221---
225222
@@ -228,9 +225,10 @@ The typechecker currently has some support for all language constructs.
228225
229226# References
230227
231−1. Damas L., Milner R. Principal type-schemes for functional programs //Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. – 1982. – С. 207-212.
232−2. Jones S. P. et al. Practical type inference for arbitrary-rank types //Journal of functional programming. – 2007. – Т. 17. – №. 1. – С. 1-82. MLA
233−3. Stuckey P. J., Sulzmann M., Wazny J. Improved inference for checking type annotations //arXiv preprint cs/0507036. – 2005. MLA
228+1. L. Damas and R. Milner, “Principal type-schemes for functional pro- grams,” in Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1982, pp. 207–212.
229+2. E. Dolstra and A. Lo ̈h, “Nixos: A purely functional linux dis- tribution,” in Proceedings of the 13th ACM SIGPLAN international conference on Functional programming, 2008, pp. 367–378.
230+3. J. G. Morris and J. McKinna, “Abstracting extensible data types: or, rows by any other name,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 1–28, 2019.
231+4. D. Leijen, “Extensible records with scoped labels.” Trends in Functional Programming, vol. 6, pp. 179–194, 2005.
234232
235233---
236234
@@ -347,7 +345,7 @@ let f = x: x.a; in f {b = "hello";}
347345```
348346
349347```
350−Error: key "a" NotPresent in { b = String; }
348+Error: key "a" not present in { b = String; }
351349```
352350
353351---