Monadic graph algorithms

Stream: lean4

[Nicolas Rouquette]

The folks working on the Yatima language provide an interesting source of Lean4 programming patterns. Their monadic formulation of strongly-connected components for directed graphs caught my attention. Since their algorithm is currently tied to Lean4's symbols as vertices, I decided it would be a fun exercise to parameterize this nifty library. The result is described in this ticket: https://github.com/yatima-inc/yatima-lang/issues/88

The refactored code is here: https://github.com/NicolasRouquette/YatimaGraphLib

I hope that the WIP https://github.com/leanprover/functional_programming_in_lean will eventually explain the Lean4 programming wizardry involved in this code. Even though I don't understand it completely, this refactoring exercise was really fun with the help of the vscode support and the lean toolchain (lake).

Independently of whether this parameterization makes sense for Yatima or not, I would like to find out how to improve the code.
For example, several definitions require different constraints on the type parameter:

structure dfsState (α) [Ord α] where
  visited : RBMap α Bool compare

def getInfo {α} [Ord α] [ToString α] (v : α) : (sccM α) NodeInfo :=  ...

def scc? {α} [Ord α] [BEq α] [ToString α] (g : Graph α) : Except String $ List $ (List α) :=...

Is there a way to reduce the duplication of such constraints?

• Nicolas.

[Kyle Miller]

One thing is that you don't need {α} since Lean automatically includes one-variable names as implicit arguments. You can also use the variable [Ord α] command, so then every time you make reference to α in the arguments of a function the Ord argument will be included too.

[Nicolas Rouquette]

Thanks @Kyle Miller ! I've applied your suggestions!

[Gabriel Ebner]

since Lean automatically includes one-variable names as implicit arguments

BTW, this was changed recently to be more general. Feel free to use more informative names:

def getInfo [Ord Alpha] : Alpha → Alpha → Ordering := compare