Substructural types

Stream: lean4

[Leni Aniva]

Will Lean ever have support for them, e.g. linear types, affine types, quantified types, etc.?

[Niels Voss]

Not an answer, but I've seen them mentioned here: #lean4 > Semantics of IO don't match provable properties? and #lean4 > FFI, Rust and mutability

[Niels Voss]

To me at least, it seems fairly unlikely that Lean's core type theory will expand to include linear and affine types, because that would require a deep change to the kernel and it probably wouldn't make sense from a cost/benefit perspective. But, it might be possible to implement linear and affine types from within Lean via clever use of opaque, Monads, and possibly additional type checkers.

[Niels Voss]

I guess the question is, what is it that you want to do with substructural types? To me at least, linear types don't feel useful when working with pure Lean structures, since everything is functional and there's no need to restrict the amount of times something is referenced. The scenarios in which I could imagine Linear Types being useful seem to mostly involve interacting with something with behavior defined by external code, like:

• Making sure that a single Array stays at reference count at most 1 so that it doesn't get accidentally copied and cause performance issues
• Having a version of IO with properties you can prove about it (so that there are no "time traveling tokens" as seen in the thread above)
• Implementing RAII for things like file handles
• FFI with languages using linear types, like Rust

It's not clear that the same solution would be best for all of these (like maybe a monad would be best for semantically valid IO but not for interfacing with Rust?)

[Henrik Böving]

This topic has been explored to some degree in: https://pp.ipd.kit.edu/uploads/publikationen/huisinga23masterarbeit.pdf

[Leni Aniva]

Niels Voss said:

I guess the question is, what is it that you want to do with substructural types? To me at least, linear types don't feel useful when working with pure Lean structures, since everything is functional and there's no need to restrict the amount of times something is referenced. The scenarios in which I could imagine Linear Types being useful seem to mostly involve interacting with something with behavior defined by external code, like:

• Making sure that a single Array stays at reference count at most 1 so that it doesn't get accidentally copied and cause performance issues
• Having a version of IO with properties you can prove about it (so that there are no "time traveling tokens" as seen in the thread above)
• Implementing RAII for things like file handles
• FFI with languages using linear types, like Rust

It's not clear that the same solution would be best for all of these (like maybe a monad would be best for semantically valid IO but not for interfacing with Rust?)

Having linear types would make it easier to reason on programs. e.g. qubits cannot be shared.

[Alok Singh]

Niels Voss said:

I guess the question is, what is it that you want to do with substructural types? To me at least, linear types don't feel useful when working with pure Lean structures, since everything is functional and there's no need to restrict the amount of times something is referenced. The scenarios in which I could imagine Linear Types being useful seem to mostly involve interacting with something with behavior defined by external code, like:

• Making sure that a single Array stays at reference count at most 1 so that it doesn't get accidentally copied and cause performance issues
• Having a version of IO with properties you can prove about it (so that there are no "time traveling tokens" as seen in the thread above)
• Implementing RAII for things like file handles
• FFI with languages using linear types, like Rust

It's not clear that the same solution would be best for all of these (like maybe a monad would be best for semantically valid IO but not for interfacing with Rust?)

just the first use case for ref counts is worth it to me