Fri Jan 20 11:08:27 CET 2017

Make illegal states unrepresentable

What is the analogy for cases where it is not possible to do this, but
it is possible to further constrain the data structure?

The point is that the illegal states don't make it past any kind of
machine interpretation.  So whether this is a simple explicit
constraint (the shape of the data structure), or some constraint that
is expressed ad-hoc, it shouldn't matter.

Maybe this really flies in the face of the original point?

So let's refine:

1. try to express all constraints as structure, as types, or as
proofs.  (whatever your tool set allows).

2. if that doesn't work, express it as properties that are exercises
by an automatic test generator such as quickcheck.