Extending the topology heirarchy · Hierarchy Builder devs & users

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.

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)

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}.

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}.

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

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):

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

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):

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):

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):

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.

Stream: Hierarchy Builder devs & users

Topic: Extending the topology heirarchy

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