Polymorphic structure versus a carrier : Type field

Stream: new members

[Nathan Taylor]

Hi all,

I'm working through the coersions section of FP In Lean and the implementation of Monoid has a convention that I wasn't expecting: the definition of the datatype embeds a Carrier : Type field, in contrast to making Monoid polymorphic over some type, e.g.:

structure Monoid (α: Type) where
  neutral: α
  op: α → α → α

Two questions:

1) Are these equivalent? I was able to finish the section on monoids with my implementation, so at least for simple cases it appears to be so, but if not, what are situations where my implementation is inexpressive enough to not work? If they _are_ equivalent, when should I favour polymorphism over embedding a carrier Type?

2) What are the runtime semantics between the two? I assume that in my polymorphic version \alpha is erased at runtime, whereas in the version used in the book, presumably, that isn't the case?

(The text later on says, "putting a type in a field of a structure, similarly to the Monoid example, can make sense in contexts where there is more than one way to implement an operation and more manual control is needed than type classes would allow"; however, I'm not sure I fully understand this point, but perhaps this is the thing I'm missing?)

Thanks,
Nathan

[Joël Riou]

In mathlib, monoids are implemented in a similar way as what you suggest https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html#Monoid
The difference is that there is a typeclass system: in mathlib Monoid is not just a structure but a class, given α : Type*, when we have defined an instance of Monoid α (this is related to variables with brackets [Monoid α]), then we can use the definitions of 0 and + transparently (everything works as if we have endowed α with a monoid structure, e.g. we can write statements like ∀ (x y : α), x + y = y + x).

In mathlib, we also have the other type of definition for the category of monoids. Then, an object in this category is a tuple consisting of type α (the carrier) and the monoid structure on it. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/MonCat/Basic.html#MonCat We would usually say that this is the "bundled" version of the definition of monoids.

Depending on what we want to do, both ways are useful and complement each other.