Re: [Factor-talk] Simulating linear types or resource tracking?

[George C. <geo...@gm...>]

I can't say about linear types, but I've dealt with types for concatenative
languages. There is an exceptionally good dissertation by Kleffner
https://repository.library.northeastern.edu/files/neu:4f186p17k/fulltext.pdf
It is useful to read Diggins' sketch before it
https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=17e9322160dc1e26cc85bb26f8ef7b8a560cb07c
Factor has a rudimentary type check (stack effect check), it is done by the
'stack-checker' dictionary. The algorithm itself is taken from the Java
stack machine,
 so it does not always work (there are no quotations in Java). I thought
about rewriting it according to Kleffner, but it is built into the compiler
as the first stage,
 and part of the compiler needs to be rewritten along with it (I'm not
ready yet).

пт, 13 июн. 2025 г. в 12:24, toastal <to...@po...>:

> Wanting to understand how safety is handled in Factor being an absolute
> concenative novice… Last year I went out to learn ATS2
> <https://www.cs.bu.edu/~hwxi/atslangweb/> in the ML family (those
> familar with OCaml or SML would be familar with the syntax). One of the
> standout features was linear types for safe resource tracking (closing
> file handles, always calling free, disallowing double free—where affine
> types only assert can be used at most once vs. linear types *must* be
> used exactly once). While the ATS2 language is a bit obtuse &
> unconventional, it felt very safe to use it due to explicit typing. For
> a ‘trivial’ example:
>
> ------------------------------------------------------------------------
>
> #include "share/atspre_define.hats"
> #include "share/atspre_staload.hats"
>
> implement main0 (): void = {
>         (* allocate for an integer, returning a tuple with proofs for
> values
>         & token for garbage collection | the pointer address *)
>         val (pfval, pfgc | ptr) = ptr_alloc<int>()
>
>         (* set pointer value to 42 (! is sugar to dereference @ address) *)
>         val () = !ptr := 42
>
>         (* get pointer value assiging to x *)
>         val x = !ptr
>
>         (* prints “x = 42” to console *)
>         val () = println!("x = ", x)
>
>         (* frees pointer using consuming both linear types *)
>         val () = ptr_free(pfgc, pfval | ptr)
> }
>
> ------------------------------------------------------------------------
>
> If I skip the ``ptr_free(…)`` I will get a compiler error:
>
> > the linear dynamic variable [pfval$8389(-1)] needs to be consumed but
> > it is preserved with the type [S2Eat(S2Eapp(S2Ecst(g1int_int_t0ype);
> > S2Eextkind(atstype_int), S2Eintinf(42)),
> > S2Evar(l$14498$14499$14500(23073)))] instead.
>
> If duplicate the ``ptr_free(…)`` line, I will get this compiler error:
>
> > the linear dynamic variable [pfgc$8390(-1)] is no longer available.
>
> It’s a lot of manual code, but these linear types prevent leaks & enforce
> cleanup at the compiler level. These types are not limited to
> hardware-level resource tracking in the sense that you could use this to
> model in the type system of a game that you can’t unlock already
> unlocked door & unlocking a door consumes a key.
>
> I understand Factor does not have these sorts of types (almost no
> languages do) & is dynamically typed (ignoring ``TYPED:``), but I am
> curious, especially from the C FFI side of things where freeing is
> normally a manual/error-prone task, how would the Factor language, or
> concatenative languages in general, model resource tracking. Is there
> some sort of stack mechanism to sort of enforce cleanup or other
> contracts?
>
> — toastal
>
>
> _______________________________________________
> Factor-talk mailing list
> Fac...@li...
> https://lists.sourceforge.net/lists/listinfo/factor-talk
>