structured concurrency

Stream: lean4

[Iocta]

I see there are some concurrency and I/O primitives in Lean4. I haven't digested it yet but I think asTask is sorta like the go statement of go statement considered harmful, and Task is a structured primitive?

[Mario Carneiro]

I think it is like the go statement but I disagree with the argument that such a primitive should not be exposed to the language. (I don't think that blogger's views are shared by the majority of language designers.) It is possible to build a scoped thread model on top of the task primitives if you want, but as long as they can be safely and purely exposed I don't see any reason to avoid giving users access to the thread spawn function. (Plus asTask isn't even a pure function so that is even less applicable.)

[Iocta]

I don't think that blogger's views are shared by the majority of language designers.

It's a relatively newish idea, but Kotlin, Swift, and Java are moving that way or have already.

[Mario Carneiro]

Actually, looking at the lean 4 code a bit more I think there are actually two kinds of tasks represented by the type Task A. One is pure tasks created by Task.mk. The only thing you can do with these tasks is map/bind them and block on them with Task.get, and they are terminated when the task handle is dropped. So the comparison to go is not correct in this case, because they do not outlive the function

[Mario Carneiro]

The second kind of task is IO tasks created by asTask and manipulated with the other IO task operations like wait and cancel. These do outlive their caller and so act like go, but it is not difficult to set up a scoped thread approach for them as mentioned

[Iocta]

(Julia's talking implementation too)

[Mario Carneiro]

I don't think any of those examples have nurseries as their only thread primitive, which is what the blogger is talking about

[Mario Carneiro]

I rather like scoped threads but I don't think they should be the only option

[Sebastian Ullrich]

Tasks are just standard futures available in virtually any stdlib, not structured concurrency

[Mario Carneiro]

The version of scoped threads I'm familiar with from rust is crossbeam::scope

[Mario Carneiro]

I want to emphasize that this is a library implemented outside the stdlib

[Iocta]

that seems a bit backwards to me. The normal case should be structured, so you need to go out of your way, like adding unstructured or at least an annoyingly long name like IO._spawn_task_without_supervision to do the less-disciplined thing. All the old languages have to support old code, and it's not easy to refactor an unsupervised-task application into structured format ("callbacks all the way down") so they provide easy ways to keep existing code running. But new languages can make their normal primitive safer and easier to use.

Fwiw there are some nice testimonials which I treat as anecdotal evidence, a particularly choice one about the Trio structured concurrency library is from Donald Stufft who runs the Python Package Index https://pypi.org

I've written Linehaul in uh
Twisted, gevent, and asyncio
and now trio
trio is the first one I feel like I can actually follow the code without my head hurting
(and that includes the fact the trio one is also way more configurable and robust, and has retries and everything that none of the others did)

[Mario Carneiro]

Do you actually have an API in mind?

[Mario Carneiro]

The designs from imperative languages with exceptions don't transfer especially well

[Mario Carneiro]

In particular, "unstructured" futures aren't unsafe in the type safety sense

[Mario Carneiro]

and the problems with catching exceptions and cancellation in trio don't seem to apply

[Iocta]

I don't have a particular design in mind, but looking around at implementations in haskell, rust, swift, etc may yield some

[Iocta]

here's an implementation of happy eyeballs in scala ZIO

[Mario Carneiro]

the ZIO example doesn't use scoped threads, it seems to be all combinators

[Mario Carneiro]

which again don't have to be part of lean core

[Mario Carneiro]

the Haskell ki library seems to be a better fit for scoped threads in pure functional languages like lean, but I'm not sure the Task primitive is low level enough to support it - one needs to be able to store type erased tasks (i.e. ThreadId in haskell) and be able to cancel tasks using the type erased handle

[Mario Carneiro]

I haven't tested but you might be able to cheat by casting a Task A to Task Unit and hopefully IO.cancel doesn't care that the types don't match

[Mac]

It is worth mentioning at this point that Lean's compiled C code uses goto? XD

[Mac]

My point here is about this statement:

Iocta said:

that seems a bit backwards to me. The normal case should be structured, so you need to go out of your way, like adding unstructured or at least an annoyingly long name like IO._spawn_task_without_supervision to do the less-disciplined thing.

I would argue it is generally the other way around. A language primitive should be primitive. It should reflect the actual bare-metal implementation as closely as possible. Higher order structures should come later. However, I do agree with your approach of using naming conventions to highlight more primitive operations (Haskell, for example, does this by appending hashtags to its primitive operations).

It is also worth noting that Lean is not a structured imperative language unlike many of the other languages (like Kotlin, Swift, Java, and even Julia to an extent) you mentioned, thus concepts do not necessarily carry over so easily.