Beginner's question in regard to borrowing ("^")

[JanBeh]

Hi, I'm totally new to Koka and I hope it's okay to ask beginner's questions here?

Checking the type of repeat in the interactive koka compiler, I get:

repeat: forall<e> (n : int, action : () -> e ()) -> e ()

The documentation on repeat says:

fun repeat( ^n : int, action : () -> e types/() ) : e types/()

This made me wonder what the ^ modifier is about. I searched the book and found this:

News:

[…]

• 2021-08-26: Koka v2.2.0 released, improved simplification (by Rashika B), cross-module specialization (Steven Fontanella), and borrowing annotations with improved reuse analysis (Anton Lorenzen).

And:

parameters ::= ( [ parameter { , parameter } ] )
parameter ::= [ borrow ] paramid [ : type ] [ = expr ]

pparameters ::= ( [ pparameter { , pparameter } ] ) (pattern matching parameters)
pparameter ::= [ borrow ] pattern [ : type ] [ = expr ]
 
paramid ::= identifier | wildcard
borrow ::= ^ (not allowed from conparams)

Is ^ a borrowing annotation? And is there some documentation on that existing already?

[anfelor]

Hi @JanBeh, thanks for your question! Yes, the ^ is a borrowing annotation. Unlike in Rust, these annotations only matter for performance and do not influence the types of the program -- so you do not have to worry about the compiler rejecting your program if you get something wrong there. In Koka, borrowing is a technique for improving the performance of a program by omitting reference counting operations. Consider a function like length:

fun length( xs : list<a>)  : int
  match xs
     Cons(x, xx) -> 1 + length(xx)
     Nil -> Nil

Normally, when computing length(xs), Koka would transfer ownership of xs to the length function. However, let us assume that you intend to use xs further after this call. Then Koka will end up incrementing and decrementing the reference count of every element of the list in short order. In this case, it is better to borrow xs by adding the borrow annotation to xs. Then Koka will not perform any reference counting operations -- for length, this is about twice as fast. This is explained in a bit more detail in Counting Immutable Beans and section 3.7 of my master thesis.

[JanBeh]

Thanks for pointing me to these publications! I'll read into them.

I think it would be nice to see the documentation updated at some point in future to explain when it's wise to use these annotations. If I understand right, it's a CPU vs memory trade-off (borrowing can increase memory use).

[anfelor]

Yes, it can be a CPU vs memory trade-off and that's how we analysed it initially. But over time we realized that it's also a consideration of whether the function is in practice called with the last reference to an object or not. If you always pass a shared object as borrowed, there is improved time but no increase in memory usage. But if you always pass a unique object, borrowing increases memory usage and is even worse on time: after your function finishes, a separate free-ing pass is required which could have been done in the function itself (consider how the length function can free the input list as it computes the length if the input list is unique and not borrowed). For this reason, borrowing is opt-in in Koka and not automatic like in Lean.

…

On 1 August 2023 20:32:32 CEST, Jan Behrens ***@***.***> wrote: Thanks for pointing me to these publications! I'll read into them. I think it would be nice to see the documentation updated at some point in future to explain when it's wise to use these annotations. If I understand right, it's a CPU vs memory trade-off (borrowing can increase memory use). -- Reply to this email directly or view it on GitHub: #347 (reply in thread) You are receiving this because you commented. Message ID: ***@***.***>