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/D8790C83-A680-4C08-8358-1CD3139C3AB9%40gmail.com.
