## Stream: Hierarchy Builder devs & users

### Topic: Extending the topology heirarchy

#### Zachary Stone (Mar 27 2023 at 02:47):

Perhaps explaining my journey with HB is useful for you to see? It's certainly useful for me to document for myself as I learn. Skip to the end for the code. My overall plan is to add stuff like "in the discrete topology" and "in the order topology" to the hierarchy.

Step 1 -------
To start, I'd like just define the mixins

``````HB.mixin Record Nbhs_isOrderTopology d M of Topological M & Order.POrder d M :=
{order_nbhsE : forall x, nbhs x = @order_nbhs d M x}.

#[short(type="orderTopologicalType")]
HB.structure Definition OrderTopological d :=
{M of Topological M & Order.POrder d M & Nbhs_isOrderTopology d M }.
``````

where `order_nbhs` is defined earlier, along with a bunch of facts about it. So far so good.

(Aside on the math: while order_nbhs is sometimes useful on a partial order, but we are only guaranteed a topology on a total order. So we want to build a Order.Total -> OrderTopological instance. But it must be behind an alias because many order types (like nat) don't typically use their induced order topology)

Step 2 ------

First problem is that we that we need `isPointed`, so I added new structure of pointed and totally ordered.

``````#[short(type="pointedOrderType")]
HB.structure Definition PointedOrder d := { M of Pointed M & Order.Total d M}.
``````

This fails with

``````You must declare the hierarchy bottom-up. There are two ways out:
- declare structure topology.PointedOrder before structure topology.OrderTopological;
- declare an additional structure from which both inherit
``````

Ok... I still don't 100% understand this, but know how to intersect two structures. So I added

``````#[short(type="pointedPOrderType")]
HB.structure Definition PointedPOrder d := { M of Pointed M & Order.POrder d M}.
``````

at the top, and that seemed to satisfy it.

Step 3 ------
Ok, so now I have `PointedOrder`, and can write down my alias and assign it all the

``````Definition order_topology {d} (M : pointedOrderType d) := M.

Section order_topology.
Context {d} {M' : pointedOrderType d}.
Local Notation M := (@order_topology d M').

HB.instance Definition _ := hasNbhs.Build M order_nbhs.
HB.instance Definition _ := Nbhs_isNbhsTopological.Build
M order_nbhs_filter order_nbhs_singleton order_nbhs_nbhs.
HB.instance Definition _ := Nbhs_isOrderTopology.Build
d M (fun x => erefl).
End order_topology.
``````

It says that `HB.instance Definition _ := hasNbhs.Build M order_nbhs. ` is non-forgetful inheritance. Now I'm a bit stuck because

1. I would have hoped an alias would have protected me from this.
2. Does HB know the actual path of competing inheritance? Which mixin are they competing for? Some extra info would be super helpful.

Acutal broken code -----------------------------
In the end, this was my attempt

``````#[short(type="pointedPOrderType")]
HB.structure Definition PointedPOrder d := { M of Pointed M & Order.POrder d M}.

HB.mixin Record Nbhs_isOrderTopology d M of Topological M & Order.POrder d M :=
{order_nbhsE : forall x, nbhs x = @order_nbhs d M x}.

#[short(type="orderTopologyType")]
HB.structure Definition OrderTopological d :=
{M of Topological M & Order.POrder d M & Nbhs_isOrderTopology d M }.

#[short(type="pointedOrderType")]
HB.structure Definition PointedOrder d := { M of Pointed M & Order.Total d M}.

Definition order_topology {d} (M : pointedOrderType d) := M.

Section order_topology.
Context {d} {M' : pointedOrderType d}.
Local Notation M := (@order_topology d M').
(* This is non-forgetful *)
HB.instance Definition _ := hasNbhs.Build M order_nbhs.
HB.instance Definition _ := Nbhs_isNbhsTopological.Build
M order_nbhs_filter order_nbhs_singleton order_nbhs_nbhs.
HB.instance Definition _ := Nbhs_isOrderTopology.Build
d M (fun x => erefl).
End order_topology.
``````

#### Zachary Stone (Mar 27 2023 at 03:46):

Ok, so after all that it turns out I was missing ` : Type` on the alias. Obvious in retrospect. We need to control when `PointedType.sort` gets called, otherwise it's not _really_ an alias. The following works fine.

``````Definition order_topology {d} (M : pointedOrderType d) : Type := M.

Section order_topology.
Context {d} (M' : pointedOrderType d).
Local Notation M := (@order_topology d M').
(* No longer non-forgettful*)
HB.instance Definition _ := Pointed.on M.
HB.instance Definition _ := hasNbhs.Build M order_nbhs.
HB.instance Definition _ := Nbhs.on M.
HB.instance Definition _ := Nbhs_isNbhsTopological.Build
M order_nbhs_filter order_nbhs_singleton order_nbhs_nbhs.
HB.instance Definition _ := Nbhs_isOrderTopology.Build
d M (fun x => erefl).
End order_topology.
``````

#### Zachary Stone (Mar 27 2023 at 04:29):

To complete the story, see https://github.com/math-comp/analysis/pull/885 for the actual code.

#### Pierre Roux (Mar 27 2023 at 07:35):

Zachary Stone said:

This fails with

``````You must declare the hierarchy bottom-up. There are two ways out:
- declare structure topology.PointedOrder before structure topology.OrderTopological;
- declare an additional structure from which both inherit
``````

Ok... I still don't 100% understand this, but know how to intersect two structures. So I added

This error message should indeed be improved. It should tell what missing join is expected. I also lost a ton of time staring at the graph trying to understand what I needed to add (might be obvious for simple examples but no longer is with a large hierarchy).

#### Pierre Roux (Mar 27 2023 at 07:37):

Zachary Stone said:

Ok, so after all that it turns out I was missing ` : Type` on the alias. Obvious in retrospect. We need to control when `PointedType.sort` gets called, otherwise it's not _really_ an alias.

I also lost time with that. We have to be careful when using `HB.instance` that it actually produces the expected instances (and not just mixins), either by looking at its output or inspecting `Print Canonical Projections order_topology.`.

#### Pierre Roux (Mar 27 2023 at 07:38):

I wonder whether we shouldn't add a warning when a `HB.instance` only produces mixins but no instance. In my experience this is usually the sign that something is wrong (except maybe in builders).

#### Cyril Cohen (Mar 27 2023 at 08:10):

Pierre Roux said:

I wonder whether we shouldn't add a warning when a `HB.instance` only produces mixins but no instance. In my experience this is usually the sign that something is wrong (except maybe in builders).

The only place where `HB.instance` can be allowed to create no instance is when one did not adapt yet code that evolved (maybe the instance is now provided by other libraries, etc,) but we want to preserve backward compatibility. So a warning is good.

#### Pierre Roux (Mar 27 2023 at 08:33):

Just opened issues on HB to remember.

#### Zachary Stone (Mar 27 2023 at 14:36):

The other debugging feature I'd appreciate is if `is_not_cannonically_a` told me which mixins were missing.

All that said, I find the performance issues much more urgent than debugging. All the waiting really slowed me down. It's a great sign of maturity for any library when performance starts to matters, so I'm actually pretty happy to be at this point.

Last updated: Sep 15 2024 at 13:02 UTC