←back to thread

Type checking is a symptom, not a solution

(programmingsimplicity.substack.com)
67 points mpweiher | 1 comments | | HN request time: 0.203s | source
Show context
Twey ◴[] No.45142218[source]
As other people here have said, type systems are merely an automated check that interfaces are used correctly. But to read this more generously, the author is saying that with sufficiently simple interfaces such checking isn't necessary. That's arguably true, though rather limiting (since a direct composition of simple interfaces is not necessarily a simple interface): a system that presents a single call that reads one byte and adds one to it, with wrapping, doesn't need a type because all inputs are valid.

Unfortunately, the examples given are not particularly representative, because they all imply complex interfaces (reading? writing? buffering?) and complex input/output formats: the shell that is doing the piping only cares about ‘bytes’, but the programs themselves have much more complex requirements on the data, which tends to be what happens once you start assigning semantics to your interfaces.

Even with spatial locality limiting the number of inputs and outputs, the ‘interfaces’ that hardware uses are usually specified in multi-hundred-page manuals, and that's mostly due to having to encode the semantics of what it means to put volts on those wires.

replies(1): >>45143315 #
ratmice ◴[] No.45143315[source]
Another thing about bytestream oriented interfaces like pipes is they tend to turn every program into a parser in order to reject invalid input. Eventually someone is just going to put a type system on top of that parser to reject more than just syntactically valid programs, but also semantically invalid ones.

As such this notion that "we don't need types, we can have parsers." kind of argument doesn't feel very inspiring.

replies(1): >>45144927 #
1. Twey ◴[] No.45144927[source]
As a reductio ad absurdum, statically typed programs are also (represented as) streams of bytes!