haskell-nix / hnix

A Haskell re-implementation of the Nix expression language
https://hackage.haskell.org/package/hnix
BSD 3-Clause "New" or "Revised" License
763 stars 115 forks source link

Add a “why” section #381

Open asymmetric opened 5 years ago

asymmetric commented 5 years ago

I’m sure there are very good reasons to re-implement the nix language, but they’re not stated in the README and therefore not discoverable by newcomers :)

jwiegley commented 5 years ago

To make it easier for Haskell authors to create new tooling for the Nix ecosystem, including but not limited to: debuggers, custom evaluators, syntax checkers, linters, formatters, code generators, etc.

davidak commented 5 years ago

@jwiegley could you add it to the README?

How do i benefit from this as a NixOS user or contributor?

Why in Haskell and not Rust or Go?

Tell something about the background. How has this project started?

Anton-Latukha commented 3 years ago

Well, it would be strange to right upfront bluntly advertise the project while official Nix agenda is ongoing.

The cornerstone is simple:

  1. Nix language is a purely functional lazy language. Haskell is a purely functional lazy language.

Because of that - it means that Nix language implementation in Haskell is straight-forward and can be very performant. Since the Haskell <-> Nix type casts are the most direct.

Nix is a DSL for system configuration. Haskell is a general purpose programming language that is very strong in DSL and language creation. The honest "haskeller" IT ecosystems evaluation is at State of the Haskell ecosystem. Strong, as a 1-st place in IT space strong, points of Haskell are:

In the "Domain-specific languages (DSLs)" Haskell is second. Well, it is known why. Because Lisp. Lisp is known as "the" DSL building language. And to be fair the Haskell System F is typed Lisp. It is possible to write in Haskell in the Lisp style, just Haskell has much richer and stricter syntax and much more inbuild machinery, programming possibilities and features.

But despite Lisp being 1-st place, the Haskell DSL languages: Agda, PureScript, Elm, DHall, DAML and so on and so on, are the ones that are gaining a lot of traction and being highly successful.

  1. Haskell is a great DSL engine. Since they have same paradigms - it is easy to make Haskell DSL that is a Nix language.

During the DSL creation the parent language the DSL is built from is known to influence the DSL syntax. Not just due to creator's bias influence, but also because of the underlying language syntax & design. It is often easier to pass-through the syntax into DSL.

For example - Lisp DLSes tend to be bracket-heavy, C/C++ DLSes also tend to inherit parent properties.

But Nix and Haskell syntaxes are frequently pretty identical, so if one would wrote Nix-like DSL in Haskell - it could-been having Nix-like syntax. With several caveats - probably without ; and with syntax alignment. And without the obvious FP implementation errors, like implementing folding by foldl builtin which famously does not terminate in infinite structures or in the infinite recursion that Nix gives away, or without search for occurrences of the "" in the string to replace them in replaceStrings primop and so on. It is easy to posteriorly critique work of course, but mistakes need to be owned to keep the owns honor, not hidden and made seem as they do not exist, reality is reality and they very do exist, in the code and use, just not in the official docs, such important things at least need to be documented in the official docs.

Because they are not in the official docs, HNix can not link to their explanation upstream, so those Nix language caveats gets documented inside as a specific code and as documentation on it.

Upstreaming them is not an option to suggest to us. In the first place, Nix upstream is very much, more than aware of them, and seems like actively voted to actively remove documentation of those important implementation bugs from the upstream docs.

  1. On top of it - Nix language is highly recursive language, many of the core types of the language are recursive (for example: recursive attrsets, functions, and expressions overall). That means it is strongly recursive in nature.

HNix harnessed that nature fully through the recursive schemes, which are a current cutting edge minimalistic direct scientific system to easily manage the recursive structures of any complexity and efficiently doing operations on them of any transformations.

F-algebras (used in recursive-schemes) effectively allows recursions to be made and managed as flat structures, or managed on layer basis. The recursion is not managed as recursion, but as standard F-algebra operations as fold, unfolds and such. And that approach also allows the recursive language to be represented non-recursively to the GHC, and the recursive code is difficult to optimize, while non-recursive result allows GHC to efficiently compile the non-recursive code we give, which is a representation of recursive code. For example, because the recursive nature of Nix and its recursive structures get represented as non-recursive - there is "no" recursivity in the GHC code result. And the difference is for example: currently, during refactoring, I see no overhead by introducing more polymorphism into the code. Often polymorphism can introduce overhead if for example the type class inference repeatedly happens in a recursive loop - but not in our case.

  1. The "Why" goes further, since Haskell has a very strong type system - that is very contrary to Nix interpreter dynamic typechecking. For example during treewide refactoring in Nixpkgs currently maintainer can not check that the replacement is sound in all places. So the treewide refactors "just make done" (oversimplifying here), and there is no way to check that refactor works in all Nixpkgs subdomains, and so refactor merges, Hydra and users catch the bugs, that often gets represented in the Hydra by delta falls, and it sometimes happens that treewide refactors get reverted compelettely, they happen by sheer trial&error on a massive scale in alive, central and relied upon codebase, because there is no way to properly type check the diff.

That is wild-westy and fun to do of course. But if at least 1 of the enterprise giants arrives into Nixpkgs - there probably would be no more of such treewide refactors - it is blind shooting and enterprises do not like those. Thorough type checking not only would allow doing refactors on a massive scale, the development experience becomes much more pleasent.

  1. Nix language strongly borrows, influenced by and builds from Haskell code development principles, syntax & development. For example, not only HNix uses recursion-schemes, Nixpkgs provides in the base the lib/fixed-points, which gets used pretty often by other libraries in Nixpkgs, any kinds of derivation extension/expansion, aka overlays, often rely on lib/fixed-points, which is just recursive schemes use really. Since there are such functions as makeExtensible, converge, extends, composeExtensions, I'd said that current Nixpkgs is not possible to do without it. What to do in highly recursive language with recursive attrsets that uses recursive structures upon recursive structures? Only fixed-point (attractor) math convergence math to make it all be written and work nicely. And on the outside people not even know it gets used, one just extends something and it works.

So, since Nix has such strong influence form Haskell, the more person knows Haskell, the more intuitive Nix becomes. So HNix brings the Nix closer to Haskell developers, since languages are pretty close.

  1. Since the proper recursion-schemes design and use and Haskell & Nix sharing paradigms - the implementation is the most direct. I mean the direct functor from Hask subcategory to Nix category - type of direct.

HNix essentially build a functor from Hask to Nix, and raising the functor is the most simple, direct, effective and transformation, which makes it elegant.

One effectively needs just to look into Value.hs to see it.

Not just Hask -> Nix functor, there is a Nix -> Hask functor which is:

-- | Module pattens use @language PatternSynonyms@: unidirectional synonyms (@<-@),
-- and @ViewPatterns@: (@->@) at the same time.
-- @ViewPatterns Control.Comonad.extract@ extracts
-- from the @NValue (Free (NValueF a))@
-- the @NValueF a@. Which is @NValueF p m r@. Since it extracted from the
-- @NValue@, which is formed by \( (F a -> a) F a \) in the first place.
-- So @NValueF p m r@ which is extracted here, internally holds the next NValue.
pattern NVConstant' x <- NValue (extract -> NVConstantF x)
pattern NVStr' ns <- NValue (extract -> NVStrF ns)
pattern NVPath' x <- NValue (extract -> NVPathF x)
pattern NVList' l <- NValue (extract -> NVListF l)
pattern NVSet' s x <- NValue (extract -> NVSetF s x)
pattern NVClosure' x f <- NValue (extract -> NVClosureF x f)
pattern NVBuiltin' name f <- NValue (extract -> NVBuiltinF name f)

This functor gets the real Nix values and extracts them into Hask-Haskell internal representation. Isn't that seems elegant?

Anton-Latukha commented 3 years ago

And would mention that because of this implementation and strong type system - the complex Nix code would be much easier to debug, HNix is & would be able to generate great and understandable code debug reports.

Anton-Latukha commented 3 years ago

rnix also seems to be the great agenda.

I am happy that it exists. The more the better Nix there, the better.

rnix does not take away from the HNix cornerstone.

The implementation elegance is strong in HNix, and is very needed to Haskellers, and very interesting for them. HNix is used already, so anyway the support and the work must be done.

As far as I know, HNix gets used in the IOHK to support Haskell.Nix infrastructure.

Really, in HNix there is only a couple of things left to do to finish for the fully working release. After that working release there would be covering of more Nix specifics.

This year for me is as a refactor & stabilization year before the working release. The main work is essentially done, so it is a great time to clean-up after the work and take this as a great moment to organize everything before saving that is works and the community grows began.