Contracts for free!
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 542 | |
| Author | ||
| License | CC Attribution 2.0 Belgium: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/61604 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
FOSDEM 2023152 / 542
2
5
10
14
15
16
22
24
27
29
31
36
43
48
56
63
74
78
83
87
89
95
96
99
104
106
107
117
119
121
122
125
126
128
130
132
134
135
136
141
143
146
148
152
155
157
159
161
165
166
168
170
173
176
180
181
185
191
194
196
197
198
199
206
207
209
210
211
212
216
219
220
227
228
229
231
232
233
236
250
252
256
258
260
263
264
267
271
273
275
276
278
282
286
292
293
298
299
300
302
312
316
321
322
324
339
341
342
343
344
351
352
354
355
356
357
359
369
370
372
373
376
378
379
380
382
383
387
390
394
395
401
405
406
410
411
413
415
416
421
426
430
437
438
440
441
443
444
445
446
448
449
450
451
458
464
468
472
475
476
479
481
493
494
498
499
502
509
513
516
517
520
522
524
525
531
534
535
537
538
541
00:00
Design by contractFreewareDiagram
00:07
Functional (mathematics)Library (computing)Run time (program lifecycle phase)Type theoryGroup actionCodePhysical systemConsistencyError messageFunction (mathematics)Formal languageConstructor (object-oriented programming)FunktorPairwise comparisonInfinityPerformance appraisalImage resolutionLoop (music)Template (C++)Design by contractInternetworkingSimilarity (geometry)LoginHash functionPasswordEmailField (computer science)Attribute grammarTelephone number mappingUsabilityComputer configurationRegulärer Ausdruck <Textverarbeitung>Configuration spaceLibrary (computing)Error messagePhysical systemComputer configurationMultiplication signFluid staticsValidity (statistics)Function (mathematics)Formal languageProjective planeMacro (computer science)Complex (psychology)Type theoryShared memoryImplementationRun time (program lifecycle phase)CASE <Informatik>NeuroinformatikDifferent (Kate Ryan album)MereologyExpressionReal numberDesign by contractSpacetimePoint (geometry)Right angleGeneric programmingElectronic program guideTypprüfungComputer programmingComputer animation
05:52
Program flowchart
Transcript: English(auto-generated)
00:05
Okay, please welcome our next speaker, Ivan, to talk about contracts for free. Hi everyone, it's a really quick talk about the Akitoy project and some unpopular opinions about using runtime types.
00:29
So, the thing is, there is an old issue, maybe you know it, in Nix, which was closed since because it will never be implemented, which is a bit embarrassing about the fact that Nix have no any static type system.
00:45
And the thing is, I changed my mindset relatively recently about that, but I will talk about it later, because what's the issue about the type system? It's the lack of a static type system,
01:01
it's the error you get, you get them at the last moment, it's really inconsistent regarding where the mistake were made, and when you read your stack trace, you get hard time to find what was the actual error. And that is really not helpless for, for example, beginners trying to work on Nix expression,
01:22
or people trying to debug Nix expression right then by other person. So, I changed my mindset because Nix is a really simple language, and it should be a simple language, and it invites us to build constructs in library space.
01:42
And if you look at Nix built-ins, for example, it's really few built-ins, and a lot of things that could be built-ins are actually implemented as Nix package libsing. And there is a Nix package lib types, maybe without an S, which is what you use when you define Nix option,
02:01
to say the option could be that or that and everything. And so, I changed my mindset because Nix is made in two steps, you know, so the first step is that you evaluate the language and produce things in Nix, or you symbolize Nix store, and after you build, you made your package,
02:24
but the instantiate part is guaranteed to terminate. You know you will, the computation will always terminate, which is what you'll expect for a type system, actually, and which is not the case of some type system or most of macro systems that are not expected to terminate,
02:42
so actually it's a good guarantee. And that's why we could do a lot of things in Nix. You can see it as, I changed my mind because I see that Nix is not really about runtime and programming language, so we could do a check at runtime.
03:03
And I wrote a thing while vacation and realized later that other folks already did it, which is Tashjian, maybe you know him, he works on Twix right now, and he also writes Nix one-pager, one of the best Nix starting guides at some point.
03:22
And the thing is, it's really simple, you define the data you want, just validator functions, so you say, I want something like that, and you check at this point of your expression, what it evaluates, that's its respect to a contract or validator function,
03:42
and that helps, actually, the error to fail early, where you want it to fail. There are differences in implementation I will not talk really about, but I, as a really simple liberal, didn't rely on Nix pack-wage, and it's fully compatible with Nix exception, so you can define a thing and share them,
04:04
and the last thing is, those composes, I go back inside, you can define types, you can define validator, instruct that became validator, and you can compose really complex things, because it's really expressive.
04:22
And also the nice things with runtime types is you can produce recoverable error, which is the case for types errors that exist in Nix itself, so for example, this will be un-recoverable, but if you use the runtime type, you will recover the situation.
04:41
Last thing is, I try to advertise this kind of technique, because it helps a lot to debug your prediction, and to have assertion about this respect and everything. This does not really solve the problem, because it's not a real type system, actually,
05:06
but if you're not starting something from scratch, if you're actually working on an existing Nix expression, an expression could be actually really large. I think personally it helps if you're starting a new thing from scratch, there's really cool things like Q, Dal, Nickel, generic JSON,
05:23
and you leave the Nix package so you can use it really easily, and there is also, I like personally ProNix, because it generates Nix output rather than JSON. Okay, I think I said most of what I would say,
05:42
so don't hesitate if you have a question or want to share opinion. We don't have time for questions. You don't have time? No, okay. Thank you. Thank you. It was really good.