parapluu
borrowing in a high order function creeps internal details into the caller
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
sharableannotation forread
My questions given the reasoning above are:
- Is there anything that I can do to the simple
filtercombinator that would give me the semantics that I want? - If not, is there anything that we can do to improve re-using code without having to write at least three functions?
- At another level, I do understand that a function that is given a linear argument that has been borrowed has the
linear borrowedannotation. However, for functions, isn't this exposing and tying the internal implementation details to top level types? - 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?
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
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:
-
fun liftv[linear t](item: t): Par[t] -
fun liftvL[linear t](item: borrowed t): Par[t] -
fun liftvL[sharable t](item: t): Par[t]
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!
