why use carrier types instead of direct polymorphism?

Stream: new members

[Rado Kirov]

(apologies if this explained in MIL, just send me a pointer to read more). I am finishing Theorem proving with Lean and it has the following example for Semigroup

structure Semigroup where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)

It is neat that dependent type theory allows for the carrier type to be just one more field in the structure, but why not use a direct polymorphism to define it:

structure Semigroup2 (α: Type u) where
  mul : α → α → α
  mul_assoc (a b c : α) : mul (mul a b) c = mul a (mul b c)

[Chris Bailey]

I think that excerpt from TPIL is just a motivating example for CoeSort. Your Semigroup2 is indeed the "preferred" way of doing it in Lean, that's how it's defined in mathlib.

(your definition of) Semigroup is what's called "bundled" and Semigroup2 is "parameterized" or "unbundled". The first thing I read that explained why someone might prefer the bundled version was this blog post by Thom Hales about proof assistants (ane Lean); ctrl+f for the first use of the word "bundled" to skip to the relevant part.

[Rado Kirov]

Fascinating, thanks for sharing that blog post. I see that there are good arguements pro and con either approach.

It seems the mathlib's definition is also a type class, instead of structure, which is somewhat surprising to me since a single type like Nat can have multiple semigroups defined. Type classes feels like better solutions for having a single instance attached to a single type.

[Vlad Tsyrklevich]

By multiple semi-groups I assume you mean for + and *, but then rather than thinking about it as 2 separate semi-groups, they are actually related by distributivity, so you would think about it as a ring, and then pull in that more-general type class.

[Shreyas Srinivas]

Follow up question: why doesn’t mathlib parametrise by both the Type and the operations? Does it mess up typeclass resolution?

[Edward van de Meent]

i'd guess it makes variations in spelling of the operation annoying to work with

[Eric Wieser]

It means that things like add_zero end up:

• having unhelpful names like op_identity
• not being eligible for simp as their key is just _

[Chris Bailey]

Rado Kirov said:

It seems the mathlib's definition is also a type class, instead of structure, which is somewhat surprising to me since a single type like Nat can have multiple semigroups defined. Type classes feels like better solutions for having a single instance attached to a single type.

Lean allows users to declare more than once instance of a typeclass for a given type. Also this is from a couple of years ago but I think most of this still holds: Anne Baanen (a user here) wrote a paper about the typeclass/hierarchy building choices made in mathlib: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.4

There are a lot of practical considerations that go into choice of representation when the primary goal is actually creating and interacting a large code base.

[Chris Bailey]

Also a tl;dr summary of the paper by the author: #mathlib4 > TC `extends` vs instance-implicit binders @ 💬

[Kyle Miller]

Typeclasses are a way to implement synecdoche (the figure of speech where you refer to something by one of its parts).

In formal math texts, this is the common "a semigroup is a pair $(G,\mu)$ such that [...], and by abuse of notation we will use $G$ itself to refer to the semigroup when it does not cause confusion." The "not causing confusion" is when there is a single canonized semigroup structure on $G$. Classes (with the type as a parameter) let us register what we consider to be the canonical structure via instances.

Lean doesn't do anything to prevent you from accidentally registering multiple instances. It's a design error when you give multiple instances.

There are techniques to attach different structures to the same type. For example, given a multiplicative semigroup on X, you can write Additive X for the type with an additive structure that is defined in terms of the multiplicative one. For example:

#eval (fun (a b : Additive Nat) => a + b) (3 : Nat) (4 : Nat)
-- 12

This works because typeclasses work on the syntactic form of the type. While Additive Nat = Nat, typeclass synthesis doesn't see that.

[Eric Wieser]

(of course, you're supposed to write (Additive.ofMul 3 + Additive.ofMul 4).toMul instead of that, but that's beside Kyle's point)

[Kyle Miller]

Thanks for keeping it honest :smile: