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.
