A linear closure (lincloptr1) is a linear value; like any other linear
values,
it needs to be used (that is, called) once and only once.
A closure is a pair (f, env); where 'f' is a function pointer, which is
non-linear,
and env is a record. If env contains a linear value, then the closure (f,
env) is
linear. If you want to have a "linear" function that can be called multiple
times,
you should try (in ATS2) to create a linear stream; evaluating the stream
once
amounts to calling the function once.
It is possible that we support other forms of linear functions in ATS3. In
any case,
I feel that this would just be a niche feature; its implementation tends to
be involved
but its usefulness is rather limited.
--Hongwei
PS: For instance, the 'move' trick in Rust can be readily implemented in
ATS2. But
doing it also complicates type-checking in a non-trivial way.
On Tuesday, August 18, 2020 at 3:53:51 PM UTC-4, Dambaev Alexander wrote:
>
> In fact, I had some issues to express the same thing in ATS2. The closest
> sample (in case if Rust does stack allocation of the clone of the line in
> closure) is:
> ```
> staload UN="prelude/SATS/unsafe.sats"
>
> extern prval hack{l:addr} ( pf: int @ l): void
>
> fn
> linum
> {l:addr}
> (
> ):
> ( (int0 @ l)
> | ( !(int0 @ l)
> | ()
> ) -<cloptr1>
> void
> ) = (pf | f) where {
> var original:int0 with pf= 0 (* pf is a linear variable here *)
> fn
> f
> ( pf: !(int0 @ original)
> | ()
> ):<cloptr1>
> void = {
> val () = original := original + 1
> val () = println!("line = ", original)
> }
> }
>
> implement main0() = {
> val (pf | f) = linum( )
> val ( ) = f( pf | () )
> val ( ) = f( pf | () )
> prval () = hack( pf) (* tell type system, that pf had been consumed *)
> val () = cloptr_free( $UN.castvwtp0(f))
> }
> ```
> But this will not compile, obviously, because *original* will be removed
> at linum's exit.
>
> The compilable example uses heap to clone *original* value, which should
> be freed explicitly. I am not sure if it follows the same semantic as Rust
> sample (I guess, only valgrind/disassembler should give an answer if rust
> uses heap for this as well)
>
> ```
> staload UN="prelude/SATS/unsafe.sats"
>
> extern prval hack{l:addr} ( pf: int @ l): void
>
> fn
> linum
> (
> ):
> [l:addr]
> ( mfree_gc_v l
> | ptr l
> , (
> ) -<lincloptr1>
> ( (int @ l)
> | (**)
> )
> ) = ( free_pf | p, f) where {
> var original:int = 0
> val (pf, free_pf | p) = ptr_alloc_tsz(sizeof<int>)
> val () = !p := original (* clone value *)
> val f = llam () =<lincloptr1> ( pf1 | (**)) where {
> prval pf1 = pf
> val () = !p := g0int_add_int( !p, 1) (* !p + 1 confuses a template
> selector for some reason *)
> val () = println!("line = ", !p)
> }
> }
>
> implement main0() = {
> val ( free_pf | p, f) = linum( )
> val ( pf | (**) ) = f( )
> (*
> *prval () = hack( pf) (* have to consume pf *) val ( pf | (**) ) = f( )*
> *)
> val () = ptr_free( free_pf, pf | p)
> val () = cloptr_free( $UN.castvwtp0(f))
> }
>
> ```
>
> the bold part had been commented out, because ATS does not allow to call
> linear closure multiple times, so uncommenting leads to a compilation error.
> But I am not an experienced user of ATS, so I might not know some tricks
> to either to reuse a linear closure, to capture linear variables in
> non-linear closures or to return a new linear closure from the f ( but I
> was not able to express the type of such function, and it seems, that the
> example with lazy stream/stream_vt does similar thing)
>
>
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/213286ae-d06a-4230-ba71-b2cfe1207194o%40googlegroups.com.
