‘Existential Type’, in the article ‘Boolean Blindness’ (see also part 1.1 of Dan Licata's 15-150 lecture 9), is right, but the explanation seems somehow askew, so here is a different take.
A boolean is said to have no ‘meaning’: “There is no information carried by a Boolean beyond its value” (original emphasis). But there is something odd/wrong with that: because it is true of all data: all data lacks meaning; the other bits in non-boolean data are not ‘meaning’/‘information’, they are just other values. It is also said that: “to make use of a Boolean you have to know its provenance so that you can know what it means” – but again that is true of all data. Where is the meaning of data? The meaning of any piece of data seems more like in its type – in the abstraction it is an instance of. And that is the thread that unravels the puzzle.
The overall point is this: when you have some data and you want to break it into parts to handle separately, you ought to have types to put those parts into. And breaking data up to handle in parts is really the essence of what software is all about – and so that is why types are so pervasively important.
(Rather than ‘boolean-blindness’, a better name might be ‘part-blindness’.)
———
Consider an everyday case: the nullable pointer. There is nothing wrong with a nullable pointer in itself. It has all it needs to be handled entirely and properly. The problem comes when you want to break it up to handle in parts.
A nullable pointer has two ‘parts’: null, and all-other-values. These can be got at with a simple if-else conditional: if p is not null then ... else ... end. And there is still nothing wrong with that. The problem arrives when you want to handle the parts – and you lack a good type system. What do you do with the non-null pointer value? You just have to put it back into a pointer again – a nullable-pointer: which is what you started with. So where has what you did with the test been captured? Nowhere. When you handle that intended part elsewhere you have to do the test again and again.
(The point is the same for other destructurable data. You might parse a string into various parts and so cases. There is nothing particularly boolean here.)
Those ‘parts’ are the separate ‘meanings’ we want to break the data into. And types express those tests in the ‘meaning’ of the intended type (and a type system mechanically implements that). Types create (are) an abstraction, and gain the leverage of that – they allow one piece of work to be used multiple times. When you break data up, types factor-out that break into one place, and allow it to be used in multiple places. Without types you cannot ever break data up into parts cleanly and reliably. You make no reusable note of what you did.
(The other part, null, is a special type: unit – it has only one value. But there is nothing too special about that here, it is just minimal. It still has a meaning and it is still perfectly possible to handle. When you handle it there is only one thing to do, and, most particularly, there is no more to break down: it is a leaf of the processing tree.)
Type systems and type checking are about being consistent: treating the same things the same and different things differently. Which is exactly the responsibility facing you after you have broken things up into parts. Dynamic typing still captures ‘meaning’ but is not checked up-front like static typing. Though it is possible to make a further distinction and clarification here: what is captured it not really the ‘meaning’, but only the difference of meaning. The ‘meaning’ is (more like) in the code that handles the types; the types, at their core, just say that things are different, not how.
———
Types are the shadows of larger conditionals.
———
Related: