When I tried to understand what is vStrptr, I found the following code from ATS prelude source code. But I’m not sure about the purpose of those “vttakeout” definitions. Do you have any idea of why people are defining these and how to use them? Thank you very much.
Say you have a value v1 of linear type VT1 and you want to take a component
v2 out of v1 that is of linear type VT2; you then make use of v2 and return
it back.
‘vttakeout’ is introduced to address such a scenario.
vStrptr is the type for a “temporary” linear string. Let me use the
function getenv (declared in stdlib.h)
as an example:
fun getenv (name: string): vStrptr0
Given a name, the function getenv returns the value associated with the
name in the current environment.
The returned value is linear: it cannot be safely embedded into another
value. However, the returned value
cannot be given the type Striptr: it cannot be explicitly freed.
There is another function getenv_gc in libc/SATS/stdlib.sats:
fun getenv_gc (name: string): Strptr0
This function calls getenv to get a vStrptr and then make a copy of it.
Thanks for your answer. But I still have questions.
Is the vt2 -<lin,prf> vt1 part used for consuming vt2 and returning back vt1
?
(But what’s that? It’s a type, but it seems that there isn’t any concrete
proof function for this type. Is it just a declaration or I miss
something?)
Should we apply that to vt2 manually or not after using vt2?
(I think it should be called manually, right?)
Does it mean that we can use such things to block access to the original vt1(since
it’s not there anymore), takeout part of it, modify it, and ensure
programmers to put it back? What if I’d like to take out something for a
"read-only" purpose? Can’t I just use “string” instead?