Having thought some more about this, I think that it can be proved that it is not possible to deal with seekability entirely by compile time type checking.
In Linux / Unix there are things called "named sockets" that exist in the file system and can be opened in the same way as other objects in the file system. The catch is that they are no seekable. And there are "device files" that have the same property; e.g. "/dev/tty" or "/dev/null".
An IO library needs to be able to create an input or output stream for an object using a filename or pathname supplied as a string; i.e. a runtime value. (If you can't do that, the language has "limited utility".)
The "open" method therefore needs to be able to cope with the cases that it could be asked to open a seekable object or a non-seekable object ... and that it won't know which is the case until it has tried it.
This means that even if you were to design a set of APIs that distinguished between seekable and non-seekable streams, there would still need to be a runtime test to determine if a specific file could be opened as a seekable (or non-seekable) stream.
In short, it is not possible deal with this entirely via static typing.
Mat Fennwick commented thus:
Perhaps I'm missing something, but it seems to me that your example could be handled with an algebraic sum type, à la Haskell. Is that not the case?
Yes, I think that you could express different flavours of stream using algebraic sum types. But I don't see how this is going to give you a compilation error if you:
- open a stream based on a pathname, then
- try to do a seek on a non-seekable stream.
You'd end up having to do a
switch to discriminate the seekable and non-seekable cases, and deal with the possibility that you've got the wrong kind of stream.
Now you could design the APIs to minimize the runtime checking. But my feeling is that that comes at a cost. And the cost is that the classes that use the APIs get more complicated. For instance, whenever you pass a stream object you have to think whether you need to declare the method to require a seekable or non-seekable stream parameter. (And you can't just say "either" all of the time and use a common supertype ... because then you need a typecast at the point where the stream needs to be seekable and your compiler can no longer detect the real problem.)
The other problem with mapping (effectively) runtime properties to compile time types / interfaces is that it gets messy when you've got multiple; e.g. imagine if you had types / interfaces for seekability, readability, writability, deletability and so on. You end up with a combinatorial explosion of the leaf classes.
Finally, if this was a good idea, you would have thought that some would have tried it, shown it to be a good idea, and convinced someone to add it to a mainstream programming language. AFAIK, the last step hasn't happened. OK, that is not proof that it won't work ... but the absence is pretty convincing.