I am not too sure if I my question is correct or make sense but still …
Say my function takes a arrayptr and I want to access it inside a local
function without passing it as an argument , so I want to do something like
example below :
extern
fun arr_exmpl{n:nat | n > 0}
(A : !arrayptr (int,n) , n: int(n)): void
This implementation works fine :
implement
arr_exmpl (A,n) = let
fun some_fn{n:nat | n > 0}
(A : !arrayptr(int,n) ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
But not this one :
implement
arr_exmpl (A,n) = let
fun some_fn ( ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
I believe(maybe incorrectly) that there must be proof for arrayptr(int,n)
when we leave/complete the function and compiler cannot guarantee that in
second implementation.
I had been under the impression that this was one of the uses of closures,
but ATS is the first language I’ve used closures in, and I have not
mastered the use of them as yet.
After reading this I guess that using linear variables in closures is also
problematic in the same way, as I was having trouble doing this (with
linear closures).On Wednesday, February 12, 2014 9:59:02 AM UTC-5, gmhwxi wrote:
There is a feature that allows you to temporarily bring a linear value
or linear proof into an inner function.
On Wednesday, February 12, 2014 9:36:39 AM UTC-5, gmhwxi wrote:
The type of a linear value may change, so it needs to be
tracked explicitly. If a linear value is used in an inner function
implicitly, then tracking cannot be easily done.
On Wednesday, February 12, 2014 9:05:52 AM UTC-5, chotu s wrote:
There is typo in 2nd implementation , it should be some_fn() .
On Wednesday, February 12, 2014 7:25:05 PM UTC+5:30, chotu s wrote:
Hello,
I am not too sure if I my question is correct or make sense but still
…
Say my function takes a arrayptr and I want to access it inside a local
function without passing it as an argument , so I want to do something like
example below :
extern
fun arr_exmpl{n:nat | n > 0}
(A : !arrayptr (int,n) , n: int(n)): void
This implementation works fine :
implement
arr_exmpl (A,n) = let
fun some_fn{n:nat | n > 0}
(A : !arrayptr(int,n) ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
But not this one :
implement
arr_exmpl (A,n) = let
fun some_fn ( ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
I believe(maybe incorrectly) that there must be proof for
arrayptr(int,n) when we leave/complete the function and compiler cannot
guarantee that in second implementation.
The type of a linear value may change, so it needs to be
tracked explicitly. If a linear value is used in an inner function
implicitly, then tracking cannot be easily done.
On Wednesday, February 12, 2014 9:05:52 AM UTC-5, chotu s wrote:
There is typo in 2nd implementation , it should be some_fn() .
On Wednesday, February 12, 2014 7:25:05 PM UTC+5:30, chotu s wrote:
Hello,
I am not too sure if I my question is correct or make sense but still …
Say my function takes a arrayptr and I want to access it inside a local
function without passing it as an argument , so I want to do something like
example below :
extern
fun arr_exmpl{n:nat | n > 0}
(A : !arrayptr (int,n) , n: int(n)): void
This implementation works fine :
implement
arr_exmpl (A,n) = let
fun some_fn{n:nat | n > 0}
(A : !arrayptr(int,n) ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
But not this one :
implement
arr_exmpl (A,n) = let
fun some_fn ( ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
I believe(maybe incorrectly) that there must be proof for
arrayptr(int,n) when we leave/complete the function and compiler cannot
guarantee that in second implementation.
There is typo in 2nd implementation , it should be some_fn() .On Wednesday, February 12, 2014 7:25:05 PM UTC+5:30, chotu s wrote:
Hello,
I am not too sure if I my question is correct or make sense but still …
Say my function takes a arrayptr and I want to access it inside a local
function without passing it as an argument , so I want to do something like
example below :
extern
fun arr_exmpl{n:nat | n > 0}
(A : !arrayptr (int,n) , n: int(n)): void
This implementation works fine :
implement
arr_exmpl (A,n) = let
fun some_fn{n:nat | n > 0}
(A : !arrayptr(int,n) ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
But not this one :
implement
arr_exmpl (A,n) = let
fun some_fn ( ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
I believe(maybe incorrectly) that there must be proof for
arrayptr(int,n) when we leave/complete the function and compiler cannot
guarantee that in second implementation.
You can form a closure with linear values in its environment.
As can be expected, such a closure is itself linear, and it needs to
take care of the linear values in its environment.
I have to say that these kinds of features are not that important in
practice.
You can always program without using them by resorting to features that are
much simpler but slightly less safe.On Wednesday, February 12, 2014 10:32:03 AM UTC-5, Brandon Barker wrote:
I had been under the impression that this was one of the uses of closures,
but ATS is the first language I’ve used closures in, and I have not
mastered the use of them as yet.
After reading this I guess that using linear variables in closures is also
problematic in the same way, as I was having trouble doing this (with
linear closures).
On Wednesday, February 12, 2014 9:59:02 AM UTC-5, gmhwxi wrote:
There is a feature that allows you to temporarily bring a linear value
or linear proof into an inner function.
On Wednesday, February 12, 2014 9:36:39 AM UTC-5, gmhwxi wrote:
The type of a linear value may change, so it needs to be
tracked explicitly. If a linear value is used in an inner function
implicitly, then tracking cannot be easily done.
On Wednesday, February 12, 2014 9:05:52 AM UTC-5, chotu s wrote:
There is typo in 2nd implementation , it should be some_fn() .
On Wednesday, February 12, 2014 7:25:05 PM UTC+5:30, chotu s wrote:
Hello,
I am not too sure if I my question is correct or make sense but still
…
Say my function takes a arrayptr and I want to access it inside a
local function without passing it as an argument , so I want to do
something like example below :
extern
fun arr_exmpl{n:nat | n > 0}
(A : !arrayptr (int,n) , n: int(n)): void
This implementation works fine :
implement
arr_exmpl (A,n) = let
fun some_fn{n:nat | n > 0}
(A : !arrayptr(int,n) ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
But not this one :
implement
arr_exmpl (A,n) = let
fun some_fn ( ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
I believe(maybe incorrectly) that there must be proof for
arrayptr(int,n) when we leave/complete the function and compiler cannot
guarantee that in second implementation.
The type of a linear value may change, so it needs to be
tracked explicitly. If a linear value is used in an inner function
implicitly, then tracking cannot be easily done.On Wednesday, February 12, 2014 9:05:52 AM UTC-5, chotu s wrote:
There is typo in 2nd implementation , it should be some_fn() .
On Wednesday, February 12, 2014 7:25:05 PM UTC+5:30, chotu s wrote:
Hello,
I am not too sure if I my question is correct or make sense but still …
Say my function takes a arrayptr and I want to access it inside a local
function without passing it as an argument , so I want to do something like
example below :
extern
fun arr_exmpl{n:nat | n > 0}
(A : !arrayptr (int,n) , n: int(n)): void
This implementation works fine :
implement
arr_exmpl (A,n) = let
fun some_fn{n:nat | n > 0}
(A : !arrayptr(int,n) ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
But not this one :
implement
arr_exmpl (A,n) = let
fun some_fn ( ) : void = {
val v = arrayptr_get_at_gint (A,0)
(* OR val v = do something with A *)
}
in some_fn (A) end
I believe(maybe incorrectly) that there must be proof for
arrayptr(int,n) when we leave/complete the function and compiler cannot
guarantee that in second implementation.