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)’ )

On Sunday, February 10, 2019 at 6:17:03 PM UTC-5, [email protected] 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 [email protected].
To post to this group, send email to [email protected].
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/7ad6f308-def1-48e1-87aa-22c352f932d6%40googlegroups.com.

Reply via email to