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