borrowing in a high order function creeps internal details into the caller

[kikofernandez]

Hi,

I was trying to use a simple high-order function but I am not sure I got this correctly. The original function is here:

fun filter[a](fn : a -> bool, ps : Par[a]) : Par[a]
  join(ps >> fun (item : a) => if fn(item) then
                                 liftv(item)
                               else
                                 empty[a]()
                               end)
end

However, I need to work with linear a;I have added the linear a type variable to the function and I also also use a borrow block in the internal function to be able to alias the linear item; after the borrow block I expected to get back my normal linear item:

fun filterL[linear a](fn : a -> bool, ps : Par[a]) : Par[a]
  joinL(ps >> fun (item : a)
                var b = false
                borrow item as borrowItem in
                  if fn(borrowItem) then
                    b = true
                  end
                end
                if b then
                  liftvL(item)
                else
                  emptyL[a]()
                end
              end)
end

However, this throws the typing error:

"ParT.enc" (line 69, column 22)
Type 'borrowed linear a' does not match expected type 'linear a'
In expression: 
  fn(borrowItem)

Since it does not allow me to use the function fn without adding the borrowed annotation, an internal detail in the implementation pollutes the top level signature of the function. The end result is:

fun filterL[linear a](fn : borrowed a -> bool, ps : Par[a]) : Par[a]
  joinL(ps >> fun (item : a)
                var b = false
                borrow item as borrowItem in
                  if fn(borrowItem) then
                    b = true
                  end
                end
                if b then
                  liftvL(item)
                else
                  emptyL[a]()
                end
              end)
end

This however does not compile because the type parameter a in ps >> fun (item : a) now needs to have the borrowed annotation as well. Ok, so I update the code to (addition of borrowed in the lambda function):

fun filterL[linear a](fn : borrowed a -> bool, ps : Par[a]) : Par[a]
  joinL(ps >> fun (item : borrowed a)
                if fn(item) then
                  liftvL(item)
                else
                  emptyL[a]()
                end
              end)
end

Now, it complains that liftvL:

"ParT.enc" (line 68, column 19)
Type 'borrowed linear a' does not match expected type 'linear a'

I do understand the message but at this pace, a combinator that wants to work with read and linear modes needs to implement at least three functions:

• one function that takes a linear thing
• one function that takes a linear borrowed thing
• one function that uses the sharable annotation for read

My questions given the reasoning above are:

1. Is there anything that I can do to the simple filter combinator that would give me the semantics that I want?
2. If not, is there anything that we can do to improve re-using code without having to write at least three functions?
3. At another level, I do understand that a function that is given a linear argument that has been borrowed has the linear borrowed annotation. However, for functions, isn't this exposing and tying the internal implementation details to top level types?
4. Can we do some kind of static analysis whenever we have a high-order function that receives a linear type so that it checks if it is possible to use the borrowed thing without having to "creep" the internal implementation to the top level types in the high-order function?

[supercooldave]

Now, it complains that liftvL:

"ParT.enc" (line 68, column 19)
Type 'borrowed linear a' does not match expected type 'linear a'

It seems to me that when you took this step, you took a step to far, because the call to liftvL certainly doesn't borrow its argument. So the error seems to be in the code in the step before that.

Do I need to introduce the borrowed block in order to borrow the linear reference, or can I just pass the linear reference to the function that borrows it?

That is, can I just write if fn(item) ... instead of

var b = false
borrow item as borrowItem in
  if fn(borrowItem) then
    b = true
  end
end

[kikofernandez]

as I understand, either you do the block borrowing or you declare the type variable in the lambda as fun (item : borrowed a). If you do the borrowing block, you have to add the borrow annotation to the fn function (i.e. borrowed a -> bool), which leaks it to the top level function. If you go for the second option, you have already declared that the type variable a is borrowed. This borrowing gets attached to the type variable, instead of being a property that you can add; it leaks the attached borrowed type variable annotation to the top level function.

To make it clear:

fun liftvL[linear t](item: t): Par[t]
  EMBED (Par[t])
    new_par_v(_ctx, #{item}, _enc__type_t);
  END
end

fun filterL[linear a](fn : borrowed a -> bool, ps : Par[a]) : Par[a]
  joinL(ps >> fun (item : borrowed a)
                if fn(item) then
                  liftvL(item)
                else
                  emptyL[a]()
                end
              end)
end

this code from above does not compile. liftvL is only linear but not borrowed, which is the problem with this code. If you solve the problem as the code below:

fun liftvL[linear t](item: borrowed t): Par[t]
  EMBED (Par[t])
    new_par_v(_ctx, #{item}, _enc__type_t);
  END
end

the typechecker now complains that:

"ParT.enc" (line 66, column 9)
Cannot capture expression 'ps' of linear type 'Par[linear a]'
In expression: 
  ps

If you add the consume to the linear ParT:

fun filterL[linear a](fn : borrowed a -> bool, ps : Par[a]) : Par[a]
  joinL((consume ps) >> fun (item : borrowed a)
                          if fn(item) then
                            liftvL(item)
                          else
                            emptyL[a]()
                          end
                        end)
end

the typechecker complains that:

"ParT.enc" (line 66, column 10)
Cannot consume immutable variable 'ps'
In expression: 
  consume ps

I don't think I can get passed this last error.

In any case, this suggests that I need to have mostly three different implementations of any combinator, e.g.liftv:

1. fun liftv[linear t](item: t): Par[t]
2. fun liftvL[linear t](item: borrowed t): Par[t]
3. fun liftvL[sharable t](item: t): Par[t]

[EliasC]

In any case, this suggests that I need to have mostly three different implementations of any combinator

When do you need to implement 1? Unless you are going to save the argument on the heap or send it to a different actor you might as well let it be borrowed.

It does seem however like your problem would be solved if there was a way to abstract over read, active and linear. If a function could promise that it would treat its argument linearly, it should be safe to also pass it something that is active or read (but not something local, as we might pass it between actors!).

Actually, when trying this out it seems like this is already the case!

read class R
end

linear class C
end

fun foo[linear t](x : t) : unit
  ()
end

active class Main
 def main() : unit
   foo(new R)
   foo(new C)
  end
end

I could rewrite your filter function using tons of stubs (and sidestepping some other bugs I ran into):

fun myLiftv[linear t](x : borrowed t) : Par[t]
  EMBED (Par[t]) NULL; END
end

fun myEmpty[linear t]() : Par[t]
  EMBED (Par[t]) NULL; END
end

fun myJoin[linear t](p : borrowed Par[Par[t]]) : Par[t]
  EMBED (Par[t]) NULL; END
end

fun myFilter[linear a](fn : borrowed a -> bool, var ps : Par[a]) : Par[a]
  myJoin((consume ps) >> fun (item : a) => if fn(item) then
                                             myLiftv(item)
                                           else
                                             myEmpty[a]()
                                           end)
end

fun tauto[t](x : borrowed t) : bool
  true
end

read class R
end

linear class C
end

active class Main
 def main() : unit
   var x = new R
   myFilter(tauto[R], myLiftv(x))
 end
end

Note that the main method is calling myFilter with a read value. There are most likely still some issues that needs to be resolved, but finishing this implementation will probably weed out bugs and help us understand how this thing should be designed!