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:
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:
>>
>>
>> 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 [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/da5a2f85-5ce0-465f-845d-54d9328bcf34%40googlegroups.com.
