Call-by-value assignment

[M88]

Hello,

I have a viewtype and I am using it in a call-by-value function.  I want to temporarily assign it to a variable for use in a template that uses call-by-reference.

Is there a way to assert that the variable has not been consumed?

Right now I am doing this, which typechecks and compiles in my case:

extern fun {env}

some_template( env : &env >> _ ) : void

fun f ( x: !VT) : void =

    let

         var env = x

         val _ = some_template<VT>(env)

         prval () = $effmask_all(

                x := env

          )

    in

   end

Is this expected behavior?  Is it possible to write a proof function that can restore "x"?

( Ultimately, x does not change, and the semantics of call-by-value seem best for this function ).

[Hongwei Xi]

The following line is problematic:

prval () = $effmask_all(x := env)

as assignment is definitely not a proof.

I suggest that you just do

val () = x := env

The compiler should allocate the same memory for both x and env.

Theoretically, you could separate x into two parts: data and (linear) proof;

only move the data into env; there is no need to move the data back from env

into x since the data is non-linear. Really not worth the trouble :)

--
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/ce57d10d-cb0a-465f-b9f6-954d7d6678cb%40googlegroups.com.

[Artyom Shalkhakov]

Hi, M88 and Hongwei,

On Sunday, February 24, 2019 at 5:45:34 PM UTC+2, gmhwxi wrote:

The following line is problematic:

prval () = $effmask_all(x := env)

as assignment is definitely not a proof.

I suggest that you just do

val () = x := env

The compiler should allocate the same memory for both x and env.

Flat viewtypes are represented by plain C structs in ATS, that is, they are directly copyable. I think this should give the C compiler a hint.

 

Theoretically, you could separate x into two parts: data and (linear) proof;

only move the data into env; there is no need to move the data back from env

into x since the data is non-linear. Really not worth the trouble :)

In practice, records are really tough to handle this way (especially the initialization and free -- casts galore! :)).

[M88]

The following line is problematic:

prval () = $effmask_all(x := env)

as assignment is definitely not a proof.

This looked a bit off.  I suppose in theory, one could wrap any function in $effmask_all and use it in proofs.

 

I suggest that you just do

val () = x := env

The compiler should allocate the same memory for both x and env.

in my case, this caused a C compilation error, "Invalid use of void expression."  Perhaps it's because VT happened to be a file descriptor.

I had supposed assignment was invalid for a call-by-value argument, but it would make more sense if "x" was a pointer.  Would this end up being the equivalent of "(*x) = env" in C?

 

Theoretically, you could separate x into two parts: data and (linear) proof;

only move the data into env; there is no need to move the data back from env

into x since the data is non-linear. Really not worth the trouble :)

I'd tend to agree :)

Another dimension is that I would need to implement templates in terms of the data.  My interface is currently in terms of VT, so it would likely require casting from within the template implementation (or, duplicating an interface in terms of some data type T).  Since some functions might reference T in an unsafe way, it's probably the equivalent of casting.

I gave it some thought, and the two best options appeared to be:

a) Since my interface is in terms of VT, the simplest thing seemed to be this:

         var env = $UNSAFE.castvwtp1{VT}(x)

         val _ = some_template<VT>(env)

         prval () = $UNSAFE.cast2void(env)

b) Supposing I want to keep things nice[ish], I could create an interface like this:

    

       absvt@ype VT0(x:id)

       castfn vt_take( !VT(x) >> VT0(x) ) ->  VT(x)

       prfn vt_put( !VT0(x) >> VT(x), VT(x) ): void

       .....

       var env = vt_take(x)

       val _ = some_template<VT(x)>(env)

       prval () = vt_put( x, env )

Version b seems pretty good for this case.

[Hongwei Xi]

>> val () = (x := env)

My mistake. This would not work as 'x' is not a left-value.

Both (a) and (b) look like a reasonable way to get around this issue.

I would probably use (a).

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/7b9e6024-d973-496e-b5b9-0c76835f3d4d%40googlegroups.com.