fun foo(x: ? >> T2) : T3
means
fun foo(x: &(T1?) >> T2): T3
T1? is the uninitialized version of T1. Also, there is the subtype
relation: T1 <= T1?
(if T1 is a non-linear type).
For every viewtype VT, there are V (linear) and T (non-linear) such that VT
= (V | T).
This T can be referred to as
Thanks! What happens when you have
fun foo(x: ? >> T2): T3
rather than
fun foo(x: >> T2): T3
?
How does one handle uninitialized values? Is that just the ? modality?
On 10/28/18 6:05 PM, Hongwei Xi wrote:
> Say you have a function of the interface:
>
> fun foo(x: >> T2): T3
>
> Internally,
Say you have a function of the interface:
fun foo(x: >> T2): T3
Internally, foo is given the following type:
fun foo{l:addr}(pf: T1@l | x: ptr(l)): (T2@l | T3)
The notation ' >> T2' is referred to as before-and-after notation.
Here is a paper that contains a lot of technical details
on views
Hi all,
Is there any literature on types in ATS such as ? >> int?
fun ret_zero() : int =
let
fun initize(x : ? >> int) : void =
x := 0
var ret: int
val () = initize(ret)
in
ret
end
I know that linear types are well-grounded in linear logic, but I know
of no language
