ATS-Postiats’ Blog¶
Some other sources of ATS: ATS Wiki.
Contents:
Global value with linear type¶
Global values with linear type can only be used in the global scope. They cannot be used inside a function scope. For example, the following code cannot pass the type checking.
staload
UNSAFE = "prelude/SATS/unsafe.sats"
absvtype VT
extern fun create (): VT
extern fun use (v: !VT): void
val v = create ()
fun temp (): void = let
val () = use (v)
in
end
implement main0 () = ()
- ATS compiler conplains that
- regexp_main.dats: 177(line=15, offs=17) – 178(line=15, offs=18): error(3): the linear dynamic variable [v$64(-1)] is expected to be local but it is not. regexp_main.dats: 177(line=15, offs=17) – 178(line=15, offs=18): error(3): a linear component of the following type is abandoned: [S2Ecst(VT)]. patsopt(TRANS3): there are [2] errors in total. exit(ATS): uncaught exception: _2home_2alex_2programs_2ats2_github_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
Usually we would cast the global value of linear type into non-linear type, and cast it back inside a function scope, which is shown below:
staload
UNSAFE = "prelude/SATS/unsafe.sats"
absvtype VT
extern fun create (): VT
extern fun use (v: !VT): void
val v = create ()
val ele = $UNSAFE.castvwtp0{ptr}(v)
fun temp (): void = let
val v1 = $UNSAFE.castvwtp0{VT}(ele)
val () = use (v1)
prval ((*void*)) = $UNSAFE.cast2void (v1)
in
end
implement main0 () = ()