for a long time now i've thought that if you were going to have a typed shell language, you'd need it to be some kind of interesting, dependently typed thing, possibly with linear types
0 Boosts
0 Likes
if foo/ doesn't exist, then `mv a foo/` should be an error. meanwhile `mkdir foo` brings foo/ into existence
type checking this must be able to see that foo/ now exists after `mkdir foo` for `mv a foo/` to be valid only after the mkdir
(why i picked a and not bar, i don'tknow lol)
so the validity after the mkdir is some kind of dependency but it's not a normal scopal dependency because `foo/` could be deleted and should then go out of scope:
rmdir foo
mv a foo
should be an error
im not sure if anyone's ever tried to actually make an informative type system for doing typed shell languages. it has interesting connections to old fashioned symbolic AI tho
@beka_valentine I imagine the first thing you'd find out is that the execution model/environment is too cursed and to get anywhere you'd want to ... change ... that problem first
my reasons ultimately come down to the fact that shell languages can both change the world, and also make sense only in the context of those changes
a good example of this is a simple sequence of actions:
mkdir foo
mv a foo/