Tradeoffs of concrete types defined as subobjects

Often, it is possible to define a concrete type as a subobject of another concrete type. Take eg the unit circle in the complex plane. It is naturally a submonoid (nevermind that it is actually a subgroup, we currently can't talk about subgroups of fields), so one natural definition would be

-- Subobject design
def circle : Submonoid Complex where
  carrier := {x : Complex | ‖x‖ = 1}
  ...

The other option would be to define it as a custom structure:

-- Custom Structure design
structure Circle : Type where
  val : Complex
  norm_val : ‖val‖ = 1

Finally, an intermediate option would be to define it as the coercion to Type of a subobject:

-- Coerced Subobject design
def Circle : Type := circle -- possibly replacing `circle` by its definition

This page is about the tradeoffs in picking one definition over another.

Typeclass search

In the Subobject design, all instances about circle are actually about ↥circle where ↥ is CoeSort.coe. Eg Foo circle is secretly Foo ↥circle. This makes the head symbol be CoeSort.coe, meaning that typeclass search will try unifying every Foo ↥someSubobject instance with Foo ↥circle. In doing so, it will try unifying every subobject someSubobject with a Foo instance with circle. This is potentially really expensive.

The Coerced Subobject and Custom Structure designs do not suffer from this performance penalty.

See #12386 for an example where switching from the Subobject design (ringOfIntegers) to the Coerced Subobject design (RingOfIntegers) dramatically increased performance.

Dot notation

In the Subobject design, x : circle really means x : ↥circle, namely that x has type Subtype _. This means that dot notation x.foo resolves to Subtype.foo x rather than the expected circle.foo x.

The Coerced Subobject and Custom Structure designs do not suffer from this (unexpected) behavior.

See #15021 for an example where switching from the Subobject design (ProbabilityTheory.kernel) to the Custom Structure design (ProbabilityTheory.Kernel) was motivated by access to dot notation.

Custom named projections

In the Subobject and Coerced Subobject designs, the fields of ↥circle/Circle are val and property, as coming from Subtype. This leads to potentially uninforming code of the form

-- Subobject design
def foo : circle where
  val := 1
  property := by simp

-- Coerced subobject design
def bar : Circle where
  val := 1
  property := by simp

In the Custom Structure design, projections can be custom-named, leading to more informative code:

def baz : Circle where
  val := 1
  norm_val := by simp

Generic instances

In the Coerced Subobject and Custom Structure designs, generic instances about subobjects do not apply and must be copied over manually. In the Coerced Subobject design, they can easily be transferred/derived:

def Circle : Type := circle
deriving TopologicalSpace

instance : MetricSpace Circle := Subtype.metricSpace

In the Custom Structure design, these instances must be either copied over manually or transferred some kind of isomorphism.

The Subobject design, by definition, lets all generic instances apply.

Conclusion

Aspect	Subobject	Coerced Subobject	Custom Structure
Typeclass search	Possibly expensive	Fast	Fast
Dot notation	✗	✓	✓
Custom named projections	✗	✗	✓
Generic instances	automatic	easy to transfer	hard to transfer but could be improved