Need help understanding free@

[rnag...@stevens.edu]

Hi all,

I'm facing some difficulty understanding how `free@' is used. I'm going through the Introduction to Programming in ATS book, and the example I'm facing trouble with is this,

fun{
a:t@ype
} list_vt_free
  {n:nat}.<n>. (xs: list_vt (a, n)): void =
  case+ xs of
  | @list_vt_cons(x, xs1) => let
      val xs1_ = xs1
      val () = free@{a}{0}(xs) in list_vt_free (xs1_)
      end
  | @list_vt_nil () => free@{a} (xs)

Why is it `free@{a}{0} (xs)' and not `free@{a}{0} (x)'? It seems that `free@' requires an unfolded constructor (here, it is operating on `list_vt_cons_unfold'). However, that begs the question -- how does `free@' know to free only the first node of the list and not the rest of the list? Any help understanding this will be much appreciated!

Thanks,

Ramana

[Richard]

If I remember correctly the node that is freed is based on the second static argument provided ( in this case, the 0 in ‘free@{a}{0}(xs)’ )

[gmhwxi]

A list node contains two cells: one holding the content and the other holding

the pointer to the next node (or null).

When xs matches the pattern @list_vt_cons(x, xs1), xs refers to a list node;

x refers to the content cell and xs1 refers to the pointer cell. In this case, the

content is non-linear (a:t@ype) and thus does not need to be moved out. But

the pointer needs to be moved out before xs can be freed:

val xs1_ = xs

The above code was written long time ago. It could be prettified a bit as follows:

fun
{a:t@ype}
list_vt_free
  {n:nat} .<n>.
  (xs: list_vt(a, n)): void =

(
  case+ xs of
  | ~list_vt_nil() => ()
  | @list_vt_cons(_, xs1) =>
    let
      val xs1 = xs1
    in
      free@{a}{0}(xs); list_vt_free<a>(xs1)
    end
)

People are often puzzled by a beautiful line like 'val xs1 = xs1' :)

[Ramana Nagasamudram]

Haha yeah `val xs1 = xs1' is quite confusing coming from other languages.

Your explanation helps a lot, and I understand the concept much better now. Thanks! Time to finish the rest of the book :)

 

---

From: ats-lan...@googlegroups.com on behalf of gmhwxi <gmh...@gmail.com>
Sent: Sunday, February 10, 2019 8:44 PM
To: ats-lang-users
Subject: Re: Need help understanding free@

 

--
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/e02a34b7-8150-482a-9f9b-93b89e063042%40googlegroups.com.

[Richard]

In the provided example, why is it that we can replace zero with any natural number?

...
free@{a}{123456(*insert random nat here*)}(xs);...
...

(typechecks and compiles with no issues...)

[gmhwxi]

This is due to

'list_vt_cons' being given the following type:

{a:t@ype]{n:nat}(a, list_vt(a, n)) -> list_vt(a, n)

free@ is give the following type:

a:t@ype]{n:nat}(a?, list_vt(a, n)?) -> void

Because list_vt(a, n1)? and list_vt(a, n2)? are the same

for any n1 and n2, it does not matter what 'n' you use as

long as it is a natural number.

On Sunday, February 10, 2019 at 9:20:29 PM UTC-5, Richard wrote:

    In the provided example, why is it that we can replace zero with any natural number?

    ...
    free@{a}{123456(*insert random nat here*)}(xs);...
    ...

    (typechecks and compiles with no issues...)


    On Sunday, February 10, 2019 at 8:43:22 PM UTC-5, gmhwxi wrote:

On Sunday, February 10, 2019 at 9:20:29 PM UTC-5, Richard wrote:

In the provided example, why is it that we can replace zero with any natural number?

...
free@{a}{123456(*insert random nat here*)}(xs);...
...

(typechecks and compiles with no issues...)


On Sunday, February 10, 2019 at 8:43:22 PM UTC-5, gmhwxi wrote: