I completely agree that this is "a level lower" than Effekt. I've used it for a while as part of a research project, and I've had significant gripes with it, mostly due to the complete lack of explicit lifetime polymorphism (which, while verbose, can be genuinely useful at times), and because its equivalent of contexts cannot be called upon with a contextOf-like function at all, so its contexts can never materialize as real values that you pass around.

This proposal addresses both those gripes, and it seems rather good!

It's good to note, btw, that Effekt's handlers aren't completely covered by this proposal since their stacks are multi-shot, while (as far as I understand), the proposed stacks aren't (and Kotlin's Continuations aren't either)
You can use reflection or bytecode manipulation to add clone methods to compiler-generated continuations (which I have done), but that's far from being a supported use case. This means that we sadly don't get monad comprehensions or non-determinism handlers, but alas.

Ah, yes, thanks for catching that! The stacks library can only support single-shot continuations, unlike Effekt's multi-shot continuations.

@RossTate are you able to add a comparison with effekt in the design documents? Specifically because it is more or less "prior work", which can help understand what Kotlin's direction would be and how it may influence the decisions.

There are a lot of research languages exploring this space, and each of these languages is made up of a unique combination of novel and existing features, so open-ended comparisons would be overwhelming. But I am happy to answer specific questions about specific languages.

Good question! Yes, those work just fine. In your example, the inferred type argument for let/with is Bar_{bar}. There isn't even any need to update their signatures.

The recover and merge functions do indeed work as you say. I should note that it's not quite "first-class" though. That is, while function parameters can themselves be functions that take local parameters, you cannot have something like Iterable<(local Foo) -> Unit>. It's like the difference between higher-kinded polymorphism and first-class/impredicative polymorphism.

Huh, I'll have to think more about that. Is there a reason why that's the case?
Is this allowed?

val merge: (local (local Raise<Int>.() -> Int)) -> Int = ...

I'm guessing it is?

Searching up higher-kinded polymorphism vs impredicative polymorphism, it sounds like function types are special-cased to allow parameterisation inside their types (in this case, lifetime parameters), but other types are not. Is that your point here?

So is it simply that function types are unique, but if I had e.g. fun interface Arrow<T, R> { operator fun invoke(t: T): R } then I can't use Arrow<(local Raise<Int>.() -> Int), Int>, but I can do so if I had typealias Arrow<T, R> = (T) -> R?

Also, FWIW, it's not such a huge limitation that Iterable<(local Foo) -> Unit> is disallowed, since interface Consumer<T> { operator fun invoke(local t: T) } is isomorphic, and would be allowed, right? I'm guessing they won't be allowed to be fun interfaces though?
If so, then hey, at least we get the spiffy lambda syntax when calling something like merge, and if we really need to store local-taking functions as data, we can always use such a SAM interface workaround.

I'm trying to keep things decidable. The issue with allowing something like local Raise<Int>.() -> Nothing to be used as a type argument is that it means inference/outference needs to be able to reliably determine that something has that type, even when there's no informative context. So if someone writes val x : Any = listOf { raise(5) }, the type checker would have to automatically determine out of nowhere that that raise could be the method of a local Raise<Int> implicit receiver, and therefore this type checks if the argument to listOf is local Raise<Int>.() -> Nothing. (Note that Raise doesn't even need to be imported; it's full name just needs to be accessible for this to be valid.)

So first-class types are those that can be used as type arguments, and it's important for them to be synthesizable. On the other hand, when we invoke a method, we can check that arguments against the method's signature. That makes it possible to decidably support signatures with more expressive types than what we can use as type arguments. As you note, when you need to get around this gap, you can make an explicit (functional) class/interface (though an alias isn't enough) as an intermediary.

Yes, this is expressible, and in fact the stack primitives can implement the single-shot semantics for this.

As for your numbered questions:

1. Explicit locality parameters (as opposed to local parameters of functions) are (currently) unconstrained by default. If you need it to be constrained by the this lifetime so that, e.g., you can know it is accessible by methods, then you can do local_{this} lifetime. (Since all methods execute within the this lifetime by default, the constraint will make this a sublocality of lifetime, so you furthermore know the methods are executing within the lifetime locality.)
2. Interestingly, I think these end up being equivalent due to the fact that the local lifetime is itself inferred. But I think the second more directly matches your informal description of the operation.
3. You don't need the bound (and it should go on local rather than the name) because explicit localities are (currently) unconstrained by default.
4. It does not; i.e. the local locality does not have to be within l. (If you did want that, you could use fun_{l} to require local to be a sublocality of l.)

Good suggestion. I've added some thoughts on this: https://github.com/Kotlin/KEEP/blob/main/notes/0007-local-lifetimes.md#type-checker-feedback

Making a class local restricts the lifetime of the this reference to have the this lifetime rather than the global lifetime. That can break existing code. We also know of a critical case where we do not want that behavior: https://github.com/Kotlin/KEEP/blob/main/notes/0007-local-lifetimes.md#strings

Good catch! I updated the document. Thanks!

Yep! The former would restrict the elements in the array to be used only locally, but not the array itself. (For example, you could upcast it to an Array<*> and get its length after foo returns.) The latter restricts the array and its elements to be used only locally.

Ah, moving the bounds to where would be really helpful.

I can't use @ because it's used to disambiguate between thises, which I reuse for the this lifetime. (Consider local inner classes of local classes.) But I can use some operator. And I realized I can drop the braces (in an older version, I needed to be able to specify a list of localities in the restriction, but now it's sufficient to simply repeatedly restrict the lifetime with each locality).

The team has identified a number of issues with the syntax for contracts in general, so we're trying to gradually move away from that syntax.

So, trying out the viable operators available left-to-right on my keyboard, here's how the syntax could look like on a complex example:

internal local class TransformingSequence<T, out R> constructor(
    private val sequence: Sequence<T>#this,
    private val transformer: (T) ->#this R
) : Sequence<R> {
    override fun iterator(): Iterator<R>#this = object : Iterator<R> {
        val iterator = sequence.iterator()
        override fun next(): R {
            return transformer(iterator.next())
        }
        override fun hasNext(): Boolean {
            return iterator.hasNext()
        }
    }

    internal fun <E> flatten(
        local# iterator: (R) -> Iterator<E>#iterator
    ): Sequence<E>#this#iterator {
        return FlatteningSequence<T, R, E>(sequence, transformer, iterator)
    }
}

internal local class TransformingSequence<T, out R> constructor(
    private val sequence: Sequence<T>$this,
    private val transformer: (T) ->$this R
) : Sequence<R> {
    override fun iterator(): Iterator<R>$this = object : Iterator<R> {
        val iterator = sequence.iterator()
        override fun next(): R {
            return transformer(iterator.next())
        }
        override fun hasNext(): Boolean {
            return iterator.hasNext()
        }
    }

    internal fun <E> flatten(
        local$ iterator: (R) -> Iterator<E>$iterator
    ): Sequence<E>$this$iterator {
        return FlatteningSequence<T, R, E>(sequence, transformer, iterator)
    }
}

internal local class TransformingSequence<T, out R> constructor(
    private val sequence: Sequence<T>%this,
    private val transformer: (T) ->%this R
) : Sequence<R> {
    override fun iterator(): Iterator<R>%this = object : Iterator<R> {
        val iterator = sequence.iterator()
        override fun next(): R {
            return transformer(iterator.next())
        }
        override fun hasNext(): Boolean {
            return iterator.hasNext()
        }
    }

    internal fun <E> flatten(
        local% iterator: (R) -> Iterator<E>%iterator
    ): Sequence<E>%this%iterator {
        return FlatteningSequence<T, R, E>(sequence, transformer, iterator)
    }
}

internal local class TransformingSequence<T, out R> constructor(
    private val sequence: Sequence<T>^this,
    private val transformer: (T) ->^this R
) : Sequence<R> {
    override fun iterator(): Iterator<R>^this = object : Iterator<R> {
        val iterator = sequence.iterator()
        override fun next(): R {
            return transformer(iterator.next())
        }
        override fun hasNext(): Boolean {
            return iterator.hasNext()
        }
    }

    internal fun <E> flatten(
        local^ iterator: (R) -> Iterator<E>^iterator
    ): Sequence<E>^this^iterator {
        return FlatteningSequence<T, R, E>(sequence, transformer, iterator)
    }
}

internal local class TransformingSequence<T, out R> constructor(
    private val sequence: Sequence<T>*this,
    private val transformer: (T) ->*this R
) : Sequence<R> {
    override fun iterator(): Iterator<R>*this = object : Iterator<R> {
        val iterator = sequence.iterator()
        override fun next(): R {
            return transformer(iterator.next())
        }
        override fun hasNext(): Boolean {
            return iterator.hasNext()
        }
    }

    internal fun <E> flatten(
        local* iterator: (R) -> Iterator<E>*iterator
    ): Sequence<E>*this*iterator {
        return FlatteningSequence<T, R, E>(sequence, transformer, iterator)
    }
}

Thoughts?

Where is '? 🙃

The team has identified a number of issues with the syntax for contracts in general, so we're trying to gradually move away from that syntax.

Yes that makes sense - my idea was more about writing a list of constraints, with whatever syntax works best, as opposed to the generic parameter approach.

Of your examples, I think I like ^ the best, except that Sequence<E>^this^iterator is rather hard to read - unless it has the obvious meaning of "the lifetime is bound by both this and iterator", which I think it actually does?

Is using a keyword an option? E.g. private val sequence: Sequence<T> in this?

unless it has the obvious meaning of "the lifetime is bound by both this and iterator", which I think it actually does?

It does 😊

Is using a keyword an option?

Probably. But I think an operator would be preferred if we could find a suitable one.

Probably. But I think an operator would be preferred if we could find a suitable one.

Personally I like the keyword because of the spacing, which makes it easier to read (IMO). You can of course do the same with the operator but it looks kind of odd (helpful, I know).

Ah, yes it is. Sorry, I've added a note explicitly stating that now. Thanks for catching this!

I totally get this concern. While I have made a conscious effort to make local lifetimes have a nice path for gradual adoption, it's of course hard to assess just how real that path is.

If it helps to have a familiar example, I took half an hour to localize the immutable arrays library. You can preview the hypothetical update here. (Since in reality much of the code is generated, I only updated the generic generated code instead of updating the generating code.) In summary, the changes were to

• make 20 parameters local,
• remove (all) 6 occurrences of crossinline,
• and add 1 _{local} and 6 _{this} lifetime restrictions.

You might notice that I did not make ImmutableArray into a local class. That's because I didn't see a particular use for it. Because ImmutableArray is generic, it can already hold elements with local lifetimes. Because ImmutableArray object is just data, making it local doesn't enable any more functionality. And because the length of ImmutableArrays tends to be dynamic, we wouldn't typically be able to allocate it on the stack anyways. So the only benefit I could think of would be to let others artificially restrict the lifetime of an ImmutableArray in order to get the type-checker to help them ensure it doesn't escape, which didn't seem particularly likely to be helpful, and which certainly isn't necessary for the library to work nicely with local lifetimes. (I only made Array into a local class in order to support stack-allocating varargs, since those do typically have a statically known length.)

Regardless, I agree with your point that a tool could likely automate most localization updates, and that it would be a good idea to provide such a tool if this feature were to ship. (A complementary option would be to provide some way to indicate that certain imported libraries have not been localized and to treat them optimistically with respect to localities.)

Nice, that's less invasive than I was expecting.

One concern I still have with the example is that library authors would need to know when they need to or should apply local. For example, I do not think it would be obvious (and wasn't to me) that I should add local to the Array, Iterable, and Sequence receivers unless there was some hinting in the IDE.

Regardless, I agree with your point that a tool could likely automate most localization updates, and that it would be a good idea to provide such a tool if this feature were to ship. (A complementary option would be to provide some way to indicate that certain imported libraries have not been localized and to treat them optimistically with respect to localities.)

I'm not sure how possible it is, but it could be interesting to handle locality inference like smart casts: code in the same compilation unit has its locality inferred (i.e. using the function body), which can then be made explicit in the signature to make it part of the API contract.

Yes

I think so, but after we first incorporate a round of feedback from this discussion and from after the talk.

Yes, but for immutable collection types that's guaranteed not to change. But I haven't actually seen any implementations that do something with the collection.

Immutable collections implementations probably wouldn't be local, so if you downcast it, you'll then be free to leak it wherever you want!

That wouldn't quite work...yet. Right now, although all objects of a non-local class, say Foo, are always created with a global lifetime, it's not the case that Foo_{restricted} is a subtype of Foo_{global}. That way, if Foo were to be made into a local class, it's guaranteed it wouldn't break any existing code using the Foo type. But, we could extend this design to enable one to declare a class/interface to be global, making it permanently a non-local class/interface, and consequently making it safe to improve subtyping accordingly. I hadn't thought of a case where this would actually be useful, but this example with immutable collections could be one.

I meant if you knew about some ImmutableListImpl which is explicitly not a local class, then would you be able to downcast to it?
Another example is can I downcast a local Any to a String for instance? I'd imagine that would work

This really is good motivation to have non-local interfaces, although you can get close ish:

interface Foo {
  val globalize: Foo_{global}
}

Remember that, to support gradual adoption, just because something is not local now does not mean it is not expected to become local eventually. So, if we were at add the global extension I mentioned, and if we were to explicitly mark ImmutableListImpl or String as global, then a type-tag test (i.e. is ImmutableListImpl or is String) would be able to drop the restriction on the lifetime.

P.S. The _{global} in your Foo signature is redundant.

I did, but there are two considerations. One is backwards compatibility; making everything local by default would break a lot of existing code (and, even though most parameters can be made local in the standard library, it can often require correspondingly restricting lifetimes in return types). The other is that, in looking at libraries (and especially the standard library), we're biasing our examination towards code where local will be more common (and, in the case of the standard library, used in more advanced ways).

I want to push back a little on the backwards compatibility concern. Any non-local class cannot have a lifetime, so all of those classes would not suffer at all here.
The question is then about interfaces and local classes. How often is Kotlin code leaking interfaces? I don't know if var x: SomeInterface is that common. Returning an interface is maybe a bit more common, but still relatively rare.

Maybe a happy middle ground would be to have some @LocalByDefault annotation. It then could be also useable on types directly, so one can do typealias LIterator<T> = @LocalByDefault Iterator<T>.

Another idea could be to have a module-wide or per-file toggle, similar to the return value checker.

I would also like to see some kind of global flag, this would also allow seeing more what kind of API design comes up when you specify lifetimes from the start, rather than when you add them retroactively to existing APIs that fit them.

It seems that you can only use local v: Blah if Blah is a local class or an interface, so it's illegal to write local v: Int, but I might be wrong on that.

Interesting, I think I had assumed the same without realizing it. But then what about

local val foo: LocalClass
val bar: NonLocalClass_{foo)

?

I meant to say local and the _{-} syntax, but I forgot midway thru...

In other words, it seems like interfaces and local classes are the only types that can have an intrinsic lifetime. Lifetime parameters seem like they can be added to anything, though

1. Correct
2. Correct
3. Correct
4. Correct: the declaration should be local class Baz(val c: Int_{this}).
5. Correct, assuming you use the corrected declaration in (4) above.

The lifetime of any type can by restricted. This is important for T_{...} to work even when T is a type parameter (which occasionally arises in the standard library, and is heavily relied upon for the stacks design). Whether a class is local or not has no effect on its subtyping behavior (which leaves room for the class to be made local without breaking code). Making a class local imposes restrictions upon its implementation, particularly by making this be restricted to the this lifetime. (Interfaces have no implementation, which is why there is no notion of a local interface.)

Interfaces have no implementation, which is why there is no notion of a local interface.

That's a question I've been meaning to ask! What about default methods in interfaces?

interface Foo {
  fun returnSelf(): Foo = this
}

This currently compiles, but presumably would be illegal now?

What to do about default methods with non-local use of this is admittedly on my to-do list. If I were to pick right now based on intuition, I would reject this. That would technically be a breaking change, but I suspect that instances of this would be rare enough that it would worth shipping the "right" default and forcing such interfaces to incorporate the restricted lifetime into the signature.

This somewhat reminds me of Scala's Separation Checking, which is built on a similar-ish system to lifetimes

Good question! Local lifetimes were explicitly designed to incorporate lifetimes without typestate. Typestate certainly has applications, but it unfortunately causes a lot more complications for both code and typing algorithms. How to support typestateful features (like "consumes") in a Kotlin-esque manner is still under investigation.

Lifetimes already allow us to have DSLs for automatic resource cleanup, so I don't think a language construct or anything needs to be added here.
The simplest case is giving access to one resource:

fun <R> withFile(path: Path, block: (local File) -> R): R = nativeOpenFile(path).use { block(it) }

The file can never leak outside the block, so using the file is completely safe!
You can take this a step further with something like ResourceScope from Arrow. I won't describe its implementation details here, but simply, it has an onRelease function that registers a finalizer to run at the end of the scope. With lifetimes, it can be made a lot safer:

interface ResourceScope<local outer> { // outer is a nice candidate to be a member lifetime
  fun onRelease(finalizer: () ->_{outer} Unit)
}

inline fun <R> resourceScope(block: local ResourceScope<local>.() -> R): R = ...

context(local scope: ResourceScope<*>)
fun openFile(path: Path): File_{scope} = nativeOpenFile(path).also { file -> scope.onRelease { file.close() } }

openFile is just as safe as withFile. The returned file is only usable within the apt resourceScope block, so all file actions will run before the finalizer, and resourceScope guarantees that the finalizer will run!

From my experience, different people have different expectations of when the lifetime of a local variable ends. The two most common are when it is no longer used, or when the function call completes. But even these have ambiguities. If a variable is only used in one case of an if, does its lifetime end when we enter the other side or only when the entire if finishes? Alternatively, if a function calls another call in a tail position (in a setting where we know we're not worried about maintaining stack traces), is the current call "completed" by the tail call? Interestingly, my algorithm doesn't actually determine "the" lifetime of an object/operation; it just determines constraints that these lifetimes must satisfy and ensures all the constraints are compatible with each other. So, because ambiguity is kind of inherent in lifetimes, I still recommend that programs be explicit about when important things like cleanup should happen.

I don't see why a value class can't have a lifetime? A very simple case is a value class that wraps a normal class:

value class MyFlow(val flow: Flow_{this})

Lifetime doesn't need to be tied to identity.

I see the intuition. Essentially, if we can arbitrarily copy an object, then does its lifetime really matter? In a design where lifetimes were shallow, then not really. But in this design, a lifetime can be deeply integrated into the signature of a class, including into the types of its fields and methods. So a copy of a limited-lifetime object can still need to have a limited lifetime. That said, if we were to add a way to mark certain classes as explicitly global, I suspect that many value classes (and data classes) would be marked as global, since in many cases they are "deeply" copyable.

That makes sense. I was getting a bit ahead of myself and thinking of the deep immutability semantics that have been proposed for value classes. It seems like they would be prime candidates to be global by default.

Also, side note, will the generated copy fun for data classes become fun copy(...): Self_{this}?

Reified types are here because of type erasure, so I think you'll still need inline functions for them.

avoiding allocation lambda objects (not just stack allocating them)

I believe stack allocation means avoiding allocating them entirely. The JVM doesn't really let you "stack allocate" beyond simply placing values on the stack. The stacks library is a clear case where avoiding lambda allocations seems important.

I do wonder how this behaves with binary compatibility guarantees and such, but I guess we'll see!

Ah, you're right! I made a mistake. It would still be the case that only inline functions can have reified type parameters.

I agree that more needs to be said here. Stacks is a good example of a use case (once you get beyond the technical details, they effectively let you have suspend APIs that compose nicely with each other). There's also some performance benefits here (avoiding allocations).

Thanks for the feedback! Admittedly, these design notes were written with the talk in mind, and I need to go back and make them more self-contained. I'll let y'all know what that's done!

Yes. You might appreciate this paper: https://cs.uwaterloo.ca/~yizhou/papers/abseff-popl2019.pdf