First, what is cloref and what is cloptr? Basically, a closure is a boxed pair (fp, env), where fp is a function pointer (to an envless function in C) and env consists of a list of values.
You can think of cloref and cloptr as being defined as follows: datatype cloref = CLOREF of (fp, env) // env is non-linear datavtype cloptr = CLOPTR of (fp, env) // env is non-linear In both cases, 'env' is non-linear, that is, the contained environment consists of only non-linear values. What happens if we want a closure where the environment contains linear values? You get lincloptr: datavtype lincloptr = LINCLOPTR of (fp, linenv) // linenv is linear A lincloptr function can and should be called once and only once. In your case, term_vt is linear. If you do LAM of (strptr, term_vt -<lincloptr> term_vt) Then the problem is that a lincloptr function can only be called once. To avoid this problem, you need to build closures on your own: LAM of (strptr, env, (env, term_vt) -<fun1> term_vt) where env is the type for environments. If you use deBruijn indices, env can just be arrayptr(term_vt). Another suggestion is that you use term_rc (instead of term_vt), where 'rc' refers to reference counting. Here is an example of reference-counted lists: https://github.com/githwxi/ATS-Temptory/blob/master/libats/SATS/list_rc.sats Cheers! On Sun, Jun 7, 2020 at 8:19 AM August Alm <[email protected]> wrote: > Hi! > > For fun, I implemented an interpreter of the untyped lambda calculus > in ATS2, using "higher order syntax" (HOAS). HOAS here means that > everything proceeds from the following datatype encoding of an abstract > syntax term: > > datatype > term_t = > | Var of string > | Lam of (string, term_t -<cloref> term_t) > | App of (term_t, term_t) > > So, it uses the function type [term_t -<cloref> term_t] of the host > language, > ATS2 in this case, to encode lambda-terms. For example, the identity > function > `lam x. x` would be encoded as the term > > Lam("x", lam(t) => t) > > It all worked out nicely. Then I tried to do the same thing with linear > types, > to get an implementation that does not require garbage collection. I > started > out like this: > > datavtype > term_vt = > | Var of strptr > | Lam of (strptr, term_vt -<cloptr> term_vt) > | App of (term_vt, term_vt) > > I got all the functions working and started doing some tests and discovered > that this of course (*face palm*) does not work as I intended. It > essentially > encodes _linear_ lambda calculus because the `cloptr` type here will not > admit > things like duplication; one cannot write terms like > > Lam("z", lam(t) => App(t, t)) . > > Any suggestions? What one needs is something that behaves like [term_t], > above, but is such that all nodes of the abstract syntax tree can be > manually > freed and are considered linear by the type-checker, so that one gets the > appropriate warnings if one forgets to do so. I guess I could try to do it > all with > (data)views and pointers, no dataviewtypes, but I'm wary of doing so since > the > complexity of doing something as simple as linked lists that way is already > considerable. > > A more concrete question is: How exactly is the type [a -<cloptr> b] > defined? > Can it explicitly as "(view | type)"? How is it related to [a -<cloref> > b]? Searching > the code of the ATS2 repo on Github I can only find the type [cloptr(a)] > which > mysteriously to me, has a single type parameter. > > Best wishes, > August > > Ps. Below is complete code for the linear version that doesn't quite work > as > intended, but compiles just fine and runs memory-safely. I compile with: > > $ patscc -O2 -flto -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -o main > -latslib > > (* ***** ***** *) > > #include "share/atspre_define.hats" > #include "share/atspre_staload.hats" > staload UN = "prelude/SATS/unsafe.sats" > > (* ***** ***** *) > > // Our type-to-be of the abstract syntax trees. > absvtype > term_vt = ptr > > // Linear function type. > vtypedef > end_vt = term_vt -<cloptr1> term_vt > > // Note: Linear closures want to be evaluated before > // they are freed with this macro. > macdef > free_end(f) = cloptr_free($UN.castvwtp0(,(f))) > > // HOAS encoding of untyped λ-calculus. > datavtype > term_vtype = > | Var of strptr > | Lam of (strptr, end_vt) > | App of (term_vtype, term_vtype) > > assume > term_vt = term_vtype > > // Frees an abstract syntax tree (all nodes). > fun{} > free_term(t0: term_vt): void = > case+ t0 of > | ~Var(s) => free(s) > | ~Lam(s, f) => (free_term(fs); free_end(f)) > where val fs = f(Var(s)) end > | ~App(t1, t2) => (free_term(t1); free_term(t2)) > > // Pretty-printing. Note that it consumes its input. > // Could not implement it memory-safely otherwise. > fun > fprint_term(out: FILEref, t: term_vt): void = > case+ t of > | ~Var(s) => (fprint_strptr(out, s); free(s)) > | ~Lam(s, f) => () where > val () = ( fprint_string(out, "λ") > ; fprint_strptr(out, s) > ; fprint_string(out, ".") > ) > val fs = f(Var(s)) > val () = (fprint_term(out, fs); free_end(f)) > end > | ~App(f, x) => ( fprint_term(out, f) > ; fprint_string(out, "(") > ; fprint_term(out, x) > ; fprint_string(out, ")") > ) > > (* ***** ***** *) > > // Reduces a term to weak head normal form. > fun{} > reduce(term: term_vt): term_vt = > case+ term of > | ~App(~Lam(s, f), t) => let > val ft = f(t) in (free(s); free_end(f); reduce(ft)) > end > | _ => term > > // The core function. Reduces a term to normal form. > fun > normalize(term: term_vt): term_vt = > let > val red = reduce(term) > in > case+ red of > | ~Lam(arg, f) => let > // Evade scope restriction on linear variable: > val f = $UN.castvwtp0{ptr}(f) > in > Lam( arg > , lam(x) => normalize(fx) where > // Get back to where you once belonged. > val f = $UN.castvwtp0{end_vt}(f) > val fx = f(x) > val () = free_end(f) > end > ) > end > | ~App(h, t) => App(normalize(h), normalize(t)) > | _ (* Var(s) *) => red > end > > (* ***** ***** *) > > implement > main() = 0 where > val x = string0_copy("x") > val y = string0_copy("y") > val id0 = Lam(x, lam(t) => t) > val id1 = Lam(y, lam(t) => t) > val idid = App(id0, id1) > val test = normalize(idid) > val () = (fprint_term(stdout_ref, test); print_newline()) > //val () = free_term(test) > end > > > > -- > You received this message because you are subscribed to the Google Groups > "ats-lang-users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/ats-lang-users/5ba1ad93-98a2-466f-95e1-b02235ec0422o%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/5ba1ad93-98a2-466f-95e1-b02235ec0422o%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp-zayFGkK-A3%3Ddn0jsfzakMaCdYLdoG396P%2BhZ%3DWhDfA%40mail.gmail.com.
