Does anybody know where I can find the natural deduction rules which specify the semantics of the module-merge?
I feel like I don’t fully understand what they can’t do, which is how I usually feel about programming language features until I’ve read the deduction rules. I’m guessing that if @roberth doesn’t know where to find them they probably don’t exist yet. If you already know what natural deduction is you can skip the rest of this message.
Natural deduction rules are the gold standard for specifying semantics in programming languages. They’re the diagrams that look like gigantic fractions. You can find examples of these starting on page 78 of @edolstra’s thesis, Figures 6 and 7 of the NixOS ICFP paper, and even in the Nixpkgs Manual cross compilation section!
Natural deduction rules are a little bit like Prolog programs, but they aren’t limited to Horn clauses or a particular search algorithm. Unlike Prolog they are higher-order: the goals can have free variables and the rules can express constraints on free variables. Twelf and λProlog were two attempts at creating a “higher-order Prolog.”
Natural deduction rules are a terrible introduction to pretty much any topic. They’re really hard to read until you have a general idea of what’s going on. But once you’ve been shown the “big picture”, natural deduction rules are the way to go for exploring all the “dark corners” of the system. In particular, if there’s a rule or behavior missing, that underspecification will be very obvious from looking at the rules.
4 Likes
I’m not aware of any.
Natural deduction rules are a terrible introduction to pretty much any topic.
I can’t disagree.
I’ve tried to write an introduction by introducing the concepts one by one in code. Wasn’t quite happy with that. Maybe deduction rules aren’t much worse? At least they’re more of a proper model instead of an ad hoc approximation.
cc @Infinisil @nbp, seen natural deduction rules for the module system by any chance?
2 Likes
I have not, I’d also be interested!
1 Like
I find lattice theory / ordered sets an extremely useful model to understand the multifaceted data overlays that render the final view (i.e. .config).
If there are natural deduction rules (I have no idea how they look and feel in context) for ordered sets, they probably partially apply modulo type checking.
That can’t:
- use the same priority twice.
- … ?
Maybe interesting questions would arise at the submodule boundary?
So, what would you say is currently the best resource for learning the gory details of exactly what is or is not possible with modules?
If just reading lib/modules.nix carefully is the answer, I’ll do that.
Also: @roberth, at one point you mentioned that there was a way to get the merge operation to not just merge, but also read-modify-write the value it was being merged with. I think the name had “transform” in it? But I haven’t managed to figure out what that functionality was. Could you remind me? That read-modify-write operation surprised me, and seemed totally inconsistent with my mental model of what the merge operation can do, so I assume my mental model is wrong. Trying to fix that is what led to this thread.