structure: field vs. parameter

Stream: new members

[Yannick Seurin]

When defining a structure that depends on some type α, one can declare it either as a parameter or a field. Say I want to do something like this (which works well):

import Mathlib

noncomputable section

structure Foo (α : Type) where
  draw_random : PMF α

variable (G : Type) [CommGroup G] [Fintype G]

def bar : Foo G where
  draw_random := PMF.uniformOfFintype G

def mul_by_const (a : G) : PMF G := do
  let x ← (bar G).draw_random
  PMF.pure (a * x)

end

But if I try to declare α as a field, then I run into the following problem:

import Mathlib

noncomputable section

structure Foo where
  α : Type
  draw_random : PMF α

variable (G : Type) [CommGroup G] [Fintype G]

def bar : Foo where
  α := G
  draw_random := PMF.uniformOfFintype G

def mul_by_const (a : G) : PMF G := do
  let x ← (bar G).draw_random
  PMF.pure (a * x) -- failed to synthesize HMul G (bar G).α ?m.14

end

Is there a way to have Lean realize that (bar G).α is actually G?

As a side question, when should one prefer the field vs. parameter approach? MIL briefly touches the question in Section7.2:

It is sometimes useful to bundle the type together with the structure, and Mathlib also contains a definition of a Grp structure that is equivalent to the following:

structure Grp₁ where
α : Type*
str : Group₁ α

The Mathlib version is found in Mathlib.Algebra.Category.Grp.Basic, and you can #check it if you add this to the imports at the beginning of the examples file.

For reasons that will become clearer below, it is more often useful to keep the type α separate from the structure Group α.

The parameter approach seems to facilitate class inference, are there other benefits? When is the field approach preferable?

[Snir Broshi]

Is there a way to have Lean realize that (bar G).α is actually G?

let x : G ← (bar G).draw_random

Also in general you should use Type* rather than Type, like the MIL example you quoted, unless you have a good reason to not be generic over universes

[Snir Broshi]

The approaches you describe are bundled vs unbundled. I think the field version is the bundled one.
The field approach with Types isn't that useful AFAIK, but with other things it is.
For example, graphs over vertices V : Type* currently have a type Walk (u v : V) where u v are the endpoints specified as parameters, but this makes it hard to compare walks with different endpoints.
There's also docs#SimpleGraph which has the parameter V : Type*, whereas docs#Graph has such a parameter but also a field vertexSet : Set V which makes it easier to work with graphs over a different set of vertices.
You can also read #mathlib4 > The design of matroids which I believe talks about similar problems.

[Yannick Seurin]

Thanks a lot for the pointers!