Proposal: Linear / Explicitly Destroyed Types

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!

14 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.

Hi,

Linear types seem super useful, having quickly read through the proposal.

Has there been any update or indication that Mojo is moving towards adopting the proposal?

Best regards,

They are implemented into Mojo, although not widely used.

1 Like

Thank you for the update.

Is there any documentation on how to use them?

Or maybe you could point me to a piece of core that uses so I can take a look?

1 Like

@explicit_destroy

2 Likes

From an ui i’m working on:

Yes, please check out theses three lineartype structs :up_arrow::
StartedMeasurement
CompletedMeasurement
Border

Border gets created by an startedmeasurement and have the origin of it!
so the border can be consumed with end_border only if the startedmeasurement is live.
(before startedmeasurement^.end_measurement() which returns an completedmeasurement)

This is a great workflow and it makes this very specific logic quite user friendly.

  • Vscode says that the lineartype is live, remind to use .end_measurement
  • remind that the border have to be consumed (draw)
  • remind that its startedmeasurement has to be live to do that

Also, only a completemeasurement can be consumed to move the cursor for new drawing,
lineartype allow us to make sure that border is included into the measurement,
and when the cursor is moved, we know that it comes from an startedmeasurement.

Also completedmeasurement can only be consumed ONCE to move the cursor:
either after measured rectangle or below rectangle.
This sort of says: no going left, no going up, (no draw on already drawed stuff)!

What is really interesting too, is that if there is an Border instance,
there is an startedmeasurement (can only init from there)!
And can only init an completedmeasurement from an startedmeasurement.

So for users, the api sort of get progressively wider:

ui -> start_measuring       -> ^.end_measuring -> ^.move_cursor
      |-> start_border
          |> ^stop_border()
1 Like

In addition, lineartype have to be explicitly destroyed in a specific manner,
but if needed, they can also be only initializable in a specific manner ! :+1:
(for example, by consuming another lineartype, (a becomes b))

Things can also gets really useful when they have no __copyinit__,
and move-only (__moveinit__):

You can start measuring and hand an startedmeasurement to a widget,
let it draw whatever it needs, and it can consume it or return the completedmeasurement.
(separation of concern)

So i’d say that LinearType makes some workflows possible and manageable,
and can help make sure all steps are done in an specific order :input_latin_letters:

By assigning the Origin of an lineartype into the parameter of another lineartype,
it is possible to help make sure the second one can only be consumed before the first.
(doing it after would be an error like: trying to use an uninitialized value)

lineartype are awesome, hope this helps !

2 Likes