Do we still need OptionM?

Stream: lean4

[Mario Carneiro]

This came up in a discussion today with some HOL4 folks, who were surprised to see that Option and OptionM are not the same thing in lean 4. As I recall, the issue had to do with type inference in auto-pure situations. Since auto-pure has since been removed, does this mean that these types can be reunified? Or are there some examples that show bad behavior if Option A is a monad?

[Leonardo de Moura]

Another issue was that Lean is not lazy, but we have already adjusted the types of key combinators <|>, *>, etc.
Example:

class OrElse (α : Type u) where
  orElse  : α → (Unit → α) → α

I don't recall other pending issues, but I don't have all the details in my mind right now.
@David Thrane Christiansen If I remember correctly you had some reservations regarding the fusion, but I forgot them, sorry. Could you please remind us?

[Mario Carneiro]

In any case we should put documentation about this issue somewhere (like on OptionM docs) since I expect it to be a recurring question

[David Thrane Christiansen]

My only reservation was that datatypes used as control structures a la Haskell and datatypes used to contain actual data often demand different laziness properties from operations defined on them. It seems quite plausible, however, that it's sufficient to make everything control-structure-like take explicitly thunked expressions in the places where a C programmer would expect short-circuiting, and then arrange for the syntactic overhead to go away via macrology, and then make everything data-manipulation-like be straightforwardly strict. I think this is probably a "try it and see what happens" kind of situation.

[Leonardo de Moura]

OptionM has been deleted, and Monad Option is back.

[Siddhartha Gadgil]

This is especially nice for exposition to a mathematical audience, as Option is (to me at least) the first natural monad. Thanks

[Edward Ayers]

Does this mean we can have Monad Task?

[Gabriel Ebner]

It's of course possible. But there are a couple of gotchas with Monad Task, which I believe is the reason we don't have it as a default instance.

1. Task.bind and co. have a priority argument, with Monad Task you'd always get the default.
2. Every bind creates a new task, which might be a bit expensive.

[Mario Carneiro]

It might be nice to have a TaskBuilder monad which encapsulates the task structure but is only actually launched when you do TaskBuilder.run : TaskBuilder A -> Task A

[Mario Carneiro]

I'm not actually sure where you would want to use Task.map or Task.bind

[Mario Carneiro]

since they seem to be variations on Task.spawn

[Edward Ayers]

Task.map and Task.bind are used in the LSP request handling logic.

[Mac]

Mario Carneiro said:

I'm not actually sure where you would want to use Task.map or Task.bind

since they seem to be variations on Task.spawn

They are much more efficient (c.f. my old task thread).

[Mario Carneiro]

is IO.mapTask different from Task.map?

[Mac]

@Mario Carneiro it executes IO code and is impure (so it can be optimized out). Otherwise, it is the same.

[Mac]

Sorry, that is in relation to Taks.bind/IO.bindTask not Task.map/IO.mapTask.

[Mac]

IO.mapTask is actually a bind not a map.

[Mac]

Task.map is just an ordinary map.

[Mario Carneiro]

I still can't imagine situations where Task.map would be a good idea compared to just determining in advance what the thread is going to return and then launching it (e.g. by passing around (A -> Task R) -> Task R if you don't yet know what R is)

[Mac]

@Mario Carneiro I am pretty sure Task.map is much more efficient than generating closures. Remember, CPS is not efficient in Lean.

[Mario Carneiro]

Task.map is going to be just as bad since you have to build up the closure in the task structure itself

[Mario Carneiro]

Mac said:

Remember, CPS is not efficient in Lean.

citation needed? As long as it turns into join points I don't see a major issue with CPS

[Mac]

Mario Carneiro said:

citation needed? As long as it turns into join points I don't see a major issue with CPS

Leo has directly said this to me. They did benchmarking and for whatever reason (he did not explain why to me) they found the Lean compiler to produce very inefficient code w/ CPS . This is why the Lean monads are not implemented using CPS.

[Mario Carneiro]

You don't want to spawn a thread and then spawn another thread just to join on the first one. The cost of calling a closure should be a lot less than the threading overhead

[Mario Carneiro]

plus there's a big difference between using CPS everywhere and just at points where you would otherwise use Task.map

[Mac]

@Mario Carneiro Task.map does not spawn a new thread. It is an extern function implemented in C. It works like the closure you mentioned but produces more efficient code.

[Mario Carneiro]

The problem is fundamentally more complicated if the thread has already been spawned, which is the case for Task.map

[Mario Carneiro]

because then you have to swap out the code the thread is currently running

[Mac]

@Mario Carneiro yes, but the problem is already solved through Lean's runtime task manager which for Task.map adds a non-thread task (produced from the map closure) as a dependency to the previous task and waits for it on a Task.get/IO.wait.

[Mario Carneiro]

I think the answer to my question then is that you should use Task.map when you want to clone the original task object and map it twice or poll both it and the mapped task later

[Mario Carneiro]

if it's just a linear sequence of steps then you should build up a closure instead to avoid the overhead in the task manager

[Mac]

Mario Carneiro said:

when you want to clone the original task object

There is no cloning going on.

[Mario Carneiro]

I mean something like this:

let a := Task.spawn foo
let b := a.map bar
let c := a.map baz
return (a.get, b.get, c.get)

[Mac]

Mario Carneiro said:

if it's just a linear sequence of steps then you should build up a closure instead to avoid the overhead in the task manager

This is true -- composing functions (e.g., manually or with comp) before a Task.map is better than doing so after (with <$>). However, this is almost always the case with functors (and not thus not particularly special to Task.map).

[Mario Carneiro]

what makes Task.map special is that you can also compose inside the argument to spawn. If in the example we only needed b.get we could instead write it as:

let b := Task.spawn fun _ => bar (foo ())
return b.get

[Mario Carneiro]

that's not a transformation that applies generally to any functor

[Mac]

true, though generally Task.map is used when you already have an arbitrary spawned task, not at spawn.

[Mario Carneiro]

right but why would you be in that situation?

[Mac]

???

[Mac]

For instance, Lake uses Task.map a lot. So does the LSP.

[Mario Carneiro]

the CPS trick is how you can avoid spawning the task in the "arbitrary context" case

[Mac]

Oh, I think understand the confusion. When one uses Task.map it is because one wants to modify an already spawned task running in parallel (or is already finished). That is, you have some set of tasks that you spawned previously to run in parallel and later on you wish to map their values.

[Mario Carneiro]

I assume they mostly fall in the case above though? That is, the task to map is not a "private" one, it is being cloned around

[Mario Carneiro]

e.g. file elaboration tasks or module build tasks

[Mac]

Mario Carneiro said:

I assume they mostly fall in the case above though? That is, the task to map is not a "private" one, it is being cloned around

Yes they likely do fit your previous a, b, c example. Though, again, no cloning is taking place.

[Mario Carneiro]

when I say clone I mean it in the rust sense, i.e. sharing a pointer

[Mario Carneiro]

in lean that usually just means you can't take advantage of unshared opts

[Mario Carneiro]

so the gist of my argument is that unshared Task.map is an antipattern

[Gabriel Ebner]

Mario Carneiro said:

is IO.mapTask different from Task.map?

Yes, Task.map will be cancelled if the refcount reaches zero. While IO.mapTask will always be executed.

[Mac]

Okay, in that case, I guess I am taking issue with Rust's misuse of terminology. That is not what cloning is. The whole point of a clone (pre-Rust) is that the two objects are not pointing to the same data (e.g., JS's clone and Ruby's clone methods).

[Mario Carneiro]

That's not a thing in lean

[Mario Carneiro]

there is no way as far as I know to force two objects to have disjoint object graphs

[Mac]

Mario Carneiro said:

That's not a thing in lean

Lean mutations produce clones (if RC > 1).

[Mario Carneiro]

no, they can still have common data

[Mac]

Which is fine (and is what a (shallow) clone is). Only a deep clone requires no nested sharing.

[Mario Carneiro]

when you clone an RC you get two pointers to the same thing and an incremented refcount

[Mario Carneiro]

same thing happens in C++

[Mac]

That's not a clone, that is just a copy-on-write. JS and Ruby also use reference counters, but their clones generate new objects.

[Mario Carneiro]

that is a "shallow clone" if you want to call it that. The pointer objects themselves are distinct, they just point to the same thing

[Mac]

A shallow clone is one in which one can mutate the clone's (top-level) data without effecting the original. A RC increment does not do that.

[Mac]

https://en.wikipedia.org/wiki/Object_copying

[Mario Carneiro]

cloning is always done lazily in lean, it copies as much as it needs to to do mutations

[Mac]

copying is always done lazily (copy-on-write) in Lean, the term clone has historically always been used to refer to shallow or deep copies (not lazy ones).

[Mac]

e.g., Java, JS, Ruby.

[Mario Carneiro]

I think the disconnect here is a disagreement about what "top level" means. You can change the pointer to point to something else without affecting the original, for example

[Mario Carneiro]

in rust objects are on the stack by default so that's the top level

[Mario Carneiro]

in GC languages everything is behind a heap pointer so that's the top level

[Mac]

A shallow copy/clone is defined as: "In that case a new object B is created, and the fields values of A are copied over to B"

[Mac]

A pointer copy (e.g., a lazy copy or copy-on-write) is something else (not a shallow copy).

[Mario Carneiro]

yup, a pointer object B is created and it's value from A is copied to B

[Mac]

Note in the definition, the "fields values of A" not A itself.

[Mario Carneiro]

well a pointer is a simple struct with one field

[Mac]

No it is not, it is not a struct at all.

[Mario Carneiro]

or in lean's case, a union between a pointer and a u64

[Mac]

both of which are not structs but simple (non-aggregate) data values, from whom the notion of copying/cloning doesn't even exist.

[Mario Carneiro]

a value exists in memory on the stack or in a register, so you can certainly copy it elsewhere

[Mac]

https://en.wikipedia.org/wiki/Cloning_(programming)

[Mac]

The article literally separates what you are talking about (a primitive copy) from the notion of cloning.

[Mario Carneiro]

in languages like C++ and Rust where objects on the stack can have destructors, the concept of cloning certainly applies to them

[Mario Carneiro]

pointers are just the trivial case where cloning is a memcopy

[Mac]

True, it does. Never did I say on object's location (stack, heap, disk, etc.) is relevant to the definition.

[Mac]

What is relevant is the object's structure.

[Mac]

Pointers a primitive values, thus they cannot be accurately described as being cloned.

[Mac]

The object pointed to by a pointer though can.

[Mario Carneiro]

An RC pointer in fact has a nontrivial destructor and clone operation

[Mac]

Yes, the pointer object is clonable.

[Mario Carneiro]

the clone operation makes a copy of the pointer value but also increments the underlying refcount

[Mac]

But that is not the same as cloning the object it points to.

[Mac]

Mario Carneiro said:

the clone operation makes a copy of the pointer value but also increments the underlying refcount

That is not a proper clone in the first place.

[Mac]

That is a C++ abuse of the clone function to do pointer magic.

[Mario Carneiro]

...

[Mac]

C++ feature abuse being very common in C++ (and, after a while, the abuse generally becomes standard practice, as with shared pointers). That is, the original idea behind the clone in C++ was to produce shallow/deep clones (hence the name), but eventually people realized it could be used to conveniently manage shared pointers, so it eventually acquired that use as well (even though that does not fit the meaning of the term).

[Mac]

Again, the term clone has a clear common definition (as noted on Wikipedia). RC increments do not meet this definition.

[Mac]

Literally the definition from Wikipedia is: "The process of actually making another exact replica of the object instead of just its reference is called cloning" (emphasis mine)

[Mac]

Obviously, this is just a debate over semantics, and there is nothing wrong with different people and groups having different terminology. My point is simply my definition of cloning is not an outlier and is the historically common notion.

[Mac]

However, as you pointed out, that distinction is now blurred in many places (e.g., C++ and Rust), thus creating a terminology schism.