rssoconnor

My discussions with David Cunningham resulting in David producing jsonnet and me creating what is now known as overlays in Nix.

jsonnet has lazy evaluation. This allows you to create mutual references between different parts of your configuration without having to manually topologically sort the evaluation order yourself.

One perk of work-from-home is that I try to structure my day around sunrise like this. I set my alarm for sunrise (usually I only adjust it once a week), with the nice perk that when DST rolls around I don't lose any sleep, I just wake up "later".

I am far enough north that at some point as summer rolls around, I transition to sunset based structure, setting my morning alarm for 9 or 10 hours after sunset.

As another example of this, In [1] I've taken a python program for counting (a bound on) the number of iterations needed of the SafeGCD algorithm to compute a modular inverse for any 256-bit (relatively prime) modulus, translated the python into Coq, and proved the implementation correct. Then by running the computation within Coq we produce a theorem about the bounds (e.g. at most 590 iterations needed for the HD variant of the algorithm).

[1] https://blog.blockstream.com/a-formal-proof-of-safegcd-bound...

My favourite example this is Mark Braverman's demonstration that all Quadratic Julia sets are computable (as in computable real numbers: meaning that you can produce arbitrary fine approximations).

However, as Mark notes, this proof proceeds by deriving 5 alternative programs to do the computation. For any given Julia set parameter 'c' (given as a computable real number) one of the 5 programs will compute the Julia set. Which one? Who knows. It depends discontinuously on the properties of 'c'.

Point is that it seems by the above calculation that a change of increase-by-25% and a change of decrease-by-20% are opposite changes of equivalent magnitude as they perfectly cancel each other out. This is why they are plotted equidistant from 0% on the original chart.

If the number of students enrolled in my course goes up by 25% one year, and then the next year the number of students enrolled in my course drops by 20%, how many students are now in enrolled in my course compared to the beginning?

What if it were reversed: what if the number of students dropped by 20% one year, and then when up by 25% the following year. How many students are now enrolled in my course compared to the beginning in this scenario?

Thanks for all your replies. While I still think it is better to use operators in order to reduce clutter in the code, after all in order for any notation to become ubiquitous it must go through a period of not being ubiquitous, perhaps more can be done to introduce the operators in the documentation. It should be pretty easy to give all the operators names since almost all of them already have a named function implementing them.

FWIW, I asked my physicist friend this question one time. He said while an outside observer would never see a "massless test particle" enter the event horizon due to time dilation effects, real particles have mass and their own gravitational field, and thus due to complicated stuff they can eventually been seen passing through or otherwise somehow merging with the event horizon.

This notion of a plain old lens has been around for a long time. See [0] for an example from 2007, but you can find this construct in functional programming at least back into the early 1990s.

However, it was hardly ever used in practice because it isn't polymorphic and, perhaps more importantly, it can only be used for accessing a single item from a record.

The reason for the explosion of interest in "optical" libraries in the 2010s is because of the development of other optics that can simultaneous access multiple fields (in order), access a functor full of fields (unordered), access field that maybe doesn't exist, pattern match on a variant, zip an indexed set of fields, etc. And all of this is done is both a composable, and transparent way.

Haskell's Traversable functors existed in 2008, and while your lens type can also be traversed, you have to explicitly convert it to a traversable to use it and, or compose it that way.

I'm sorry you feel the need to understand profunctors in order to use optics. Ideally the system would abstract that all way. Unfortunately in Haskell, some of these components leak out (how much varies from implementation to implementation) because this abstraction uses constraints and polymorphism in a very novel way. It's kinda amazing that Haskell's type system accepts it at all.

The alternative seems to involve a proliferation of casting of optics upon every use, requiring either chaining of casts or writing n^2 casting functions from between every related pair of optics.

[0]https://web.archive.org/web/20071023064034/http://luqui.org/...

I agree. I do feel there is a double standard here. C gets away with using `->` and `^=` and `*foo.bar` mixes prefix and infix and postfix with hard to remember precedence rules; C uses `{` and `}` instead of `BEGIN` and `END` and no one bats an eye. But when lens libraries use operators, suddenly some people lose their mind.

I perfer `rec^.field` with operators in lens for the same reason I prefer `ptr^.field` in Pascal over hypothetically writing `ptr DEREFERENCE ACCESS field` or `ACCESS(DEREFERENCE(ptr),field). It lets me hide what is essentially just plumbing-like-grammer behind operators in order to let me focus of the parts of the program related to the business logic at hand, namely `rec`, `ptr` and `field`. Otherwise the plumbing tends to drown out the more important parts of what is going on.

Not that you would necessarily use the same words in Haskell, but I'm curious how you would read `user1^.name` in Pascal, or `user1->name` in C or `(*user1).name` in C?

(Edit: I'd also be curious about `x += y` and `x << y` in C.)

While maybe not impossible, it is quite hard to cox Nix to "install" multiple different versions of the packages. They all cannot be in your path at the same time.

I still encourage you to give it a try. You can build different versions of same package and not "install" them. Instead just execute the binary from the built version (I do this where I have a built-but-not-installed version of openssh-8.6 laying around because I have an old service that modern SSH no longer supports).

You can also run `nix-shell -p <custom-package-version>` to get a shell with a specific package available in the path, overtop of whatever might be globally installed.

Who knows, you might even be tempted to dip your toes into the Nix language by writing a custom `shell.nix` to build a shell with some more complex development environment, or to simply automate a complex `nix-shell -p` command.

My method was to spend 25 years listening to colleagues mumble about Category Theory and slowly picking up the basics. Even I didn't really use Category Theory in my abstraction work. It's just that after months of effort to crack my problem, I showed my pages of work to the Category Theory folks and they were like "oh, it's simply Yoneda this and Yoneda that and your proof can be done in 4 lines.".

That said, if I had to guess at what would be effective at getting up to speed without spending 25 years, would be to checkout https://github.com/hmemcpy/milewski-ctfp-pdf Category Theory for Programmers. Milewski was one of those people who were like "Oh, it's simply Yoneda this and Yoneda that", and he figured it out all himself in parallel without seeing my proof.

But I doubt it will be like, knowing Category Theory will enable you to have super powers for abstraction design. Rather it will be a matter of having enough mathematical tools at your disposal plus the right inspiration at the right time to realize that ones of those tools can happen to solve your abstraction programming problem you happen to be facing at some moment, in a way that is not obvious, if you are lucky. In fact, you likely have to first guess at what the right abstraction is and then fall back on Category Theory to verify the sanity of your guess.

I think your understanding is a little off the mark, at least with respect to my not-so-well written comment, which was just meant as a rambling story about how category theory influenced my and others development of (functional) programming "optics" over the last decade.

The new "optics" people are have designed in reference 4 are not themselves "elements of category theory", but category theory provides the theoretical framework that these composable optics live in. Once that framework is identified, it becomes much easier to say "oh, this new optic definition I've just identified, fits into this framework, and so does this other optic, and so forth"

To make a loose analogy, one could imagine identifying triangles and cubes and such and such that have these rotational and reflective symmetries, and notice how you can compose those operations, and then see how performing specific shuffles of cards is also composable and has some properties similar to rotating cubes in that repeated operations have a certain period and other such things. Then when someone introduces you to group theory and says yes both the cube rotations and the card shuffling can all be seen as a group and group theory can be used to generically answer your questions about these otherwise seemingly very different operations. And then you start seeing that lots of things are groups, like that Rubik cube puzzle you have, or lines through an elliptic curve. Coming up with new optics is analogous to noticing various things are groups, a task that is much easier when you have group theory and know how to recognize a group when you see it.

That said, I think a better answer to your question may be in one of my later replies https://news.ycombinator.com/item?id=33806744: Category Theory has been useful for devising an entirely new (functional) programming abstraction, the theory of "optics" in my case. But for day-to-day programming you don't normally need to invent entirely new programming abstractions, you can just use the ones that have already been developed by the computer scientists.

> Or, more negatively, nobody else willingly put themselves in a straight-jacket so tight that they had to use monads to be able to do many real-world things, like I/O or state.

I want to emphasize how true this is. In the Haskell 1.2 report, before Haskell Monads existed, the type of `main` was more or less:

    type Dialogue = [Response] -> [Request]
    main :: Dialogue

The main function was took a lazy list of, let's call it OS responses, and issued a lazy list of requests to the OS, whose response you would find at some point on the input list. Your task was to keep your lazy generation of `Request`s in sync with yourself as you consumed their `Response`s in turn. Read ahead one to many `Response`s and your `main` would dead-lock. Forget to consume a `Response` and you would start reading the wrong `Response` to your request.

The suggestion was to use continuation passing style (something that later we see conforms to the Continuation monad interface) to keep things in check, but this was not enforced, and by all accounts was a nightmare.

So yes, Haskell's laziness straight-jacket (Haskell was basically invented to study the use of lazy programming without having to purchase Miranda) basically means they had to invent the use of Monads for programming, or at the very least invent the IO monad.

I agree with you. CT seems mostly useful as a way of devising entirely new abstractions, but once those abstractions are developed, you don't need CT to use them.

For example if it were 2008 and you want to be inventor Applicative functors for use in Haskell, then knowing lax monoidal functors from CT might be helpful. But if you want to just use Applicative functors, you don't need to learn lax monoidal functors first.

So programmers probably don't need to learn CT because they can just let the computer scientists devise their abstractions for them. But if you want to be a computer scientist and one day devise your own abstractions[0], then maybe CT would be helpful.

[0]https://news.ycombinator.com/item?id=33805923

Apologies for the jargon, but there isn't room in a comment box for a detailed explanation.

"The Essence of the Iterator Pattern"[0] posed an open problem in type theory as to whether or not "lawful traversals", of type `∀ F:Applicative. (X -> F X) -> (B -> F B)` could appear for anything other than what is called a "finitary container"[1], B := ∃S. X^(P S) where the (P S) is a natural number (or equivalently a polynomial functor B := ∃n. C_n * X^n). Or rather, there was an open question as to what laws are needed so that "lawful traversals" would imply that B is a finitary container.

Eventually I came up with a fairly long proof[2] that the original laws proposed in "The Essence of the Iterator Pattern" were in fact adequate to ensure that B is a finitary container. Mauro Jaskelioff[3] rewrote my proof in the language of category theory to be few lines long: use Yoneda lemma twice and a few other manipulations.

Anyhow, the upshot of reframing this as a simple argument in Category Theory meant that, with the help of James Deikun, I was able go generalize the argument to other types of containers. In particular we were able to device a new kind of "optic"[6] for "Naperian containers" (also known as a representable functors) which are of the form B:=P->X (aka containers with a fixed shape).

Since then people have been able to come up with a whole host of classes of containers, optics for those classes, representations for those optics, and a complete characterization of operations available for those classes of containers, and how to make different container classes transparently composable with each other[4].

For example, we know that finitary containers are characterized by their traversal function (i.e the essence of the iterator pattern). Naperian containers are characterized by their zip function. Unary containers are characterized by a pair of getter and setter functions, something implicitly understood by many programmers. And so on.

I don't know if all this means that people should learn category theory. In fact, I really only know the basics, and I can almost but not quite follow "Doubles for Monoidal Categories"[5]. But now-a-days I have an "optical" view of the containers in, and forming, my data structures, slotting them into various named classes of containers and then knowing exactly what operations are available and how to compose them.

[0]https://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator...

[1]https://en.wikipedia.org/wiki/Container_(type_theory)

[2]https://github.com/coq-contribs/traversable-fincontainer

[3]https://arxiv.org/abs/1402.1699

[4]https://arxiv.org/abs/2001.07488

[5]https://golem.ph.utexas.edu/category/2019/11/doubles_for_mon...

[6]https://r6research.livejournal.com/28050.html

People in this thread tend to be supportive of the idea that he is simply playing by the rules. While I have no reason to doubt the legality of this strategy, I question whether it ought to be legally appropriate for Peter Thiel to decide the valuation of his own investment (more or less) by himself. His initial deposit into his Roth IRA doesn't strike me as an arm's length independent valuation. It was simply the par-value of the stock, which AFAIU is a valuation for accounting purposes and not at all an independent appraisal of the stock's value.

That said, when this topic came up last year on Hacker News, it did make me rethink my own personal tax-sheltered strategy. (I'm in Canada, so I'm thinking about TFSA instead of Roth IRA). Before I had been following the advice to shelter my high-tax items, which for Canada would be bonds. But after reading about this, I've rearranged things to instead shelter (hopefully) high growth items (e.g. VTI). The idea being that by growing room in my sheltered accounts I can eventually save more on taxes than I would by sheltering bonds

I'd be interested in other people's comments on tax-sheltered-account strategies for tech workers.

I recently learned that my local police have designated areas in their station's parking lots for these sorts of exchanges:

<https://www.wrps.on.ca/en/staying-safe/buy-and-sell-exchange...>

I recently took a 4 year old space heater (in the form factor of a small wood burning stove with a fireplace effect) to be repaired. I guessed that the thermal fuse had blown and the blower was dirty.

It cost $45 (CAD) to have it opened and another $95 to complete the repairs, which is very close to the cost I paid for the device in the first place. Not that I'm complaining. The guy said he completely disassembled and cleaned the blower motor in addition to replacing the fuse. I wouldn't be surprised if it lasts even longer now. Plus I do like the way it looks and fits in my office.

My point is that I understand why there are few repair shops. When North American labour costs for repairs end up being the same price as buying a replacement off the shelf, no wonder people throw away working and nearly working devices.

Perhaps I could have repaired it myself. I don't know. I'm pretty nervous about the idea of fiddling with 120 volt devices with zero training.

Thanks, "Does not provide bus power" and upto 50 m (edit upto 100m). Sounds fantastic. Do you think you'd make wall ports out of them?

When searching for active cables, all I saw were 2m and providing 100 watts of power.

> as far as general cleanliness, one of these years I'm gonna cut a hole in my wall and drop some cables to the basement with TB3 or DP 1.4 active fiber cables (not electrical cable so fire code ignores it)

Is it possible to purchase active fibre cables that are unpowered? I understood that these cable includes a pair of copper wires for power (the fire hazard) in addition to the optical link for data. And that the active components of these cables use (and hence require) that transported power.

How do you feel about the 32" size? I understand there is a 27" version with identical features.

The Lenovo ThinkVision P27u-20 27-inch Monitor is Thunderbolt 4 and cheaper, but also smaller and the ethernet port is still only 1Gb/s.

Good observation. PC Magazine says the ethernet port of this Dell monitor I'm considering is 1000Mb/s. I can probably live with that, though I'd certainly prefer a monitor-hub with a 10 Gb port if I can find one (that still has DP and HDMI inputs).

For a person satisfied with a single monitor, I figure it makes sense to get a monitor that is itself a dock.

At the moment I'm considering the Dell UltraSharp 32 4K USB-C Hub Monitor - U3223QE. I know it is only a USB-C hub, but I'd like to be able to plug my older laptops into it on occasion, so I need something with a least an HDMI input and preferably also a DisplayPort input.

I don't know anything about monitor-hubs so if people have comments or recommendations, please let me know.

There is nothing special about how Nix evaluate system configurations that is any different from how Nix evaluates any other expression.

Being able to write

     let usercfg = { username = "nix-user";
                     homedir = "/home/" + usercfg.username;
                   };
     in usercfg

is nearly a hallmark of non-strict semantics, which is achieved by lazy evaluation.

Strict languages can simulate these non-strict semantics by using functions of no parameters to delay evaluation, but you lose the efficiency that comes from the memoization of record fields that you get with lazy evaluation.

P.S. The above would perhaps be more likely be written as

    rec { username = "nix-user"; homedir = "/home/" + username; }

but when specifying larger configurations composed of multiple nested records with wide cross-cutting inter-dependencies, "rec" doesn't really cut it as "rec" works best with extremely local inter-dependencies.

I actually agree with you about inheritance and OOP. It's funny because when I finally understood how to override packages with this late-binding technique, I said to myself "Finally I've found a use for inheritance!".

I certainly think people should exercise caution as this could probably be abused quite badly. Maybe people will come up with better designs in the future. However I will say, that the method it has replaced was much worse. The old way was adhoc and almost always failed to achieve ones desires in all but the simplest cases.

Don't just take my word for it. Peter Simons also agrees: <https://github.com/NixOS/nixpkgs/commit/3c8b33eee442fd573d47...>

> To seriously answer the question: is the Nix language required for the Nix packaging system to exist? Laziness is required, to some degree, but can the next iteration provide an on-ramp which doesn't involve learning a new lang and paradigm? Guix folks sure think so.

I'd love to hear from someone deeply familiar with Nix and Guix about laziness.

I'm deeply familiar with Nix and I've concluded that lazy semantics is absolutely critical for a configuration language. It lets me refer to other attributes of my configuration from anywhere. For example, I can refer to port number from my whatever service in my firewall. Nix's system of overlays depends on laziness too to provide efficient late-binding familiar from OOP.

I don't need to topologically sort the evaluation of the various inter-dependencies of my configuration. So long as there exists an evaluation order, laziness finds it.

Laziness is compelling enough that I managed to convince the author of Jsonnet <https://jsonnet.org/> of it when he was designing it, and in turn he helped me design what is now known as overlays in Nix.

I don't even understand how Guix manages to work without laziness, though clearly it does somehow. I'm curious as to how that is possible, though I fear I will only ever truly understand by diving into Guix.