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)) [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)` ..) 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] <javascript:>> > 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] <javascript:>. > 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/173cc0ed-d0bd-4973-9690-5f5b5fcb03b1o%40googlegroups.com.
