Stream: Hierarchy Builder devs & users

Topic: Extending the topology heirarchy


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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..

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Pierre Roux (Mar 27 2023 at 08:33):

Just opened issues on HB to remember.

view this post on Zulip 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: Apr 21 2024 at 02:41 UTC