Re: A small query about closures

[Hongwei Xi]

The following header:

fn
linum (): void -<cloref1> void = 

should be changed to

fn
linum (): () -<cloref1> void =

But this does not give what you expected.

You could use a reference:

fn
linum (): () -<cloref1> void=
let
val
line = ref<int>(0)
in
lam () =>
let
val () = !line := !line + 1
in
println! ("Current line number = ", !line);
end
end

implement
main0() =
{
val f0 = linum()
val () = f0()
val () = f0()
val f1 = linum()
val () = f1()
val () = f1()
}

On Tue, Aug 11, 2020 at 10:10 AM Timmy Jose <zolta...@gmail.com> wrote:

Hello,

I have a small closure implementation in Rust which looks like so:

fn linum() -> impl FnMut() {
    let mut line = 0;

    Box::new(move || {
        line = line + 1;
        println!("Current line number is {}", line);
    })
}

fn main() {
    let mut l = linum();
    for _ in 0..5 {
        l();
    }

    l = linum();
    for _ in 0..5 {
        l();
    }
}

Basically, I simply want to capture the line variable in my closure. Running it:

$ rustc linum.rs && ./linum
Current line number is 1
Current line number is 2
Current line number is 3
Current line number is 4
Current line number is 5
Current line number is 1
Current line number is 2
Current line number is 3
Current line number is 4
Current line number is 5

as expected. Now, I was trying to replicate this behaviour in ATS (please note that I am totally new to ATS) using the chapter on functions, and this was my attempt:

fn
linum (): void -<cloref1> void=
  let val line = 0
  in
   lam () =>
      let val line = line + 1
      in
       println! ("Current line number = ", line);
      end
  end

which gives the following errors:

$ make
acc pc -DATS_MEMALLOC_LIBC -O3 -o closures closures.dats

/Users/z0ltan/dev/study/ats/introduction_to_programming_in_ats/revision/chapter3/closures.dats: 12:4-16:10

   error(3): dynamic arity mismatch: more arguments are expected.

patsopt(TRANS3): there are [1] errors in total.
      exit(ATS): (1025)
make: *** [closures] Error 1

Can someone help me understand what the problem is? I'm pretty sure my knowledge of ATS is not enough right now to maybe fully implement this the way I want it, but I would like some pointers on this error message and maybe a nudge in the right direction to be able to implement this!

Thanks!

Best Regards,

Timmy

(P.S: I hope it's all right if I keep posting questions every so often? I tried the IRC channel, but it appears to be inactive. Please let me know otherwise, in which case I'll bunch up my questions after having finished the basic tutorials!).

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/92bd27f3-5d34-48dc-ac71-b9924ec58b4dn%40googlegroups.com.

[gmhwxi]

BTW, I don't quite understand what the Rust program does in terms of

memory management.

If you want a memory-clean implementation ATS, then you can do it as follows:

#include
"share/atspre_staload.hats"

fun
{a:t@ype}
stream_vt_uncons
(xs: &stream_vt(a)): a =
let
val-
~stream_vt_cons(x0, tl) = !xs in (xs := tl; x0)
end

fun
linum
(line: int): stream_vt(int) =
$ldelay

let
val
line = line + 1

val () =

println!
("Current line number = ", line)

in
  stream_vt_cons(0, linum(line))
end

implement
main0() =
{
var f0 = linum(0)
val _1 = stream_vt_uncons(f0)
val _2 = stream_vt_uncons(f0)
val () = ~f0
var f0 = linum(0)
val _1 = stream_vt_uncons(f0)
val _2 = stream_vt_uncons(f0)
val () = ~f0
}

Valgrind confirms the memory-cleanness of the implementation:

==30566== Memcheck, a memory error detector
==30566== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==30566== Using Valgrind-3.11.0 and LibVEX; rerun with -h for copyright info
==30566== Command: ./abcde_dats
==30566==
Current line number = 1
Current line number = 2
Current line number = 1
Current line number = 2
==30566==
==30566== HEAP SUMMARY:
==30566==     in use at exit: 0 bytes in 0 blocks
==30566==   total heap usage: 11 allocs, 11 frees, 1,184 bytes allocated
==30566==
==30566== All heap blocks were freed -- no leaks are possible
==30566==
==30566== For counts of detected and suppressed errors, rerun with: -v
==30566== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.

[Dambaev Alexander]

Hi,

I want to ask someone who knows Rust about this example: if I remember correctly, mutable variable in Rust is stack allocated, so I want to know how it is able to move line to a closure, because I thought, that the lifetime of line is the same as lifetime of linum(). Am I missing something?

[Timmy Jose]

Hey Hongwei,

Thanks for the reply! I have no idea what happened, but my message was auto-deleted by Google groups, and I thought it had disappeared for good, so was surprised to see the notifications now! :-)

By the way, I had got a working version in the meantime which looks remarkably like the first one you shared. Here is the version I came up with:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

fn
linum () :<cloref1> () -<cloref1> void = 
  let val line = ref<int> (0)
  in
    lam () =<cloref1> (
      !line := !line + 1;
      println! ("Current line number is ", !line)
    )
  end

fun loop (li0: () -<cloref1> void, n: int): void = 
  if n > 0 then (li0 (); loop (li0, n - 1))

implement main0 () = {
  val li0 = linum ();
  val () = loop (li0, 5)

  val li0 = linum ()
  val () = li0 ()
  val () = li0 ()
  val () = li0 ()
}

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.

[Timmy Jose]

Yes! This looks quite like more in line with the Rust version as well. I'm still in Book 2 of "Introduction to programming in ATS", but I assume that this version uses linear types, right?

Thank you. I will analyse this code snippet and try to make sense of it. Hopefully I should be able to wrap up the first tutorial book soon so that I can understand it fully. :-)

Cheers,

Timmy

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.

[Timmy Jose]

Hey Alexander,

The `mut` in line is simply so that the variable can be modified inside the closure. The actual magic happens with the `Box` and `move`. So we move the ownership of `line` to the closure with the `move`, and the `Box` allocates it on the heap, passing the ownership of the closure itself to the client code.

(Hence also the `FnMut` type for the returned closure).

Cheers,

Timmy

[Dambaev Alexander]

Hi, Timmy.

That is why I have asked: for me, `line` is stack allocated and have to be freed at linum()'s exit. That is why I am asking how rust is able to move it to a closure, which lives longer than `linum()` itself. In my world, I was sure, that only heap allocated memory is being able to survive after exit of function, in which it had been allocated. The only way it is able to work, for me, is that it implements trait Copy, such that closure contains a mutable copy of line and original line is being freed as expected at linum's exit.

speaking of linearity: no, in ATS you should use either view or viewtypes explicitly, which are linear.

ATS's `ref int` is an analogue to `Box<int>` in Rust: ie it is a boxed value (heap allocated)

[Timmy Jose]

HI Hongwei,

Ah, okay, Sorry, I misunderstood the original question (including Alexander's) !

Yes, you're quite right. In this case, `line` is a Copy-able trait, so the `move`  would copy over `line` into the closure, but would not invalidate the local copy of `line` (inside `linum`). If `line` were not a Copy-able type, then, of course, the value would still be copied over to the closure as part of the `move`, but the

value in `linum` would now be invalidated. So the `move` part is sort of orthogonal to the actual mechanism of the move itself - it is required by the ownership system whether the value is Copyable or not, but the actual mechanism of the move would be copying over the value (I'm sure the compiler must do

some sort of copy elision/optimisations to mitigate the overhead as much as possible).

So, something like the following works:

fn foo () -> impl FnMut() -> () {
    let mut line = 0; // copyable type
   
    let baz = Box::new(move || {
        line += 1;
        println!("line is {}", line);
    });

 

   // local copy still works since the move

  // only did a copy of a Copyable type
    println!("local line is {}", line);
    line += 100;
    println!("local line is {}", line);
   
    baz
}

fn main() {
    let mut bar = foo();
    bar();
    bar();
}

whereas the following does not work since `Box<T>` is not a Copy-able type:

fn foo () -> impl FnMut() -> () {
    let mut line = Box::new(0); // non-Copyable type
   
    let baz = Box::new(move || {
        *line += 1;
        println!("line is {}", line);
    });

   // the Ownership system will not

  // allow this since the move was

// done on a non-Copy type

    println!("local line is {}", line);

    *line += 100;
    println!("local line is {}", line);
   
    baz
}

fn main() {
    let mut bar = foo();
    bar();
    bar();
}

Cheers,

Timmy

[Timmy Jose]

Ah sorry, that previous message was directed to Alexander. My bad! :-).

Best,

Timmy

P.S: Also, thanks for the tip on using viewtypes and linearity (right now I don't understand much of those terms, but hopefully soon!). Much appreciated.

[Dambaev Alexander]

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)

[gmhwxi]

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.