Both reference counting and deep copying sound like they could be workarounds I could be happy with. What I meant was simply that, ordinarily, if I find myself wanting to duplicate a linear variable I can hack it with casts or even FFI:ing to C. However, in this case all terms should (in the end) be constructed by a parser and I have a hard time imagining how to automate such dirty, manual hacks into a sensible parser algorithm. Will have to think a bit more, and do some reading.
Den måndag 8 juni 2020 kl. 06:52:46 UTC+2 skrev [email protected]: > > > On 7 Jun 2020, at 22:31, August Alm <[email protected] <javascript:>> > wrote: > > > Thanks for commenting, Artyom! > > Yeah, I tried the !-modality. I even tried the ?! and the `dataget` > castfn. Can't get it to work. > As you may guess I'm also hoping to implement a parser of > lambda-expressions to abstract > syntax terms. For that I think I need to be able to write, e.g., something > like > > val twice = Lam(s, lam(t) => App(t, t)) > > > Yes, I see the problem now. I think you will have to use reference > counting or deep copying... but I guess these are the manual workarounds > you mentioned? > > [lam(t) => App(t, t)] is not a valid [!term_vt -<cloptr1> term_vt]. Of > course, if I wanted to > duplicate like that I could achievie it by manual work-arounds, I think, > but it would be hard > to automate during parsing. (It would show up parsing `lam x.x(x)` ..) > > > What do you mean by automating during parsing? > > Much of the point of > the HOAS-route is to make parsing easy. No need for de Bruijn. That and > speed, assuming > ATS is fast at closure conversions. > > Den söndag 7 juni 2020 kl. 21:08:02 UTC+2 skrev [email protected]: >> >> Hi August, >> >> This is interesting stuff you’re working on. :) >> >> On 7 Jun 2020, at 15:19, 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. >> >> >> Could you try (!term_vt) -<cloptr> term_vt instead? That means that the >> closure function will preserve the argument passed to it, and that it may >> use the argument many times. >> >> Also in your code below for printing, you could use the same modality so >> the printer doesn’t discard the AST! >> >> A more concrete question is: How exactly is the type [a -<cloptr> b] >> defined? >> >> >> I think that it will correspond to a C function with an extra pointer >> argument for holding the environment (i.e. all the captured variables). >> >> 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. >> >> >> There was some documentation on this here: >> >> http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c1220.html >> >> This probably doesn’t answer all of your questions, though. >> >> >> 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] <javascript:>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/ats-lang-users/173cc0ed-d0bd-4973-9690-5f5b5fcb03b1o%40googlegroups.com > > <https://groups.google.com/d/msgid/ats-lang-users/173cc0ed-d0bd-4973-9690-5f5b5fcb03b1o%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/ccc8c42f-1788-4a8e-a33f-3c7fdc94a1dco%40googlegroups.com.
