> On 7 Jun 2020, at 22:31, August Alm <[email protected]> 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. > > -- > 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. -- 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/5CBED973-BA27-4519-89D4-9942094DD0B5%40gmail.com.
