Associated types in classes

Stream: lean4

[Tage Johansson]

I wonder if there is any way to write Rust like associated types in Lean classes?

Imagine I have a class for monadic file system operations MonadFS and a class for file read operations MonadFileRead.
Then I could write the file system class like this:

class MonadFS (m : Type → Type _) where
  -- Some file system related methods like:
  ls : (dir : FilePath := ".") → m (Array IO.FS.DirEntry)
  ...
  -- Type of monad for reading files.
  mf : Type → Type _
  monadInst : Monad mf
  readInst : MonadFileRead mf
  -- Perform file reading on a specific file.
  readFile : FilePath → mf α → m α

The problem is that I want Monad m and MonadFileRead m to be instances and not explicit members of the class. The user of the class should not need to refer to monadInst and readInst when using the mf monad.

I could make mf as an outParam, and it works, but the class head gets really large and I will have to repeat it in every subclass of MonadFS.

The problem is how to specify that mf should have some instances. In Rust like syntax an associated type could be written:

        type MF: Monad + MonadFileRead;

But I don't know if this is possible in Lean?

[Kyle Miller]

I haven't run this, but in principle I believe this might implement what you're asking:

class MonadFS (m : Type → Type _) where
  -- Some file system related methods like:
  ls : (dir : FilePath := ".") → m (Array IO.FS.DirEntry)
  ...
  -- Type of monad for reading files.
  mf : Type → Type _
  [monadInst : Monad mf]
  [readInst : MonadFileRead mf]
  -- Perform file reading on a specific file.
  readFile : FilePath → mf α → m α

attribute [instance] MonadFS.monadInst MonadFS.readInst

The square brackets in the MonadFS declaration may or may not be correct; what these do is make it so that when you construct a MonadFS then it will try to use typeclass inference to fill in monadInst and readInst automatically given mf.

Setting the instance attributes makes it so that you can use MonadFS.mf m as a monad, for example. (Assuming I got the implicit/explicit arguments correct here of the top of my head.)

[Eric Wieser]

I think outParam is probably the answer here in general

[Eric Wieser]

class MonadFS (m : Type → Type _) (mf : outParam $ (Type → Type _)) [Monad mf] [MonadFileRead mf] where
  -- Some file system related methods like:
  ls : (dir : FilePath := ".") → m (Array IO.FS.DirEntry)
  ...
  -- Perform file reading on a specific file.
  readFile : FilePath → mf α → m α

[Eric Wieser]

Then the caller just writes [Monad mf] [MonadFileRead mf] [MonadFS m mf] if they're writing generic code

[Tage Johansson]

Miller's solution works. The only annoying thing is that I have to write MonadFS.mf m instead of m.mf.

def foo [MonadFS m] : MonadFileRead (m.mf) := inferInstance

[Kyle Miller]

Eric Wieser said:

Then the caller just writes [Monad mf] [MonadFileRead mf] [MonadFS m mf] if they're writing generic code

Sweeping tradeoffs under the rug using the word "just" makes lots of things easy :smile: Tage was asking how to avoid that ("I could make mf as an outParam, and it works, but the class head gets really large and I will have to repeat it in every subclass of MonadFS.") Outparams have the following nice properties: they make it more likely that mf has the canonical instances (having a monadInst field allows users to override the instance), they make it so one can refer to whatever mf is directly (when it's a field, you generally have to refer to MonadFS.mf m otherwise typeclass inference might not work), and subclass diamonds don't have any special considerations at all since the class doesn't actually hold a copy of the instances. I think for both it's fairly straightforward to add additional typeclass constraints to mf in either subclasses or by users of MonadFS.

[Eric Wieser]

Apologies, I totally missed the outParam sentence :(

[Kyle Miller]

Still, outparams are a very strong alternative, with the downside of being rather verbose.

[Kyle Miller]

@Tage Johansson With the way name resolution works, m.mf can't work because it doesn't know that it should look at MonadFS to resolve the mf function. m is merely a value that has an associated MonadFS instance. The name resolver would have to go out of its way to see that there's an instance involving m that has an mf defined.

I think I remember some discussions about how to eventually support this though. There are at least a few places in mathlib where this feature would really help.

[Tage Johansson]

If I export mf I can write m |> mf though, so I think that's very acceptable.
Thanks for the help.

[Tage Johansson]

I don't think this "square-bracket"-syntax in classes/structures and the instance attribute thing is documented anywhere though. At least I couldn't find it.

[Mario Carneiro]

it should surely have some documentation, typeclasses are a rather core part of lean

[Mario Carneiro]

the manual has https://leanprover.github.io/lean4/doc/typeclass.html, although it's not particularly fleshed out

[Mario Carneiro]

I guess your point was about using square brackets in class declarations; this falls out of the fact that class declarations consist of binders and [inst : MyClass A] is a binder

[Alex Keizer]

Mario Carneiro said:

[..] class declarations consist of binders [..]

I think it's this point that is not super clear, especially when writing the binders (as is idiomatic) like

structure Point (α : Type u) where
  x : α
  y : α

I know I didn't make the connection between x : α syntax and binder syntax until I saw a structure defining its field with bracketed binders, like (x : α). Once that connection is made, trying out implicit and instance binders becomes more natural.

[Eric Wieser]

I think the key realization is probably that

structure Point (α : Type u) where
  x : α
  y : α

is roughly short for

inductive Point (α : Type u)
| mk (x : α) (y : α)

where now not only are the binders visible, but so is the function Point.mk that they're being used for