NickHu / homotopy-io

Rewritten homotopy-core
3 stars 2 forks source link

Dimension storage #14

Closed jamievicary closed 4 years ago

jamievicary commented 4 years ago

At the moment we store a dimension in RewriteN, but not in DiagramN. It would be good to discuss the rationale for that here. It could be that it's the right way to go, but it's not obvious to me.

One possibility is for both DiagramN and RewriteN objects to store dimension integers, for convenience. (Potential downside is that we're storing a lot of unnecessary information.)

Another possibility is to never store dimension integers, since they can always be computed for well-typed structures. (Potential downside is that it would then take O(n) to compute the dimension of an n-dimensional Diagram or Rewrite, as you need to track to the bottom of the syntax tree.)

Another possibility is for only one of DiagramN and RewriteN to store dimension integers. If we choose this path, it might be easier to store the dimension in DiagramN, and not RewriteN. One reason is that rewrites can be identities, which currently store no information at all, which seems nice to preserve. Another reason is that diagrams are the primary geometrical entities which we display. Another reason is that diagrams already store meta-information, like their source boundary, while rewrites don't, being sparse; so it's perhaps to natural to attach one more piece of meta-information to a diagram, than to a rewrite.

zrho commented 4 years ago

A RewriteN might have no cones, in which case the dimension can't be determined, except that it isn't zero. These are always identity rewrites, and there is some design space around these, but in the way Rewrites are encoded currently, having the dimension explicitly makes sense. For Diagrams, even when there is no cospan, the dimension can always be determined by traversing the path along the sources, as it is currently.

At the moment there is no explicit type to represent rewrites that aren't zero dimensional, like there is a type for non-zero dimensional Diagrams. Hence there are a couple of functions acting on Rewrites that are marked Partial because they don't make sense for rewrites of 0-diagrams. This isn't a specific design decision, and we might change that at some point. Luckily types make refactoring a breeze.

On Wed, 5 Aug 2020, 23:11 jamievicary, notifications@github.com wrote:

At the moment we store a dimension in RewriteN, but not in DiagramN. It would be good to discuss the rationale for that here. It could be that it's the right way to go, but it's not obvious to me.

One possibility is for both DiagramN and RewriteN objects to store dimension integers, for convenience. (Potential downside is that we're storing a lot of unnecessary information.)

Another possibility is to never store dimension integers, since they can always be computed for well-typed structures. (Potential downside is that it would then take O(n) to compute the dimension of an n-dimensional Diagram or Rewrite, as you need to track to the bottom of the syntax tree.)

Another possibility is for only one of DiagramN and RewriteN to store dimension integers. If we choose this path, it might be easier to store the dimension in DiagramN, and not RewriteN. One reason is that rewrites can be identities, which currently store no information at all, which seems nice to preserve. Another reason is that diagrams are the primary geometrical entities which we display. Another reason is that diagrams already store meta-information, like their source boundary, while rewrites don't, being sparse; so it's perhaps to natural to attach one more piece of meta-information to a diagram, than to a rewrite.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/NickHu/homotopy-core/issues/14, or unsubscribe https://github.com/notifications/unsubscribe-auth/AACXKJIUBKTPHUTYNBUYMRTR7HDJ5ANCNFSM4PV44EOA .

jamievicary commented 4 years ago

My understanding was that RewriteI was to be used for an identity rewrite of any dimension. I understand from what you're saying that RewriteI is only to be used for a zero-dimensional identity rewrite. OK, that changes things slightly.

jamievicary commented 4 years ago

Looking through the code, I see that it's convenient to define the dimension of a rewrite so that you can have the composite of rewrites of different dimension be undefined. Of course, this would typically never arise if we're working only with type-checked structures, and it would be possible for the failure case of rewrite composition to be detected in the base case (where we would be composing a Rewrite0 with a RewriteN.)

The current definition of dimension for diagrams could be slightly optimised by checking if there are any cospans, and if so returning 1 plus the dimension of one of the legs.

It's still unclear to me if there are objective reasons for preferring dimensions to be attached to rewrites rather than diagrams, but it's not a big deal.