Parallelism outside IO

Stream: lean4

[Geoffrey Irving]

Task seems to be how to do parallel computation inside IO. Is there a purely functional version? In particular, is there Array.map but parallel?

[Henrik Böving]

Sure, task is pure: docs#Task

[Geoffrey Irving]

Whoops, apologies for the hallucination! I saw an example with IO and didn’t read carefully.

[Geoffrey Irving]

Are there lemmas for the semantics of Task, showing that it doesn’t change values? In particular, I don’t see Task.get_pure or a LawfulMonad instance.

[Geoffrey Irving]

I suppose these would need to be axioms, so they’re costly?

[Henrik Böving]

No you could prove stuff like that given that you have a proper Lean representation in the form of a structure instead of an opaque.

[Geoffrey Irving]

Ah, I see: it has transparent reference implementations which are then swapped out. Thanks!

[Henrik Böving]

Geoffrey Irving said:

Whoops, apologies for the hallucination! I saw an example with IO and didn’t read carefully.

Note that you can also have IO with tasks through docs#IO.asTask

[Utensil Song]

Henrik Böving said:

No you could prove stuff like that given that you have a proper Lean representation in the form of a structure instead of an opaque.

Can such a proper Lean representation with proven properties point to the underlying structure/method in C++/Rust etc.? I can only find guides on pointing opaque Lean types to them, which only proves inhabited. Can I expect deeper connections?

[Henrik Böving]

Utensil Song said:

Henrik Böving said:

No you could prove stuff like that given that you have a proper Lean representation in the form of a structure instead of an opaque.

Can such a proper Lean representation with proven properties point to the underlying structure/method in C++/Rust etc.? I can only find guides on pointing opaque Lean types to them, which only proves inhabited. Can I expect deeper connections?

These things are primitives in the run time right now but iirc there was some discussion about generalizing this approach a while back

[Utensil Song]

Yes, I understand that only needing to prove inhabited is a feature to prevent foreign code to compromise the soundness in Lean. But somehow I imagine Lean can also support some parallel implementation, the one in Lean is a conceptual and reasonably efficient implementation, it's both runnable and have proven properties, the other one in C++/Rust etc. to handle real-world subtleties and is sufficiently efficient, and there's native support in Lean to make the correspondence and swap in the implementation where needed, which guarantees the soundness of the algorithmic skeleton which is the major concern of the soundness.

[Utensil Song]

I fail to find the discussion about generalizing this approach, any keywords or pointers?

[Henrik Böving]

https://github.com/leanprover/lean4/pull/2292

[Utensil Song]

Thanks for the pointer, it's illuminating.