Nix value representation.

[layus]

At the moment there remains at least two different values representation in HNix, and the ambiguity is killing performance and any ability to refactor or otherwise tune execution of the code.

1. We have NValue ~= Free (NValue' NValue) | Pure thunk. That is, our main value type is either a WHNF value or a thunk.
2. The other standard seems to pass around (m v) actions for things that are yet unevaluated (akin to thunks) and v for evaluated values.

The confusion arises because we mix all the hnix contexts (monads). There is an haskell execution context (think IO) and a nix execution context (think Context). But they are indistinguishable ! It appears clearly in the thunk :: m v -> m v signature, where we wrap an action into a value. We would expect it to be m v -> v, but the thunk mechanism itself relies on IO. It would make sense to distinguish these contexts. What about evalM whnf -> execM v ?

This raises a second puzzle for me: There is no way to tell thunks from WHNF values. A generic value can be either, but in many cases we know more than that. For example demand :: m v -> m v gives not information at all to the type system. But we know that the result of demand cannot be a thunk, so we could type it deamnd :: m v -> m v' where v' is the type of WHNF values (an NValue' in most cases).
I did that in a branch, and it works, with a negligible performance loss.

The implementation of demand is also a puzzle. On Pure t values, it is demand =<< force t. We see that we force the thunk, and continue demanding values as long as the thunk evaluation yields another thunk.
We see that there are two levels of thunks. Thunks at the NValue level (Pure t) and thunks at the MonadThunk level (t). Having both defeats the purpose of locking thunks, because the chain of thunks being forced is interrupted, and thus the loop detection mechanism aborted.

My experiment discovered that it does not happen because eval ensures it does not happen (once in all the test suite, possibly a bug to be discovered).
The experiment removed a single demand in eval and suddenly there were inifinite evaluations in some tests testing the absence of divergence. Because we are not backed by the types, we can miss invocations of demand.
The experiment also showed that we can drop some invocations of demand too. At some place, we demand things that cannot be thunks.

My point is that we are not leveraging the types to convey enough information about our values. I guess it results from the history of the project.
Or because or types are already quite convoluted ? (think forall e t f m. )

[Anton-Latukha]

Sorry for not giving a response right away. Still need to process the idea to respond with continuation.

[layus]

My experiment discovered that it does not happen because eval ensures it does not happen (once in all the test suite, possibly a bug to be discovered).

This part is wrong, We do rightfully have thunks into thunks, when we pass a thunk as a function argument. All the funtion arguments are thunked by default, creating a thunk stack. It is how the code works.

[Anton-Latukha]

What I know is that the Eval and Parse stages of HNix are intertwined. Because Nix import eagerly parses and evaluates files.

[layus]

If we compare with nix, we find a clever optimisation where thunking only happens on complex expressions https://github.com/NixOS/nix/blob/fb0ad898ed0f1c8d5297f5dc1035b2e6ac7e3632/src/libexpr/eval.cc#L680-L726

We cannot do that in our eval because it is kind of a fold (see adi) and eval is NExprF (m v) -> m v. At the time of eval, the NExprF children have already been evaled. That is weird for a lazy interpreter, so I am considering breaking the adi abstraction and use raw eval recursion.

[Anton-Latukha]

To pile on the topic.

"Haskell High Performance Programming" (2016 book) reminds us that the HNix thunk implementation bears an additional ineffectiveness - in that it uses & manipulates references as values - a thing which GHC can not optimize in any way & mutable references additionally prone to accumulate thunks "it's deceptively easy to accidentally accumulate a big chain of unreferenced thunks in an IORef, because modifyIORef is not strict in its second argument", it talks about IORef, we mostly use Control.Monad.Ref but that is hardly any difference - the approach is still a complex fragile & ineffective. Since profiling does not show what eats memory - everything eats equally - it may be thunks get suspended & hanging everywhere, it may be this thunking system (maybe deferred thunks?).

Maybe at least it looks like it can be possible for force to become just atomicModifyRef, because after refactoring it the hell looks like as an implementation of one, & there is strict in both arguments atomicModifyRef'.

And Obsidian guys not changed that thing.

I wonder at the basic idea of it: why abstracting & simulating thunking are that much needed, while it is an inherent concern/property of Haskell to manage it effectively. If only to be easy enough to defer. Maybe getting rid of the concept of thunks altogether & relying on that languages are essentially the same, so that GHC becomes an "already good enough" thunking mechanism for HNix, and we just profile & control strictness of evaluation right in the Haskell code, a bonus for it would be - inherent concurrency & ease to enhance concurrency of the project code through any (default &) available Haskell means.

It would've been great if someone experienced in the question looked at it again & at least made suggestions.

[Anton-Latukha]

Yes. If to formulate fundamentally: separately construct a lazy system & evaluation mechanism & control, inside already lazy language & tooling it exposes ... seems as a very complex & redundant task I know no points, moreover a sum of ones that validates/explains the creation of & to take on that complex task that produced ... effects unto the project. With a caveat of my ignorance on the reasons.

[layus]

Yes. If to formulate fundamentally: separately construct a lazy system & evaluation mechanism & control, inside already lazy language & tooling it exposes ... seems as a very complex & redundant task I know no points, moreover a sum of ones that validates/explains the creation of & to take on that complex task that produced ... effects unto the project. With a caveat of my ignorance on the reasons.

My current understanding is that it is not the same kind of lazyness, and that forces upon us another layer of thunks. Haskell lazyness is only about pure computations, but nix is lazy in side-effect actions. Haskell is not lazy in monadic actions. Not sure if that makes sense though.

[Anton-Latukha]

Hmm... Interesting.

So having a continuation-passing style in a thunk mechanism maybe was a good code to have.

It is a pity that things are done and not explained.

Or to say properly:

It seems thunk mechanism would not be needed if effects are programmed in a continuation-passing style to give effects call-by-value. So we pass effects around, until we return them at the end of processing of effects by calling them. Therefore wrapping the effect storage into State monad & storing effects there until calling them into IO - may be a good idea.

In any case, collecting all actions into a structure then sequenceA on them to run them into IO - that is what I call good design. I love when IO actions are stored & then through sequenceA "fused" & executed sequentially at once - when I see that - I know something is done right.

[Anton-Latukha]

If to think further.

NValue is implemented as a Free monad. That creates shenanigans. People already complained at strangeness of the main type, & type signatures during any work blow up. Yesterday I tried again to make main value type a newtype - & GHC can not bear that. Free monad is used exactly for purposes of running unknown structure at runtime. Free monads are used for easy prototyping & Kmett (& others) has a rule: if dunno - implement in a Free monad, search for homomorphism (comparability) to some other Monad & build them, when search is matched - remove the Free monad.

It also goes with the idea of putting things into accumulator & then doing something once for all of them.

Collecting effects lazily directly connects with NValue Free monad - after lazy effects - a homorphism should be seen as obvious to replace Free with concrete implementation. In the result - with lazy effects & NValue as a proper type - the thunking system probably woudn't be needed at all. Why would we have one - if we have lazy effects & lazy language.

I'd indeed appreciated, if we distinguished lazy thanks, WHNF (& evaluation & execution were pointed-out & put clearly through the type system) and NF values.

As I am stupid - I think stupidly - I gradually do these simple moves.

Therefore from all insight you say - besides agreeing with other things, I react most strongly to v' - it is a thing that needs to be done in any course of events. I stongly agree.

[Anton-Latukha]

As I understood type system was deliberately was done that polymorphic & open.
I agree that the type system is too open, it does not provide enough information & type safety.

The strictness analysis so far was not done & it is not that long to do it, I just want to postpone it until it would be needed, so ! receive a be more final stable place.

It would be good if we would be able to distinguish between WHNFs & not, but going that route may complicate the multithreading, I am talking about that one that Obsidian guys almost provided, I do not know thou precisely, it should be looked into.

Please, lets stick with adi as long as possible, its question should be studied deeply. The work on type system & multithreading & strictness analysis is already enough too much work for now.

[Anton-Latukha]

Ok.

Part of it I already clearly understand.

Indeed:

could type it demand :: m v -> m v' where v' is the type of WHNF values (a NValue' in most cases).

Agree. It seems to be the next logical step.