Lambdas that use linear resources

Skip to first unread message

Oct 4, 2021, 11:19:34 PM10/4/21
to ats-lang-users
Hi all,

I'm trying to understand higher-order programming in ATS better, but I keep running into errors when my lambdas use linear resources.  Here's a small example that doesn't compile:

    extern fn {a,b:vt@ype} map_vt {n:nat} {e:eff} (
      l: !list_vt(a, n), f: !(!a) -<cloptr,e> b
    ):<!wrt,e> list_vt(b, n)

    fn prefix_sums {n:nat} (l: !list_vt(int, n)): list_vt(int, n) =
        var acc: int = 0
        val f = lam(x: !int): int =<cloptr,!wrt> (acc := acc + x; acc)
        val result = map_vt(l, f)
        val () = cloptr_free{void}($UNSAFE.castvwtp0(f))
      in result end

Compiling this gives an error saying that proof search for the view at 'acc' failed.

So, my questions are:
1. Why is this failing to compile, and how can I fix it? (Ideally without threading through an 'env' view parameter to all the closures.)
2. Is there a way to avoid the UNSAFE cast?
3. Would there be a way to do it with a stack allocated closure?




Oct 7, 2021, 7:07:09 AM10/7/21
to ats-lang-users
First, let me say that lambdas are one part of ATS that I'm not super experienced in myself.  However, if you haven't been there already, I'd recommend reading the chapters on linear & stack-allocated closures in the " A Tutorial on Programming Features in ATS " here & here respectively.

Now, to answer your questions:
  1. (Why is it failing to compile?)  Your lambda doesn't see "acc", the easiest way to solve this is to pass "acc" to your lambda via reference (aka use the "&" operator in the function argument.)
    1. Side note: You don't need to say "x: !int", because "int" is not a linear type, you can leave it "x: int" without the "!" part.
  2. (Is it possible to avoid the UNSAFE cast?)  The page I linked to you above about linear closure says that yes, there is a way, but that it's cumbersome to use.  That's all I know, I've not seen any example code.
  3. (Can I do this with a stack allocated closure?)  Yes, and in fact it's probably better to use a stack allocated closure in this instance because you are not keeping the closure around to use with multiple functions.  Were you storing this closure in a struct for example, then a linear closure should be used.
Let me know if you have any other questions, and good luck!
Reply all
Reply to author
0 new messages