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 " be? It seems it needs to consume all the 
linear props in the "environment" in the form of exists(p) where p is under 
. 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/64e7fb4b-f8f1-4d6f-9046-c80c3f587e81%40googlegroups.com.

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

[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 " be? It seems it needs to consume all 
> the linear props in the "environment" in the form of exists(p) where p is 
> under . 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(subdirs)) where
{
  impltmp
  list0_vt_foreach0$work(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)
}

 

-- 
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/73a0eddd-afe7-413b-9c6d-699d5a6c4087%40googlegroups.com.

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

[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:
>
> 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 " be? It seems it needs to consume all 
> the linear props in the "environment" in the form of exists(p) where p is 
> under . 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.

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

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

On Fri, May 31, 2019 at 7:03 PM Richard  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 " be? It seems it needs to consume all
>> the linear props in the "environment" in the form of exists(p) where p is
>> under . 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
> 
> .
>

-- 
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.

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

[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

-- 
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/2cc575cc-4257-4db6-ae81-c49e4de403b0%40googlegroups.com.

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

[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.

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 " be? It seems it needs to consume all 
> the linear props in the "environment" in the form of exists(p) where p is 
> under . 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

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

[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?

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 " be? It seems it needs to consume all
>> the linear props in the "environment" in the form of exists(p) where p is
>> under . 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

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

[Chris Double]

On Sun, Jun 2, 2019 at 10:24 AM Shimin Guo  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

-- 
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/CALn1vHFgf83RgKYTDfBvNzt217zcOqN99cwAQPTtOrqJce-%3Dnw%40mail.gmail.com.

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

[Shimin Guo]

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

On Sun, Jun 2, 2019 at 7:46 PM Chris Double 
wrote:

> On Sun, Jun 2, 2019 at 10:24 AM Shimin Guo  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
>
> --
> 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/CALn1vHFgf83RgKYTDfBvNzt217zcOqN99cwAQPTtOrqJce-%3Dnw%40mail.gmail.com
> .
>

-- 
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%2B7DsfnTT-CQQcTr7Y3SnyHVSdskQ_aM8wvs3Wto2NuxohQ%40mail.gmail.com.