monad performance

Stream: lean4

[Calvin Lee]

Is the identity monad strict?
Instead of using the identity monad as a base for my transformer I used IO (to debug) and my computation finished instantly...
I'm thinking this is because IO is strict. Is Id not?

[Calvin Lee]

Ok, I eliminated the identity monad and performance is the same (poor). Is there anyway to enforce strictness without using IO?

[Wojciech Nawrocki]

@Calvin Lee can you elaborate on what you are trying to do? Lean is a strict language, so unlike for example in Haskell, most expressions are strictly evaluated by default.

[Calvin Lee]

@Wojciech Nawrocki
Yeah, I can say exactly what I'm doing.
So for one of my courses I'm writing a Sudoku solver (in Lean 4). To do this I wrote the LogicT monad transformer (with some restrictions due to problems with universes/polymorphism) in Lean and wrote a pretty simple backtracking algorithm using it.
When using the Logic = LogicT Id monad, it is very slow, and will not even be able to solve an empty 3x3 board. However, LogicT IO is very quick and will evaluate almost instantly

[Calvin Lee]

I could post my code here, but I've been hesitant to crowd it with asking for help too much since this channel is devoted to lean4 developments
But I was also told to post here instead of in #new members

[Wojciech Nawrocki]

I'm not familiar with that paper, so it is hard to say exactly what is going on. By all means do post your code though, this channel is for Lean 4 users after all.

[Calvin Lee]

Ok, so if I replace Logic here with LogicT IO it gets a ton faster https://git.sr.ht/~pounce/Sudoku/tree/master/item/Sudoku/Solve.lean#L81
The logic transformer itself is here, and is continuation based https://git.sr.ht/~pounce/Sudoku/tree/master/item/Sudoku/Logic.lean#L10

[Wojciech Nawrocki]

That repo looks private/inaccessible.

[Calvin Lee]

@Wojciech Nawrocki whoops the settings are wrong, they're right now

[Mario Carneiro]

Because lean uses in-place mutation a lot, you should ensure that your monad combinators are using their values linearly. That seems the most likely culprit when it comes to continuation monads

[Calvin Lee]

Hmm, but wouldn't this create a performance issue with both IO and Id?

[Calvin Lee]

Logic definitely isn't linear (it duplicates continuations on mplus), but this is necessary for transparent backtracking
But I don't think that's the main issue since it's duplicated for IO as well (since LogicT IO is still backtracking)

[Calvin Lee]

So the only thing I'm thinking so far, is that IO is defined with the IO.RealWorld constant that prevents "reordering" of operations.
Does this really affect compilation, or is it just there for future use?

[Calvin Lee]

Yes! This seems like the case!
I replaced IO as a base for my monad transformers with StateM Unit and it runs very quickly

[Mario Carneiro]

You might also get the same result with ReaderM Unit; there is a big difference between A and Unit -> A in order of evaluation, so that seems like the key difference

[Calvin Lee]

Yeah, it might be too eager in some places perhaps. I may try experimenting with thunks to see if I can get rid of the performance issue with Id
The LogicT paper was originally written for Haskell with a few extensions.... so I'm sure there are some issues that I don't yet understand about using it in Lean

[Calvin Lee]

Mario Carneiro said:

You might also get the same result with ReaderM Unit; there is a big difference between A and Unit -> A in order of evaluation, so that seems like the key difference

Yeah this is it spot on
StateM Unit is the same type as Thunk (what I just realized) so all I needed was lazyness and this gave it to me