Recorded myself singing one of my favorite modern Hebrew songs:
In my professional life as well as in various volunteer contexts, I've noticed (at least) two kinds of roles people can fall into. Understanding their dynamics can help both someone trying to recruit or manage others in a project and someone deciding whether to jump in or understanding their own role.
Last weekend, annoyed yet again at a lack of proper quotient types, I decided to dig into cubical type theory. A weekend's reading and pondering does not an expert make, but I wanted to highlight some surprising structural ways in which these theories differ from previous type theories, which none of my sources noted.
Note: This post assumes some familiarity with and interest in Nix. In particular, a basic understanding of the distinction and relationship between the Nix language and the Nix store is required.
In the Nix expression language, all strings have some metadata associated with them called "context". At a high level, this context is used to track dependencies in our build scripts to ensure we have all of the packages we need available during our builds. In this post, we'll go into more detail about why this context is necessary, how to interpret it, and the technical details of how this feature interacts with other aspects of the language.