andremedeiros has quit [Quit: ZNC 1.8.2 - https://znc.in]
andremedeiros has joined #nix-lang
siraben has quit [Ping timeout: 245 seconds]
siraben has joined #nix-lang
mcint has quit [Ping timeout: 246 seconds]
globin_ has joined #nix-lang
globin has quit [Ping timeout: 240 seconds]
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
<aaronjanse>
Aha! I figured out how to cache evaluated values across edits, so auto-complete for `with pkgs; [ <typing here> ]` is now as fast as you can type :D
mcint has joined #nix-lang
<siraben>
Is there a formal semantics for Nix?
<siraben>
The closest I could find is the PhD thesis which gives a small-step operational semantics
globin_ has quit [Ping timeout: 245 seconds]
globin_ has joined #nix-lang
mcint has quit [Quit: just do it!!!]
mcint has joined #nix-lang
<sterni>
pretty sure no
evanjs has quit [Read error: Connection reset by peer]
evanjs has joined #nix-lang
Synthetica has joined #nix-lang
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
<pie_>
lol formal semantics for nix
<pie_>
:c
<siraben>
Reading the operational semantics it seems let is desugared to a recursive attr set lol
<siraben>
pie_: Is it possible at all? I think Nix could be "well behaved" (I might be entirely wrong)
<siraben>
Or have a well-behaved fragment
<siraben>
The latter is like the work on Oxide (a formally verified subset of Rust)
<siraben>
Even formalizing Eelco's proofs about the rules producing closed terms might be a good start for formal work in Nix
<Profpatsch>
siraben: I want to see you formalize the interaction of with and let lol
<Profpatsch>
I mean it would probably help some people understand it
<Profpatsch>
But e.g. to formalize the type coercion rules of strings (with and without context) and path … good luck
<aaronjanse>
Nix simply searches the scope without `with`, then evaluates the `with` only when an identifier isn't found
<Profpatsch>
Although it would be interesting to finally have a full type of all builtins
<aaronjanse>
So `let a = 1; with { a = 2; }; a` is `1` but if you remove the `let` it becomes `2`
<siraben>
Profpatsch: ah a formal semantics need not imply a type system haha
<siraben>
as in, when you have an "ill typed" term, no evaluation rule applies
<siraben>
so it gets stuck
<aaronjanse>
In other words, adding `with` can only change a variable from undefined from defined
<siraben>
Profpatsch: yeah, I will need to see more details later
<siraben>
I should warm up by formalizing simply-typed lambda calculus, with records
<aaronjanse>
Side note, the pointer equality thing is required to evaluate Nixpkgs :-/
<siraben>
uh oh
<siraben>
lol that would complicate a formal semantics considerbaly
<siraben>
considerably
<aaronjanse>
Because without it, `localSystem != crossSystem`
<aaronjanse>
Since the attr sets have lambdas
<siraben>
equality of expressions is "syntactic" according to the thesis
<siraben>
Ok so there's Nix-light which Nix compiles to, looks like records are simplified
<siraben>
Hmm
<siraben>
Lol semantics and typing of the with construct are omitted
lukegb has quit [Ping timeout: 252 seconds]
lukegb has joined #nix-lang
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
<pie_>
aaronjanse: Profpatsch siraben: I was mostly being snarky about all the weird corner cases that come from implementation details
<tazjin>
<siraben> Is there a formal semantics for Nix? <- I am working on a language spec, and the next step there would be formalising it (though I'm not sure how much benefit we'll derive from that, at least for my personal goals)
<tazjin>
my evaluator design is converging on a modified krivine machine, for which there'll be defined evaluation semantics (but they're kind of implementation-specific)
<tazjin>
<aaronjanse> Side note, the pointer equality thing is required to evaluate Nixpkgs :-/ <- we should fix this
<puck>
i've already looked into this before, it's very much non-trivial
<tazjin>
puck: as a thought experiment, what would happen if function equality was over equality of the function's AST (as supplied by the user, maybe at most with de-bruijn indexing)?
<puck>
what does it mean for a function to be equal to another? is it if they behave exactly the same? is it if they are the same defined object?
<tazjin>
I gave a definition
andremedeiros has quit [Read error: Connection reset by peer]
<Profpatsch>
can we remove the equality on the struct with functions, and use the string triplet instead?
<Profpatsch>
imo we shouldn’t even do function equality
<Profpatsch>
we should error out
<puck>
this means that if someone accidentally passes a function into a thing, it'll explode
<Profpatsch>
yes
<Profpatsch>
as it should
andremedeiros has joined #nix-lang
<tazjin>
Profpatsch: sounds good, will you refactor everything to do with `system`? :p
<Profpatsch>
tazjin: huh, as I said, why not compare the string repr
<puck>
tazjin: also doing it based on AST breaks sealers
<Profpatsch>
like e.g. python does for objects
<puck>
Profpatsch: nix already does this
<puck>
> { type = "derivation"; outPath = "foo"; bar = "baz"; } == { type = "derivation"; outPath = "foo"; quux = "lol"; }
<{^_^}>
true
<tazjin>
is that actually because of string repr, or because attribute sets are represented as a sorted list?
<tazjin>
like both of these are read into the same structure in memory
<tazjin>
oh wait
<tazjin>
what!
<tazjin>
that's terrible
<puck>
eh
<Profpatsch>
you can set outPath?
<Profpatsch>
I mean I guess don’t do that
<puck>
> let a = { type = "derivation"; outPath = "foo"; bar = "baz"; }; in "${a}"
<{^_^}>
"foo"
<puck>
special-case in stringifying
<puck>
> let a = { type = "derivation"; outPath = "foo"; bar = "baz"; }; in builtins.toJSON a
<{^_^}>
"\"foo\""
<puck>
anyways, i actually abuse function inequality in a project, and it being AST-based breaks a design concept i'm using
<Profpatsch>
so don’t abuse it
<Profpatsch>
like, somebody abusing it doesn’t mean we shouldn’t get rid of it
<tazjin>
my take is that formalising the language semantics should accommodate nixpkgs, but not external projects
<tazjin>
and then once that's done we have a clear line in the sand
<puck>
let seal = value: let key = (a: null); in [ key (a: if { inherit a; } == { a = key; } then value else builtins.throw "invalid key") ]
<puck>
(untested code, but should work)
<puck>
actually, wow, that doesn't work, and afaict not even because of issues in my code
<puck>
man i wonder what i ended up doing /differently/ for it to work
<puck>
presuming evaluation order, hahah
<puck>
seal = value: let key = { __key = (a: null); }; in [ key (a: if a == key then value else builtins.throw "invalid key") ]
__monty__ has joined #nix-lang
<pie_>
puck: tazjin: just supply multiple equality operators for gods sake
<tazjin>
please no more features
<puck>
oh i need those anyways
<pie_>
well if you want to shove a bunch of differnt equality opreators into one bad one you can hav e == :)
<lukegb>
can we have == and === and =~=
<tazjin>
what's the actual minimum required function equality nixpkgs depends on
<lukegb>
semantics are left up to the reader
<tazjin>
so it's pointer equality, which means that it should be the same literal definition
<tazjin>
it could just be defined as that, and how the implementation handles that is up to it
<puck>
> let inf = 1.79e308 * 2; nan = inf / -inf; in [ (nan == nan) (nan > nan
<puck>
) (nan < nan) (nan >= nan) (nan <= nan) ]
<{^_^}>
error: syntax error, unexpected $end, at (string):495:1
<tazjin>
(check definition positions, check pointer equality if you have that, ...)
<pie_>
is it really that hard to have a separate pointer equality and structural equality operator
<tazjin>
pie_: no, but that is a different language, also it doesn't really solve the problem here
<pie_>
or whatever it was
<tazjin>
since you're comparing a structure that contains things compared by pointer equality
<pie_>
(idek what is going on here specifically)
<tazjin>
so you'd have to write a `systemEquals` function and use the right operators in the right fields
<pie_>
i just know i had problems with *something* here.
* pie_
returns to the shadows
<sterni>
puck: what do you need seal for
<sterni>
do I even wanna know
<sterni>
tazjin: I think for the system stuff you can probably just introduce some equality thing depending on type or something
<sterni>
tazjin: but I think it'd be better just to refactor it
<sterni>
already now it's a bit stupid since for example not everything making up the platform ends up in parsed
<sterni>
which means that pkgsMusl (which only switches out parsed) will potentially alter your platform in an unexpected way
<tazjin>
sterni: if we can come up with a refactoring plan that would be ideal
<tazjin>
it would be great if the new evaluators could converge on a standard that is the minimum required to evaluate nixpkgs, so that we can start dropping some of the nutty things
<sterni>
it doesn't even to be motivated by evualtion entirely
<sterni>
it'd also be great for nixpkgs itself probably to clean this up
<sterni>
but it's a bit of a task I can imagine
<sterni>
I don't understand it fully yet and it kind of scares me :p
<sterni>
but I feel like there is a lot of nuance to it and also tsuff tacked on bit by bit
<sterni>
for example useLLVM is kinda significant, but it doesn't end up in parsed which other stuff relies on
<sterni>
“kinda significant” == nobody uses it lol
<sterni>
well wasm targets I think
<puck>
<sterni> puck: what do you need seal for <- what *don't* you need a sealer for
<tazjin>
nixpkgs
<sterni>
puck: I'm not sure I have never used one consciously
<puck>
tazjin: why not rename nixlang to nixpkgslang then
<tazjin>
I just want to get to a stable base constrained by the most important use of the language before committing to any of its current features
<tazjin>
we can probably get rid of a lot of cruft with some cleanup
<Profpatsch>
+1
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
andremedeiros has quit [Read error: Connection reset by peer]
andremedeiros has joined #nix-lang
mcint has quit [Quit: just do it!!!]
mcint has joined #nix-lang
evanjs has quit [Read error: Connection reset by peer]
evanjs has joined #nix-lang
evanjs has quit [Read error: Connection reset by peer]
evanjs has joined #nix-lang
rajivr has quit [Quit: Connection closed for inactivity]
andremedeiros has quit [Read error: Connection reset by peer]