Something similar to sorry but for IO

Stream: Lean for Scientists and Engineers 2024

[Eric Taucher]

For those new to functional programming and liking the concept of sorry in that it leaves the proof unfinished without a parade of errors, when using IO with do notation for similar one can use

def io_do_nothing : IO Unit :=
  return ()

example usage:

def some_io (inPath : String) : IO Unit := do
   io_do_nothing

A common usage for such is when first creating the first few lines of code and needing to check the import statements and such. This short circuits the code so that one can concentrate on just those issues and not also having unneeded errors in the mix which greatly complicates learning.

Note that Unittype ref is often new to those learning functional programming so better to learn it now than suffer for years with a hole in the thought processes as I did.

I am not sure if the Lean community has a prefered or more idiomatic way to do this with IO; part of the reason to note this is that it shows how easy it is to get around some problems with a little knowledge.

Enjoy.

---

Bonus question for the curious

What is the value of the unit type being returned?

Answer:

()

---

F# uses the same value - https://learn.microsoft.com/en-us/dotnet/fsharp/language-reference/unit-type

[Eric Wieser]

Another good option is panic! "TODO(me): actually do this"

[Eric Wieser]

This also works for things like def myReadFile : IO String, which your io_do_nothing does not work for