Btw, I didn't mean that types should be the arbiter of "a | b", just that it should guide the search process. Obviously, you should always be allowed to really choose "c" even if the system determined "b". But our UI could be so much efficient if the system chose "b" most of the time.
EDIT: Classic case, btw: "find ... -print0 | xargs -0 ...". Unless we have pervasive and dependent types, how is any formalism going to know that?
Well, it's been sufficient. That doesn't mean we can't improve on it. My point was simply that assigning types doesn't actually change things - it is still the case that every program needs to be able to interpret whatever is generated by every program you want to pipe into it, or you need some kind of translation.
'Classic case, btw: "find ... -print0 | xargs -0 ...". Unless we have pervasive and dependent types, how is any formalism going to know that?'
Dependent types aren't necessary for that. They might be necessary for `find ... $MIGHTBEPRINT0 | xargs $MIGHTBEDASH0`
Edited to add - or wait, you mean the resulting command built by xargs may have a type dependent on the arguments produced by find? That's... messy, yeah.
Yes! Thinking about interactive CLIs... yes.
EDIT: I should add: My main point here is that types would constrict the search space to be reasonable, rather than seeing that "1200 commands are available, do you want to show them all?" prompt. I really think we could be doing much better in this space.
While I mostly agree with your thesis that types could be great in the shell, I think this particular bit is incorrect in a way that undermines your argument (not, I think, fatally). If a program's output doesn't match up with another program's input, a bit of sed (and maybe some awk) will usually do the trick. And if we added types, that would still be the case - output from one command would have to be the right type to be input to another.