Thanks for your reply and kind words. I think I got it. Basically to prove the existence of dir1/dir2 we must first prove the existence of dir1, and `rm -r dir1` will destroy that proof.
I've long been thinking about how to improve something like ansible, and recently had this idea, and thought it might actually work. I have no clue how to actually implement it though. I hope someone much smarter than I can make it happen :) On Fri, May 31, 2019 at 7:03 PM Richard <qpot...@gmail.com> wrote: > Apologies, forgot to say hello, > > Hi Shimin, this is a great question. I like your thinking! > > On Friday, May 31, 2019 at 7:33:37 PM UTC-4, Shimin Guo wrote: >> >> I'm thinking of using linear types for system administration. >> Specifically, I want to add type annotations to commands like mkdir, rm, >> etc., so I can reason about the state of the system after they are executed. >> >> For example, mkdir will have the type >> >> p: path -> isdir(p) >> >> where isdir(x) is a linear prop. rmdir will consume that prop. >> >> What I'm currently stuck on is the following scenario: >> >> touch a/b/c >> rm -r a >> >> After the touch, there should be a linear prop exists(a/b/c), and after >> the rm, the linear prop needs to be consumed. My question is, what should >> the type signature for "rm -r <dir>" be? It seems it needs to consume all >> the linear props in the "environment" in the form of exists(p) where p is >> under <dir>. Is there a way to represent such a signature in a language >> like ATS? >> > -- > You received this message because you are subscribed to the Google Groups > "ats-lang-users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to ats-lang-users+unsubscr...@googlegroups.com. > To post to this group, send email to ats-lang-users@googlegroups.com. > Visit this group at https://groups.google.com/group/ats-lang-users. > To view this discussion on the web visit > https://groups.google.com/d/msgid/ats-lang-users/2157ce50-566b-4a17-8b4c-873a43ec1d2d%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/2157ce50-566b-4a17-8b4c-873a43ec1d2d%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAA6Z%2B7DQKXheevWMKVowFuRKivU7HAXoK-do%2BzEHVTmg_nY3MQ%40mail.gmail.com.
