| 11 Dec 2025 |
 hexa | * can't do
${foo} = "bar"
but you can do
foo.${bar} = "baz"
| 22:39:34 |
 emily | overlays can be quite easily typed with row types. | 22:39:56 |
 KFears (burnt out) | Yeah, that's also weird... I'm not sure about it, like, it's convenient, but it feels weird, like I'd maybe expect a builtin that allows creating those kinds of arbitrarily-named attributes instead of it being a syntax thing | 22:41:57 |
| emily | e.g.
Overlay : Row -> Row -> Row -> Type
Overlay Final Prev Extra = {...Final} -> {...Prev} -> {...Extra}
data Overlays : Row -> Row -> Type where
nil : forall Final. Overlays Final {}
cons : forall Final Prev Extra. Overlay Final Prev Extra -> Overlays Final Prev -> Overlays Final (Prev // Extra)
addsFoo : forall Final Prev. Overlay Final Prev {foo : …}
addsFooUsingBar : forall FinalR Prev. Overlay (FinalR // {bar : …}) Prev {foo : …}
changesFoo : forall Final PrevR. Overlay Final (PrevR // {foo : …}) {foo : …}
changesFooUsingBar : forall FinalR PrevR. Overlay (FinalR // {bar : …}) (PrevR // {foo : …}) {foo : …}
(function to evaluate these left as an exercise)
| 22:48:44 |
| emily | I'd say it's not really that much different to typing TypeScript objects tbh | 22:49:49 |
 raitobezarius | ~~Now do IFDs~~ | 23:20:26 |
 Charles | Box<dyn Any> | 23:25:25 |
 rosssmyth | Sure, row polymorphism works but in reality a type theory that uses that would be really poor in practice | 23:43:27 |
| rosssmyth | And some types may be infinitely large | 23:44:50 |
| rosssmyth | * Sure, row polymorphism works but in reality a type theory that uses that would be really poor to use in practice | 23:45:38 |
| 12 Dec 2025 |
| emily | because of recursive object types? sure, that is just the problem any OOP language has to deal with really | 00:47:11 |
| emily | I don't think there are many challenges for the Nix case here that TypeScript does not already have to deal with (admittedly it sacrifices soundness) | 00:47:27 |
| emily | the Nix attrset typing case is also not far off what 1ML does FWIW | 00:47:58 |
| emily | (I do think there are things that would make typing existing Nixpkgs idioms somewhat painful, but I don't think the basic attrset system is the big issue there) | 00:50:34 |
|  whispers (it/fae) changed their profile picture. | 04:51:24 |
 aloisw | In reply to @commentator2.0:elia.garden
What about scala sytle no brackets at all and just :: between the elements? :D
i.e.
a :: b :: c
/j That looks like something that only works well when the lists are linked lists. | 06:35:56 |
| aloisw | In reply to @piegames:flausch.social
We need them for attrsets obviously, and a way to access those, but we already have that. Having a "foo bar" key is important, but having a variable named "foo bar" in a let binding? What for? I agree that having the variable in the let binding may not be that important in itself, but there's also the module-like use case of attrsets and you kinda need identifiers to be able to represent all keys to not have weird edge cases (think "with/inherit/let open … in (or whatever it may be called) only works under these specific conditions on the keys"). | 06:40:22 |
| emily | (I agree that raw identifier reference syntax is preferable to banning raw identifier binding) | 11:28:25 |
 helle (just a stray cat girl) | It will be interesting to do any nixlang2 work in such a way that in addition to writing the spec, we at the same time write the tutorial for people who have never touched nix (and aren't functional language or compiler nerds, etc), because this would show things that are hard to explain to beginners | 11:35:03 |
| helle (just a stray cat girl) | and note, if you can write something differently to what you tell beginners, they still need to be able to understand what is written | 11:35:24 |
| emily | lazy evaluation is going to be a tough one no matter what (and intimately tied to the nested fixed point structures the package set and module system builds up). in some ways easier to explain to someone without an (imperative) programming background than with | 12:56:15 |
| emily | the combination with dynamic typing has the fun side effect of burying errors as deep/late as possible and also making it much harder to trace the causes of them, which is just an awful property for learners | 12:58:24 |
 teo (they/he) | fwiw some of the spooky fixed point stuff can be explained to people in terms of inheritance which is a bit more familiar sometimes | 13:11:11 |
| teo (they/he) | * fwiw some of the spooky fixed point stuff can be explained to people in terms of inheritance which is a bit more familiar sometimes. although that assumes people actually understand that :) | 13:11:49 |
| emily | I think you can get some way with that for the way the package set is built up from overlays, but it's a bit weird since you're talking about using the already-esoteric mixins to form an inheritance chain and even that fails to capture why attrsets being strict in their keys causes tons of infrec unless you're careful
(admittedly one can ignore much of this for most use, but same applies to the vast majority of the Nix language)
| 13:28:56 |
| emily | for the module system... I think the analogy is hard to stretch | 13:29:13 |
| emily | it is very much taking fixed points of a Weird Monoid | 13:29:44 |
| emily | with in fact multiple layers of monoidal structure (merging of module definitioms, overrides, and the individual option types and their merge operations) and where the definitions for some of the monoids involved are themselves part of the values the monoidal structure applies to and also these pervasively recurse into each other 🤪 | 13:32:58 |
| emily | I suspect the median NixOS user models each definition in their configuration modules as essentially imperative mutation of global state | 13:34:36 |
| teo (they/he) | the module system is a monster! but it is very convenient | 13:34:38 |
