Program Main without IO

Stream: new members

[Simon Daniel]

Hi,
im writing a library where i want to prevent Users from performing IO in programs, except through my own API. My idea was to provide a 'custom' main method which gets called from within an actual main that is located in the library. Is there some way of forward declaring a function, or supply this class instance in an other file after the main?

--library
class CustomMain where
  main:(List String) -> UInt32 -- no IO here

def main (args : List String) [CustomMain]: IO UInt32 := do --no valid main without CustomMain instance
  return CustomMain.main args

--other file
instance: CustomMain where
  main args := 0

[Niels Voss]

Unfortunately no, there is no way to forward declare functions. This is because forward declarations would allow you to use mutual recursion, which would in turn let you prove False.

That being said, maybe there's another way to do it using more advanced features in Lean, like mutual or implementedBy, or even defining a custom command with metaprogramming, but I am not aware of them. You would need to ask someone else.

Do you trust the user of your library not to run code they shouldn't? Because what you could do is make a function def run [CustomMain] : IO UInt32 and then expect users to write def main := run somewhere after declaring an instance of CustomMain

[Niels Voss]

You could even in theory make a command with metaprogramming so that you could use run_main (args : List String) : UInit32 := 0 without having to worry about interacting with main directly, though ofc a user that deliberately wants to run impure programs could.

[Simon Daniel]

im currently using a run function like you suggested. I guess having to write outdef main := run is just a minor inconvenience.
It would be cool however to prevent the user from running impure code, instead of having to rely on him correctly calling into the library.
A metaprogramming solution also seems nice to hide the main from the user!

[Niels Voss]

The problem is that there's no way to tell a file A to do something from a file B unless A imports B. If your library code is in file A, then making B.lean can't really affect A, because A basically has no idea that B.lean even exists. At most, maybe you could do some trick to try to search folders for files like B.lean and dynamically resolve imports, but that's probably more trouble than it's worth.

I do not know if it is possible to attain "inversion of control" where the library contains main and you write a plugin to hook onto that. Maybe you could achieve it by having your end user specify an "entrypoint" in the lakefile? This does sound like more trouble than it's worth

[Eric Wieser]

You could write a linter in your library that rejects any definition of main other than def main := run

[Eric Wieser]

(linters get to run every time downstream code adds a definition)

[Simon Daniel]

seems like linters could do the job, from looking at examples from batteries it should be a Std.Tactic.Linter?

@[env_linter] def checkMain : Std.Tactic.Lint.Linter

with env_linter it seems to only run the linter on a #lint command, is that correct?