Add Control.Monad.ST.Linear and implement IO.Linear in terms of it

[shlevy]

No description provided.

[shlevy]

This PR is a draft because of this. Options, assuming this PR is otherwise wanted:

1. Accept the breaking change
2. Keep IO a newtype (but derive instances and relevant functions via coercing from ST still)
3. Fix GHC and wait

[aspiwack]

Sorry I didn't come back to you earlier. I think that in regard of the discussion with @treeowl below and the fact that a linear ST monad is always going to be pretty niche, I say let's not break compatibility here.

It doesn't matter that IO is an instance of ST. And there's a potential future where they aren't. Let's honor that by IO and ST both be independent newtypes.

[shlevy]

@aspiwack You said this about IO, I assume you believe it of ST as well?

[aspiwack]

Yes, I don't see why ST or IO would make a difference here.

[aspiwack]

Hi @shlevy ,

I'll look at this more next week. In the meantime, can I ask you what use-case you imagine for a linear ST monad?

It's been my assumption, so far, that a linear ST isn't particularly useful because ST is mostly about shared mutations, and linear types tend to preclude sharing and already support mutation in non-monadic code.

[treeowl]

In addition to the fact that ST seems like it should be unnecessary, the way GHC pretends that ST and IO are the same is semantically suspect, and leads to subtle problems (mostly relating to demand analysis). Maybe not the best conflation for research?

[shlevy]

The main motivation is for pure mocks that are backed by ST and involve cleanup (e.g. a mock of a filesystem where you want to be able to “close” the file).

[shlevy]

So you’d write code polymorphic over s and one implementation that uses the actual filesystem only works when s ~ RealWorld but they all involve linear resource management.

[treeowl]

But why use ST for that purpose?

[aspiwack]

@treeowl

In addition to the fact that ST seems like it should be unnecessary, the way GHC pretends that ST and IO are the same is semantically suspect, and leads to subtle problems (mostly relating to demand analysis). Maybe not the best conflation for research?

I didn't know about that. Do you have some documentation on the issue?

[treeowl]

@treeowl

In addition to the fact that ST seems like it should be unnecessary, the way GHC pretends that ST and IO are the same is semantically suspect, and leads to subtle problems (mostly relating to demand analysis). Maybe not the best conflation for research?

I didn't know about that. Do you have some documentation on the issue?

Not quite off the top of my head. GHC has gotten more conservative to make IO exception behavior more predictable, at the cost of less precise demand analysis for ST. The essential issue is pretty simple: IO is fundamentally lazy, while ST is fundamentally strict. In ST,

m >>= const _|_ = _|_

However, in IO,

m >>= const _|_ ≥ _|_

In particular, m may have observable side effects, which users tend to expect to occur even if an error happens later.

Another example: For any m in ST, fix (m >>) = _|_. But in IO, the same expression could represent, say, the main loop of a program.

GHC needs special cases to deal with this aspect of IO, and those end up affecting ST too, even though they really shouldn't—an ST action that ends up in bottom doesn't have any observable effects (aside from unsafe trickery, of course).

[shlevy]

But why use ST for that purpose?

So I can use STRefs to mock out the state.