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.
