I’ve been using Nix and NixOS for many years now,
both personally and professionally, on workstations and servers.
While the tools aren’t without their warts, I strongly believe the
model espoused by Nix for package management is a leap ahead of other
available tools. However, the Nix language can be very unstructured,
and knowing how to use it in an effective and composable way can
involve a lot of searching and deep-diving through nixpkgs. This
series aims to collect patterns and good practices I encounter or
devise, significantly for my own future benefit, but hopefully other
people will find it helpful too.
In programming, we typically think of a variable as a location to
store a value. It turns out this is mostly an implementation detail;
if we generalize them into their interface, we find a rich space of
languages that captures the distinctions between several different
types of programming language that seem very different at first
glance.
If you’ve done much functional programming, you’ve probably heard of
the λ-calculus, invented by Alonzo Church in the 1930s. If you
haven’t, the term might be quite new to you; but don’t worry, despite
the intimidating name the λ-calculus is actually very simple.
Linear types are an application to type theory of the discipline of
linear logic, first described by Jean-Yves Girard
(Girard, 1987).
Since its inception it has led to many fruitful discoveries in
computer science. In this article I hope to explain why it is so
interesting, as well as relate it to concrete tools and practices
available to programmers today.
I often focus too hard on the design of websites to the detriment of
the content, so the design of this site was intended to front the
content. Originally I didn’t even have a title on pages, but I’ve
never been able to pass up the opportunity for a subtitle…
Lorem ipsum dolor sit amet, consectetuer adipiscing elit. Donec hendrerit tempor tellus. Quis donec pretium posuere tellus. Proin quam nisl, tincidunt et, mattis eget, convallis nec, purus. Cum sociis natoque penatibus et magnis dis parturient montes, nascetur ridiculus mus. Nulla posuere. Donec vitae dolor. Nullam tristique diam non turpis. Cras placerat accumsan nulla. Nullam rutrum. Nam vestibulum accumsan nisl.