Thanks Artyom for your detailed reply. It's illuminating. I think I should say more about my motivation. In my day-to-day work, we often need to set up server hosts, and we use ansible to do that. There are other tools like Chef, SaltStack, etc., that are all similar. With these tools, instead of using shell commands, we can use commands that are higher-level, more declarative, and idempotent, such as "path /a/b/c should exist", "file xyz should have this content", "package foo should be installed", etc. While definitely an improvement over shell scripting, they still leave a lot to be desired. Specifically, I'd like to be able to - reason about the state of the system after a sequence of commands are run, and - state formally what a sequence of commands should accomplish.
Using the same example as earlier, if I have these commands: - create file a/b/c - recursively delete a It should be possible to infer, statically, that a/b/c doesn't exist after these commands are run. Therefore, if my specification says "a/b/c should exist", then this sequence of commands should be rejected. Back to your solution, I think it will work well if all the filesystem nodes are created within our code. But there is a problem when we establish the existence of a node by asking the filesystem. Imagine: - Check if a/b/c exists. If not, abort # this gives us a "lease" to a, b, c - Do something with a/b/c - Recursively delete a # destroys handle to a. b and c are now unreachable So this seems to work. But what if we check a/b/c twice? We would then have two "leases", and we would still have a path to a/b/c after a is recursively deleted. Seems we would somehow need to prevent duplicate leases from being issued. Is it possible to solve this problem at the type level? On Sat, Jun 1, 2019 at 5:43 AM Artyom Shalkhakov < artyom.shalkha...@gmail.com> wrote: > Hi Shimin and welcome! > > For me ATS is a place where I can bring some dry linear logic calisthenics > to life with programming. So let's get started. > > On Saturday, June 1, 2019 at 2:33:37 AM UTC+3, 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? >> > > I think it would make sense to somehow "leave" b and c to "be", i.e. > discard the handles to them but leave them as-is in the filesystem. That > could be a no-op function, even, but of course, for total correctness you > don't want any other process to have links to b or c... So as you can see, > it gets a bit problematic. However, putting this scenario aside, you could > have a function to "free" the handles, then use it to dispose of the > handles, and then finally remove a. I once wrote a variadic macro that > helped me to clear out such linear-typed variables in one line. > > Here are a few rambling thoughts about your problem. Please take with a > grain of salt. It's really complicated to do this as I describe below (with > the indexes), but might give some ideas. > > We could represent the filesystem as labelled tree (every label is the > file or directory name). Directories may contain subdirectories and files > (files cannot be nested). So it can be seen as a graph, where > files/directories are two sorts of nodes, and containment relation between > any two nodes are the edges. Then a path is just a sequence of steps > through the tree nodes, same as in graph theory. For example, a is a node > of sort "directory", b is a node of sort "directory", b is contained in a, > c is a node of sort "file", c is contained in b, and also, the file path > a/b/c is a sequence of steps, starting at a, following through the > "contained in" relationship between nodes, and ending at "c". > > Since it makes sense to think of these nodes as resources, then we > represent these with linear types. Then we are left with the containment > relation. > > Imagine we have an abstract linear type fsnode(bool) where fsnode(true) is > assigned to files and fsnode(false) is assigned to directories. We could > also introduce some casts if we wanted to (e.g. introduce a type "file" > that is convertible to fsnode(true) and vice versa, and a type "directory" > that is convertible to fsnode(false) and vice versa). > > One way to deal with it is to index every node with an integer denoting > the count of subdirectories/files that it contains. Then you'd have an > fsnode(bool,int), where the second index is the count of > subdirectories/files that are contained in the directory (for files it > would be always 0, of course). This kind of solution is not very practical, > though. So another approach could be to track in the indexes two more bits > of information about the node: > > 1. the identity of a node (as something opaque, e.g. an addr index) > 2. the identity of a node's parent > > Then for a root directory node you'd have a type like fsnode(false, p, > null) where p is some non-null address, And for a subdirectory that's under > the root directory you'd have have a type like fsnode(false, p1, p), that > is, it's contained in p, and p1 is not the same as p (this would be usually > discharged by the typechecker, we don't really care about it). > > So in your case, it would go like this, in code: > > val r = fs_root () // : fsnode(false, r, null) > val a = mkdir (r, "a") // : fsnode(false, a, r) > val b = mkdir (a, "b") // : fsnode(false, b, a) > val c = mkdir (b, "c") // : fsnode(false, c, b) > val () = free (c) // [c] is no more in our code > val () = free (b) // [b] is no more in our code > val () = rm (a, true(*recursive*)) // [a] is removed, recursively > val () = free (r) // we don't need [r] anymore > > The "free" and "fs_root" are more like "leasing" the resources from OS > (i.e. asking for them to use temporarily, but then eventually we are > obliged to give them back to their justful owner). > > Since these functions that we give to the user are the only way to > legitimate work with the abstract types, they will have to comply with the > protocol that we impose on them, or their program will fail to compile. > > A similar approach is taken below (please see the provided tests, too, > since they are actual programs you can run): > > https://github.com/ashalkhakov/typesafe-dom/blob/master/src/SATS/dom.sats > > It depends on what you want to accomplish. This approach is very > fine-grained and may be too difficult to work with. > > -- > 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/5f9a7255-20ef-4aad-9002-2e37680e6e8e%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/5f9a7255-20ef-4aad-9002-2e37680e6e8e%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%2B7DBVUYcxZoY%2B_%2BAZaz-oUC3RwJ-W0bDYTcLEYHDwmRVqA%40mail.gmail.com.
