Consume all linear props of a given form in the environment?

[Shimin Guo]

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?

[Richard]

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

Here you mean "mkdir -p a/b/c" correct? 

 

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?

One way could be to model directory operations within ats... 

Just a quick (naive) idea...

#include "share/HATS/temptory_staload_bucs320.hats"

// Here 'Dir' is a (linear) datatype or 
// data-view-type as they call it in ats
// it is defined using mutual recursion to allow
// rmdir to work properly (as in only work for empty dirs)
// rmdir_dir should probably be named rm_r

datavtype Dir =

  | empty of Empty

  | dir of (string, subdirs)

  and Empty = empty_dir of (string)

where subdirs = list_vt(Dir)

extern fun mkdir_empty : string -> Empty

extern fun mkdir_dir : (string, subdirs) -> Dir

extern fun rmdir_empty : Empty -> void

extern fun rmdir_dir : Dir -> void

implfun mkdir_empty(path) = empty_dir(path)

implfun rmdir_empty(dir) =

  case+ dir of

    | ~empty_dir(_) => ()

implfun mkdir_dir(path, opt_dirs) = dir(path, opt_dirs)

implfun rmdir_dir(dirp) =

  case+ dirp of

    | ~empty(x) => (rmdir_empty(x))

    | ~dir(_, subdirs) => (list0_vt_foreach0<Dir>(subdirs)) where

    {

      impltmp

      list0_vt_foreach0$work<Dir>(x) = rmdir_dir(x)

    }

#symload mkdir with mkdir_empty

#symload mkdir with mkdir_dir

#symload rmdir with rmdir_empty

#symload rmdir with rmdir_dir

#define :: list0_vt_cons

#define nil list0_vt_nil

implfun main0() =

{

  val xs = mkdir("hey")

  val () = rmdir(xs)

  val xs = mkdir("empty0")

  val ys = mkdir("empty1")

  val zs = mkdir("full0", empty(xs)::empty(ys)::nil())

  // if we do not free our linear datatype 'Dir' as
  // seen below, the typechecker will warn us that 
  // zs needs to be consumed.
  // val () = rmdir(zs)

}

 

[Richard]

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:

[Shimin Guo]

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 :)

--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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.

[Richard]

On Saturday, June 1, 2019 at 2:26:33 AM UTC-4, Shimin Guo wrote:

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 :)

Sure you could do it, you already have a perspective of what you would like to improve. By that, you have already accomplished half the battle! 

For such an idea, linear viewtypes in ATS are a great start on your journey. I would encourage you to learn more about them. Here is a good place to start http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/p3319.html. Programming with linear viewtypes is definitely one of (if not the most) advanced features in ATS however, once you get some understanding you will find that programming with viewtypes is quite intuitive. 

Best, 

Richard

[Artyom Shalkhakov]

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.

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.

[Shimin Guo]

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?

--

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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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.

[Chris Double]

On Sun, Jun 2, 2019 at 10:24 AM Shimin Guo <smgu...@gmail.com> wrote:
> 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.

I also use Ansible in my daily work and have desired a more type safe
way of handling deployment, etc. I'm very interested in seeing what
you come up with. I ended up exploring a more prolog-like solution,
but would still like to see what's possible in the typed world. I went
for prolog to solve the problem of "Here is system in state A", "here
is my target state, B", search for the optimal commands to run that
take the system from A to B.

An approach I was considering doing was having an ATS program generate
an ansible playbook when run. So instead of writing error prone
Ansible/Python, write ATS which checks the types like your examples,
and when run it produces the Ansible playbook.

--
http://bluishcoder.co.nz

[Shimin Guo]

Interesting, anything you can share about your prolog-based approach? Sounds like I finally have an excuse to learn prolog :)

--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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/CALn1vHFgf83RgKYTDfBvNzt217zcOqN99cwAQPTtOrqJce-%3Dnw%40mail.gmail.com.