Howdy all, here’s the proposal for Linear / Explicitly Destroyed Types (plus GitHub issue).
TL;DR: We’d upgrade the type system to be able to express “explicitly destroyed types”; a struct (or trait) definition could use an e.g. @explicit_destroy("Use some_method(a, b, c) to destroy")
annotation to inform the use when they haven’t disposed the object correctly.
This solves a bunch of problems, for example:
- Remind the user when
Coroutine
objects go out of scope, and that they should instead await
them (and take ownership of the coroutine’s result).
- A (hypothetical)
t: Thread
object should never go out of scope, the user should only destroy it via t^.join()
or t^.abandon()
.
- Require the user call e.g.
spaceship.land(landing_zone)
instead of just letting the ship go out of scope.
For more examples, check out the proposal! Also take a look at this talk at the 2024 LLVM conference where I talked a bit about these concepts.
I previously implemented this feature in Vale, and I’ve implemented a proof-of-concept to verify this is possible in the Mojo compiler (proposal’s steps 1-7), but some open questions still remain:
- How might this do at scale?
- What should we call these things, that are temporarily named
@explicit_destroy
, destroy
, ImplicitlyDestructible
, etc.
- Are the benefits (better type system, less errors) worth the costs (different traits for some generic functions).
None of this is final, so I’d love to get everyone’s feedback! Feel free to leave comments here or in the GitHub issue. Cheers!
13 Likes
Hi, your talk at LLVM devmtg was very nice.
Have you considered how Linear types would work with context managers -3. Data model — Python 3.13.1 documentation - for resource acquisition? Technically they should dovetail together:
@explict_destroy("Call rollback() or commit()")
struct Transaction:
...
fn rollback(owned self):
# some operation
destroy self
fn commit(owned self):
# some operation
destroy self
# Assume __enter__ is already implemented
fn __exit__(owned self):
# assume success
self^.commit()
You just never mention if there are gotchas around usage like this.
2 Likes
I think by default, if the user doesn’t implement a __exit__
, then we should show an error if they use it with a with
statement (which then of course doesn’t know how to destroy it).
Your solution looks pretty reasonable, if someone actually does want to enable with
statements for their explicitly destroyed type. And it means the user has a choice: when they have a Transaction
object, they can:
- Use it like a regular linear type, and call
commit()
or rollback()
explicitly at the end of the scope.
- Use it with a
with
statement, to default to commit()
(in your example).
I wonder: can the user still rollback()
it in the middle of the with
? Like:
with db.new_transaction() as t:
...
t^.rollback()
...
# End of scope, doesn't call t^.commit(). Possible?
…though now that I think of it, that’s a more general question about with
statements, and not necessarily linear types. I’ll look into this a bit, and any thoughts here would be appreciated!
1 Like
That is an interesting consideration. Normally it would be unnecessary to explicitly call clean-up functions if you’re inside a context manager, you raise an exception instead which would be passed to exit, I imagine for Mojo it would look something like:
...
fn __exit__(owned self, error: Error | None = None) -> Bool:
if error is not None:
# ...
self^.rollback()
return True # Propagate error
self^.commit()
return False
I know union types are not supported yet, this is just to illustrate.
You know, I believe linear types really work well with context managers. I’ve just remembered an instance when I was still getting started with SQLAlchelmy where I assumed the context manager handled commit automatically for the basic session when it didn’t. Explicitly destroyed type would have made such false assumptions a compile error. wow.
Edit: It probably wouldn’t have been so simple as in this sqlachelmy case calling commit is only necessary if changes have been made within the context.