ownership / borrow-checking

Stream: lean4

[Adrien Champion]

The end of the Counting Immutable Beans paper mentions the idea of supporting some form of borrow-checking

In order to statically approximate this extended system, we would need to extend our type system with support for some kind of lifetime annotations on return types as featured in Cyclone [Jim et al. 2002] and Rust [Matsakis and Klock 2014].

I think I remember a dev log where this was briefly discussed. Is this idea (still) on the table, and if it is is there additional info on this somewhere, like a paper/blog post/zulip thread?

[Sebastian Ullrich]

You might be interested in @Marc Huisinga's master's thesis to be finished and published in about a month that will discuss ownership and borrowing, though lifetime annotations are not part of it

[Locria Cyber]

How to make some type that cannot be copied? Is that possible in lean?

[Locria Cyber]

Adrien Champion said:

The end of the Counting Immutable Beans paper mentions the idea of supporting some form of borrow-checking

In order to statically approximate this extended system, we would need to extend our type system with support for some kind of lifetime annotations on return types as featured in Cyclone [Jim et al. 2002] and Rust [Matsakis and Klock 2014].

I think I remember a dev log where this was briefly discussed. Is this idea (still) on the table, and if it is is there additional info on this somewhere, like a paper/blog post/zulip thread?

Check out Clean, ATS or Idris 2.

[Adrien Champion]

@Marc Huisinga maybe it would be useful for me to leak the email you sent me so that people like me have a few papers to read until your work is published? Is that okay?

[Alex Keizer]

I would certainly be interested in reading those papers!

[Adrien Champion]

Well the short version is that "uniqueness types" are investigated. That's a concept related to, but different from, linear types

If you'd like to know more about uniqueness types and how it relates to linearity, the recently published "Linearity and Uniqueness: An Entente Cordiale", as well as de Vries' PhD thesis "Making Uniqueness Typing Less Unique" are good places to start.

I found the former in particular to be extremely useful

[Adrien Champion]

Ended up paraphrasing Sebastian

[James Gallicchio]

Sebastian Ullrich said:

You might be interested in Marc Huisinga's master's thesis to be finished and published in about a month that will discuss ownership and borrowing, though lifetime annotations are not part of it

was this ever published? I can't find anything online but I don't really know where I should be looking!

[Sebastian Ullrich]

It now is at https://github.com/mhuisi/Uniq/releases/tag/submission!

[Marc Huisinga]

The official thesis "publication" can also be found here: https://pp.ipd.kit.edu/publication.php?id=huisinga23masterarbeit

[Henrik Böving]

Are there plans on your side to get this integrated into the actual compiler at some point? Or is that something the compiler team will have to deal with? @Marc Huisinga

[Marc Huisinga]

Difficult to say at this point - I work full-time now and definitely need a break from Lean related things for a bit. I wouldn't mind if someone other than me who has some prior experience with substructural type theory takes a stab at it.

There's also some additional theory work left to be done for the type theory to be user-friendly.

[James Gallicchio]

I'm definitely interested in helping push the implementation forward. I might also be able to help on the theory side after this Fall semester (hopefully taking a special topics course on substructural TTs...)