HOAS encoding of lambda calculus with linear types

[August Alm]

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

[artyom.s...@gmail.com]

Hi August,

This is interesting stuff you’re working on. :)

On 7 Jun 2020, at 15:19, August Alm <augu...@gmail.com> wrote:



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.

--
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 ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5ba1ad93-98a2-466f-95e1-b02235ec0422o%40googlegroups.com.

[August Alm]

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.

Hi August,

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.

[artyom.s...@gmail.com]

On 7 Jun 2020, at 22:31, August Alm <augu...@gmail.com> 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?

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/173cc0ed-d0bd-4973-9690-5f5b5fcb03b1o%40googlegroups.com.

[August Alm]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/173cc0ed-d0bd-4973-9690-5f5b5fcb03b1o%40googlegroups.com.

[Hongwei Xi]

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!

--
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 ats-lang-user...@googlegroups.com.

[August Alm]

Hi, thanks for answering!

I have a semi-educated guess as to how the various ATS-closure

functions are translated into C. What I was fishing for was rather if

the details/internals can be exposed from within ATS. E.g., the

heuristic

datatype cloref = CLOREF of (fp, env) // env is non-linear
datavtype cloptr = CLOPTR of (fp, env) // env is non-linear

suggests that, possibly, the only difference between `cloptr` and

`cloref` is a `view`; informally:

cloptr = (cloptr_v | cloref) .

If that was the case then it would be possible to take out the cloref,

do stuff a cloptr is not ordinarily allowed to do, and then fold it back

with the linear proof term.

Reference-counting seems the way to go. Thanks. (I haven't looked

at Temptory but eagerly await Xanadu!)

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.

[August Alm]

I'm very close to getting this to work. =) My code typechecks but does

not compile yet. I'm getting the error:

implicit declaration of function ‘atspre_eq_strptr_strptr

It seems a template is not implemented. How should [strptr] terms best

be tested for equality?

Cheers!

[Hongwei Xi]

eq_strptr_strptr is implemented in prelude/DATS/strptr.dats

The error message is from the C compiler, stating that the function

atspre_eq_strptr_strptr is used in the generated code before it is declared.

Don't know why.

You can try to add the following lines to the beginning of your code:

%{^

extern

atstype_bool

atspre_eq_strptr_strptr(atstype_strptr, atstype_strptr);

%}

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/2d9b0a30-1456-424c-84b9-b4b766f73569o%40googlegroups.com.

[Hongwei Xi]

Or you can use

compare_strptr_strptr

which is defined in C and should be okay.

[August Alm]

My code typechecks but compilation segfaults without explanation. I don't

know how to figure out why. I'd be very grateful if someone is interested in

this project and willing to look at what might be wrong. Complete code here:

https://github.com/August-Alm/Lambda-Calculus-by-Linear-HOAS

Best wishes and happy midsummer everyone!

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/2d9b0a30-1456-424c-84b9-b4b766f73569o%40googlegroups.com.

[August Alm]

It seems that it is patsopt and not gcc that segfaults during compilation. Where do I start debugging? With runtime crashes I have some ideas (gdb, valgrind) but segfault during compilation has never happened to me before and I can't seem to find anything relevant on the web.

[Hongwei Xi]

I took a look.

This error is caused by the compiler not being able to

infer some template arguments.

The following declaration says that refcnt is co-variant:

absvtype
refcnt_vt0p(a: vt0ype+) = ptr

But refcnt is actually in-variant. So you need to remove the '+':

absvtype
refcnt_vt0p(a: vt0ype) = ptr

Unfortunately, your code makes use of some features that are not

supported. For instance, the use of flat arrays are not properly supported

in ATS2:

vtypedef
ctxarr = @[bind][CTXCAP]
typedef
ctxidx = [i: nat | i < CTXCAP] uint(i)
vtypedef
ctxstruct = @{arr = ctxarr, cur = ctxidx}

These things can be fixed. What cannot be easily fixed is that linear closures

(lincloptr) cannot be duplicated. You have a function find_in_ctx, which requires that

the found term to be duplicated (so that the copy is returned while the original one is

still kept in the context).

I don't yet know if there is a way to circumvent this issue.

--Hongwei

On Thu, Jun 18, 2020 at 3:13 PM August Alm <augu...@gmail.com> wrote:

It seems that it is patsopt and not gcc that segfaults during compilation. Where do I start debugging? With runtime crashes I have some ideas (gdb, valgrind) but segfault during compilation has never happened to me before and I can't seem to find anything relevant on the web.

--
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 ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3ba508d9-316e-4fbb-b4ae-a0bb7ed17420o%40googlegroups.com.

[Hongwei Xi]

One has to modify the ATS2 compiler in order to support duplication of

linear closures (lincloptr). I have kept a note of this. Maybe we could support it

in ATS3. This is a non-trivial task, and I have to contemplate on it for some time.

I implemented a normalization function for pure lambda-terms in ATS3 (not ATS2):

https://github.com/xanadu-lang/xinterp/blob/master/TEST/xatslib_githwxi/test-2020-06-18.dats

This version can be thought of using higher-order abstract syntax if we simply treat

TM2lam( TM1lam(x1, t1), env )

as a shorthand for:

TM2lam(lam t2 => evaluate(t1, cons((x1, t2), env)))

If we use ref-counted versions for term1 and term2 in the code, then we should be able to get an

implementation that is completely memory-clean.

[August Alm]

Wow, many thanks for the heads-up and effort you put into this. Now I have an excuse to start dabbling with ATS3.

You're amazing, Hongwei!

You received this message because you are subscribed to a topic in the Google Groups "ats-lang-users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ats-lang-users/s4zuDhJ4BB8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoxSRJSWLURddML7%2B5C4Sz462W6E%3DnjzM2EWH9pOEH3qg%40mail.gmail.com.

[Hongwei Xi]

Hi August,

I managed to get a version that is memory-clean:

https://github.com/githwxi/ATS-Temptory/blob/master/docgen/CodeBook/RECIPE/LambdaCal/LambdaCal_rc.dats

And Valgrind confirms:

==1475== Memcheck, a memory error detector
==1475== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==1475== Using Valgrind-3.11.0 and LibVEX; rerun with -h for copyright info
==1475== Command: ./LambdaCal_rc_dats
==1475==
K = TM1lam(x; TM1lam(y; TM1var(x)))
S = TM1lam(x; TM1lam(y; TM1lam(z; TM1app(TM1app(TM1var(x); TM1var(z)); TM1app(TM1var(y); TM1var(z))))))
SKK_nf = TM1lam(z; TM1var(z))
App_2_3 = TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1app(TM1var(f); TM1var(x)))))))))))))))))
==1475==
==1475== HEAP SUMMARY:
==1475==     in use at exit: 0 bytes in 0 blocks
==1475==   total heap usage: 753 allocs, 753 frees, 15,384 bytes allocated
==1475==
==1475== All heap blocks were freed -- no leaks are possible
==1475==
==1475== For counts of detected and suppressed errors, rerun with: -v
==1475== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)

#################################################

I have to say that the current support for ref-counted datatypes in ATS/Temptory is not user-friendly.

I would not suggest using it for something more serious at this stage. Once I get ATS3 to a point where

other people can use it, I will find time to beef up the support for ref-counted datatypes, which can be a

very useful feature!

Cheers!

Hongwei

PS: Thanks for bringing up this programming challenge :)

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAAHDgBFY_j0Ai%3DcSO9zZ%3DW2HtoGkgHeBvSGL_3e0x3gD2wUWYg%40mail.gmail.com.

[August Alm]

Nice! Sort of semi-HOAS; using hand-rolled closures instead of the built-ins.

I think the way reference counting is handled isn't too bad. Very explicit, but that

is the ATS philosophy, I guess, and I'm used to it by now. =) The overloaded

symbols (bang ! and so on) you introduced went along way.

(I've been in the countryside, without internet connection, so haven't answered.)

The idea of using ATS as a target for small functional DSLs is appealing to me.

Cheers!

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3ba508d9-316e-4fbb-b4ae-a0bb7ed17420o%40googlegroups.com.

--
You received this message because you are subscribed to a topic in the Google Groups "ats-lang-users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ats-lang-users/s4zuDhJ4BB8/unsubscribe.

To unsubscribe from this group and all its topics, send an email to ats-lan...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoxSRJSWLURddML7%2B5C4Sz462W6E%3DnjzM2EWH9pOEH3qg%40mail.gmail.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 ats-lan...@googlegroups.com.

[Hongwei Xi]

A big inconvenient thing with a ref-counted value right now is that it is not treated as a left-value.

In order to do call-by-reference with such a value, one needs to take out the pointer inside it explicitly.

>>The idea of using ATS as a target for small functional DSLs is appealing to me

With ref-counted values, it becomes quite straightforward to implement memory-clean programs. In an

embedded setting, we need to go one step further, that is, being able to compute a bound for the maximal

amount of memory needed for the execution of a program. Once this bound is obtained, we can statically

allocate a chunk of memory of adequate size; and calls to malloc/free during the execution only manage

this chunk of statically allocated memory.

--Hongwei

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/f51deee7-eb34-4467-8de8-15cf2da80f8do%40googlegroups.com.