Proving stuff about programs using monads

Stream: Is there code for X?

[Thomas Vigouroux]

In a project I have, I'd like to rewrite a purely functionnal program without monads to use mondas (mainly to allow for logging).

My problem is that in the current version, I can prove things about the behavior of my function (because it does not have monads). With monads I can't find a way to prove the correctness of my function, as it depends on the behavior of my monad.

As an example, let's take https://leanprover.github.io/functional_programming_in_lean/monads/arithmetic.html.

And let's say that my goal is to prove that if my evaluation function returns a number, then I am sure that no division by zero happened.

[Thomas Vigouroux]

Is there a easy way to do that ?

[Thomas Vigouroux]

Put differently, I'd like to have a function the logs something when it is called, and I'd very much like that to be done without too much hassle in terms of types.

[Kim Morrison]

def f (n : Nat) := dbg_trace s!"{n}"; n*n

#eval f (f 2)

[Thomas Vigouroux]

Oh god so it's that simple :sad:

[Thomas Vigouroux]

Thank you soooo much
This was bugging me for days !

[Kim Morrison]

As the name suggests, this is for debugging only, not production code. :-)

[Thomas Vigouroux]

I think it is fine :wink:
The changes in the code to have proper logging seem a little too much for me, and I am not familiar enough (yet) with functionnal programming to get it right

[Yaël Dillies]

Oooh, is dbg standing for "debug"? TIL

[Eric Wieser]

If you want to add non-debug logging, you could write your function to be Monad-polymorphic using a HasLog typeclass; for proving, you use a monad that has a no-op log, but for execution you use a monad that uses IO.println

[Thomas Vigouroux]

Indeed

[Thomas Vigouroux]

I'll try to do that later on then !

[Eric Wieser]

This also lets you pick a middle ground where for proving you use a state monad that collects the log messages, so that you can also prove it logs if you really care!

[Eric Wieser]

Yaël Dillies said:

Oooh, is dbg standing for "debug"? TIL

Is it missing a docstring that explains that?