Linear types in Lean

Stream: lean4

[Alex Keizer]

What is the community's opinion on having linear / substructural types in Lean?
(To be clear, this is not a feature request. I'm considering doing a PhD on this topic, but it would very likely require kernel modifications, thus buy-in from the core team & community)

I'm mostly thinking about the benefits to Lean as a programming language. Looking at Linear Haskell, an effort to add linear types to Haskell, they cite two reasons:

• Linearity enables optimizations like in-place mutation. IIUC Lean does do in-place mutation when the reference count of a value is 1, but it's currently easy to introduce a performance regression. A type like Array might be a good candidate for being linear (or at least, affine), with an explicit copy method, so that it's very clear when things are done in-place, and when a copy is required

• Safe Monadic Programming. Currently, a value of IO ... might be accidentally copied, causing the associated effect to happen twice. Linear types would help prevent this (again, with some explicit copy method when the double effect is actually desirable).

Of course, Lean is also a proof assistant. Presumably, the addition of linearity to the kernel would translate to benefits to, e.g., the recent effort to port Iris developments to Lean.

The idea would be to make this all as gradual, and opt-in, as possible, where currently written code and proofs keeps working classically, but there is some way to opt-in to linearity.

[Sebastian Ullrich]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/ownership.20.2F.20borrow-checking/near/324859952!

[Sebastian Ullrich]

Alex Keizer said:

• Linearity enables optimizations like in-place mutation

In the general case you'll want Clean-like uniqueness types for this, not linear types. Marc's thesis will expand on that.

Safe Monadic Programming. Currently, a value of IO ... might be accidentally copied, causing the associated effect to happen twice. Linear ypes would help prevent this (again, with some explicit copy method when the double effect is actually desirable).

I don't understand this point, copying an IO value does nothing until you actually execute them, which is always an explicit action in Lean.

Of course, Lean is also a proof assistant. Presumably, the addition of linearity to the kernel would translate to benefits to, e.g., the recent effort to port Iris developments to Lean.

Lean's type theory is relatively conservative, there are no plans to introduce multiplicity into the kernel.

[James Gallicchio]

(Leo had mentioned at some point wanting to add multiplicity annotations, right? But with a checker that is outside the kernel?)

[Sebastian Ullrich]

Yes, that is roughly Marc's approach