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: > > > 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' :) > > On Sunday, February 10, 2019 at 6:17:03 PM UTC-5, rnagasam wrote: >> >> 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 >> > -- 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/6495082c-d729-4027-8189-592346f21f4f%40googlegroups.com.