Zulip Chat Archive

Stream: lean4

Topic: monad performance


view this post on Zulip Calvin Lee (Jan 26 2021 at 23:36):

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?

view this post on Zulip Calvin Lee (Jan 27 2021 at 01:13):

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

view this post on Zulip Wojciech Nawrocki (Jan 27 2021 at 01:22):

@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.

view this post on Zulip Calvin Lee (Jan 27 2021 at 01:26):

@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

view this post on Zulip Calvin Lee (Jan 27 2021 at 01:33):

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

view this post on Zulip Wojciech Nawrocki (Jan 27 2021 at 01:39):

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.

view this post on Zulip Calvin Lee (Jan 27 2021 at 01:50):

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

view this post on Zulip Wojciech Nawrocki (Jan 27 2021 at 01:59):

That repo looks private/inaccessible.

view this post on Zulip Calvin Lee (Jan 27 2021 at 03:22):

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

view this post on Zulip Mario Carneiro (Jan 27 2021 at 03:28):

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

view this post on Zulip Calvin Lee (Jan 27 2021 at 03:32):

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

view this post on Zulip Calvin Lee (Jan 27 2021 at 03:39):

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)

view this post on Zulip Calvin Lee (Jan 27 2021 at 17:40):

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?

view this post on Zulip Calvin Lee (Jan 27 2021 at 17:51):

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

view this post on Zulip Mario Carneiro (Jan 27 2021 at 17:59):

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

view this post on Zulip Calvin Lee (Jan 27 2021 at 18:05):

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

view this post on Zulip Calvin Lee (Jan 28 2021 at 20:00):

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


Last updated: May 07 2021 at 13:21 UTC