githwxi / ATS-Postiats

ATS2: Unleashing the Potentials of Types and Templates
www.ats-lang.org
Other
354 stars 54 forks source link

'Move' linear variable? #276

Closed sparverius closed 1 year ago

sparverius commented 1 year ago

Surely we have discussed this at length at some point in the past...

Being that embedded templates are nice alternatives to closures, I've been wondering about the following:

although this is a (silly) contrived example, is there a "safe" way to 'move' the linear view type variable into the embedded template?

Looking at this particular example, the compiler can infer that the freeing of the element in question will need to be handled by the caller of the function...... perhaps I've been programming in rust too long and have since confused the idea of "at most once" vs. "exactly once"

extern fn{T:vt@ype} function(): T
extern fn{T:vt@ype} function$embedded_template: () -> T

implement{T} function() = function$embedded_template()

fun{} silly_fun(): List_vt(int) = {
    val linear_list: List_vt(int) = $list_vt{int}(1,2,3)
    val result = function<List_vt(int)>()
        where {
            implement
            function$embedded_template<List_vt(int)>() = (*MOVE*) linear_list
        }
    val () = println!(result)
}

// ... the linear dynamic variable "linear_list" is expected to be local but it is not ...
sparverius commented 1 year ago

for the sake of completeness with the above questions, here are some amusing alternatives (and ramblings...)


#include "share/atspre_staload.hats"

#staload UN = "prelude/SATS/unsafe.sats"

sortdef vtbox = vt@ype

extern fn{T:vtbox} function(): T
extern fn{T:vtbox} function$embedded_template: () -> T

implement{T} function() = function$embedded_template()

// Assumptions:
// - 'var'           is allocated on heap
// - $list_vt{..}... is allocated on heap
fun{} silly_fun(): List_vt(int) = result where {
    var linear_list: List_vt(int) = $list_vt{int}(1,2,3)
    val result = function<List_vt(int)>()
        where {
            implement
            function$embedded_template<List_vt(int)>() = res
            where {
              // this is clearly not ideal...esp. for threads, async...
              val (pf, fpf | p0) = $UN.ptr_vtake(addr@(linear_list))
              val res = $UN.ptr0_get(p0)
              prval() = fpf(pf)
            }
        }
    val () = println!(result)           // to easily verify...
    val () = $UN.castvwtp0(linear_list) // cast to avoid double free...
}

// is there instead a way to just "move" the 'linear_list' into the embedded template?
// perhaps the only way is to make a copy?
(*
fun{} silly_fun(): List_vt(int) = {
    val linear_list: List_vt(int) = $list_vt{int}(1,2,3)
    val result = function<List_vt(int)>()
        where {
            implement
            function$embedded_template<List_vt(int)>() = MOVE(linear_list)
        }
    val () = println!(result)
}
*)

extern fn{T:vtbox} function(): T
extern fn{T:vtbox} function$embedded_template: () -> T

implement{T} function() = function$embedded_template()

fun{} silly_fun_copies(): List_vt(int) = result where {
    var linear_list: List_vt(int) = $list_vt{int}(1,2,3)
    val result = function<List_vt(int)>() where {
            implement
            function$embedded_template<List_vt(int)>() = res
            where {
                val (pf, fpf | p0) = $UN.ptr_vtake(addr@(linear_list))
                val tmp = $UN.ptr0_get(p0)
                prval() = fpf(pf)
                val res = list_vt_copy<int>(tmp)
                val () = $UN.castvwtp0(tmp) // otherwise double free...
            }
        }
    val () = println!(result)
    val () = free(linear_list)
}

implement main0() = free(silly_fun_copies<>())
githwxi commented 1 year ago

Strictly speaking, the following kind of code is ill-typed (as linear_list, a linear value, is not allowed to be used to form a closure):

fun{} silly_fun(): List_vt(int) = { val linear_list: List_vt(int) = $list_vt{int}(1,2,3) val result = function<List_vt(int)>() where { implement function$embedded_template<List_vt(int)>() = (MOVE) linear_list } val () = println!(result) }

Unfortunately, I don't have a satisfying solution yet.

okeuday commented 1 year ago

@githwxi Wouldn't this be a use-case for an aPtr1 from prelude/SATS/pointer.sats?