## Stream: lean4

#### Calvin Lee (Jan 26 2021 at 23:36):

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 (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?

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

#### 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

#### 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

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

#### 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

#### Wojciech Nawrocki (Jan 27 2021 at 01:59):

That repo looks private/inaccessible.

#### Calvin Lee (Jan 27 2021 at 03:22):

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

#### 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

#### Calvin Lee (Jan 27 2021 at 03:32):

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

#### 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)

#### 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?

#### 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

#### 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

#### 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

#### 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