Dependent Types are a Runtime Maybe

Awhile back I was discussing dependent types with someone and we ended up concluding that dependent types can always be replaced by a runtime Maybe.  This seemed to me then (and still does today) as a fairly surprising and provocative conclusion.  So I thought I'd put the idea out there and see what people think. Let's look at a few examples that are commonly used to illustrate dependent types: Vectors of length N Matrices of size m x n Sorted lists Height-balanced trees (trees where the height of subtrees differ by at most one) The argument is roughly as follows.  All of these examples ultimately boil down to enforcing some kind of constraint on some data types.  The more powerful your dependent type system, the more rich and expressive will be the constraints that you can enforce.  If we take this thought experiment to its logical conclusion, we end up with a dependent type system that allows us to enforce any constraint that can be computed. The important realization here is

Setting Up A Private Nix Cache

I recently went through the process of setting up a private Nix binary cache. It was not obvious to me how to go about it at first, so I thought I would document what I did here. There are a few different ways of going about this that might be appropriate in one situation or another, but I’ll just describe the one I ended up using. I need to serve a cache for proprietary code, so I ended up using a cache served via SSH. Setting up the server For my cache server I’m using an Amazon EC2 instance with NixOS. It’s pretty easy to create these using the public NixOS 18.03 AMI. I ended up using a t2.medium with 1 TB of storage, but the jury is still out on the ideal tradeoff of specs and cost for our purposes. YMMV. The NixOS AMI puts the SSH credentials in the root user, so log in like this: ssh -i /path/to/your/key.pem To get your new NixOS machine working as an SSH binary cache there are two things you need to do: generate a signing key and turn on cache serv


I'm reposting this here because it cannot be overstated.  I've been saying roughly the same thing for awhile now.  It's even the title of this blog!  Drew DeVault sums it up very nicely in his opening sentences: The single most important quality in a piece of software is simplicity. It’s more important than doing the task you set out to achieve. It’s more important than performance. Here's the full post: I would also like to add another idea.  It has been my observation that the attributes of "smarter" and "more junior" tend to be more highly correlated with losing focus on simplicity.  Intuitively this makes sense because smarter people will tend to grasp complicated concepts more easily.  Also, smarter people tend to be enamored by clever complex solutions.  Junior engineers usually don't appreciate how important simplicity is as much as senior engineers--at least I know I didn&#

Fake: Generating Realistic Test Data in Haskell

On a number of occasions over the years I've found myself wanting to generate realistic looking values for Haskell data structures.  Perhaps I'm writing a UI and want to fill it in with example data during development so I can see how the UI behaves with large lists.  In this situation you don't want to generate a bunch of completely random unicode characters.  You want things that look plausible so you can see how it will likely look to the user with realistic word wrapping, etc.  Later, when you build the backend you actually want to populate the database with this data.  Passing around DB dumps to other members of the team so they can test is a pain, so you want this stuff to be auto-generated.  This saves time for your QA people because if you didn't have it, they'd have to manually create it.  Even later you get to performance testing and you find yourself wanting to generate several orders of magnitude more data so you can load test the database, but you still

Efficiently Improving Test Coverage with Algebraic Data Types

Think of a time you've written tests for (de)serialization code of some kind, say for a data structure called Foo .  If you were using the lowest level of sophistication you probably defined a few values by hand, serialized them, deserialized that, and verified that you ended up with the same value you started with.  In Haskell nomenclature we'd say that you manually verified that parse . render == id .  If you were a little more sophisticated, you might have used the QuickCheck library  (or any of the numerous similar packages it inspired in other languages) to verify the  parse . render == id  property for a bunch of randomly generated values.  The first level of sophistication is often referred to as unit testing.  The second frequently goes by the term property testing or sometimes fuzz testing. Both unit testing and property testing have some drawbacks.  With unit testing you have to write fairly tedious boilerplate of listing by hand all the values you want to test with

Armor Your Data Structures Against Backwards-Incompatible Serializations

As almost everyone with significant experience managing production software systems should know, backwards compatibility is incredibly important for any data that is persisted by an application. If you make a change to a data structure that is not backwards compatible with the existing serialized formats, your app will break as soon as it encounters the existing format. Even if you have 100% test coverage, your tests still might not catch this problem. It’s not a problem with your app at any single point in time, but a problem with how your app evolves over time. One might think that wire formats which are only used for communication between components and not persisted in any way would not be susceptible to this problem. But these too can cause issues if a message is generated and a new version of the app is deployed before the the message is consumed. The longer the message remains in a queue, redis cache, etc the higher the chances of this occurring. More subtly, if you deploy a

Talk: Real World Reflex

I recently gave a talk at BayHac about some of the things I've learned in building production Reflex applications. If you're interested, you can find it here: video slides github