Library structure - follow standard library? about cubical HOT 21 CLOSED

About Relation it seems a good place to put properties of relations or relation transformers, but less so for specific relations.

Agreed. In the standard library we settled for Data.X.Relation subfolder for specific relations (originally they were in Relation, another design bug encountered and then hastily backed away from!)

from cubical.

I think the main requirement is to keep Cubical.Core quite minimal. The rest is quite flexible I think.

Can you elaborate on how it would look if we followed the structure of the standard library and how that would help with extensibility?

from cubical.

I think the main requirement is to keep Cubical.Core quite minimal. The rest is quite flexible I think.

Yup no need to enlarge that.

Can you elaborate on how it would look if we followed the structure of the standard library

So for example much of the Basics folder would be rearranged as follows:

• Data
  • Bool
    • Properties
  • BinNat
    • Properties
  • Empty
  • Int
    • Properties
  • Nat
    • Properties
  • Unit
  • Sum (currently in Cubical.Basics.NTypes)
  • Product (currently in Cubical.Core.Prelude)
• Codata
  • Stream
• Function

Not sure where Univalence and Equiv fit. Some other folder?

The major point is that in the standard library we've found that mixing definitions and proofs is a common cause of dependency cycles. The inclusion of the Properties files above tries to address this.

At the moment the definition, various operations and the properties of Nat are all mixed together. This will almost certainly cause problems when you want to use machinery that depends on the definition of Nat but not the properties. I hypothesis that you're already running into this problem and that's why the definition of Nat is not currently actually exported by Cubical.Basics.Nat but is exported in Cubical.Core.Prelude...

How that would help with extensibility?

The problem is that these dependency problems will eventually need to fixed by re-organising the library. Every time the library has to be re-organised to fix a design problem, it results in users broken code. The trick is to come up with a structure which works from the start. Sadly we've been forced to break a ton of code depending on the standard library in the last couple of years, so I thought this library might be able to learn from our mistakes!

Finally in my opinion the layout above makes it easier to navigate. What is considered "basic" varies drastically between people 😄

Sorry I realise this probably isn't very helpful, as I don't have time to contribute to this myself. Just thought I should raise it as a suggestion though! It's not a problem if this library goes in a different design direction.

from cubical.

@MatthewDaggitt Those sound like reasonable concerns.

In the standard library, you have e.g. Data.Maybe, Data.Maybe.Base and Data.Maybe.Properties, with Data.Maybe re-exporting only Data.Maybe.Base.

It seems like once you have both .Base and .Properties it would make sense for Data.Maybe to re-export both. Any particular reason to avoid this?

from cubical.

It seems like once you have both .Base and .Properties it would make sense for Data.Maybe to re-export both. Any particular reason to avoid this?

Not that I can see. That sounds like a good idea. That way you get the best of both worlds.

from cubical.

I like this idea! I haven't really used Agda or the standard library for over 10 years, so I'm really appreciating some feedback on how to design this library.

Maybe we should just drop the Basics folder and have folders Data and CoData directly in Cubical? I'm not sure if the HITs should go in Data or stay in a separate folder (maybe with another name like HData)?

About where Equiv, Univalence and NTypes should go: maybe instead of Basics we have Foundations and have those files there? (This is the way Voevodsky called his original univalent foundations library where he invented these notions)

from cubical.

Maybe we should just drop the Basics folder and have folders Data and CoData directly in Cubical?

Yup, I agree. Not all data is basic, as @gallais would testify from his work on AVL trees!

I'm not sure if the HITs should go in Data or stay in a separate folder (maybe with another name like HData)?

I'd err on the side of keeping them separate though perhaps give a more descriptive name than HData.

About where Equiv, Univalence and NTypes should go: maybe instead of Basics we have Foundations and have those files there? (This is the way Voevodsky called his original univalent foundations library where he invented these notions)

That sounds like a good idea!

The one other major area of the standard library that I haven't touched on is Relation, mainly because I can't really find any sort of equivalent as of yet in this library. In the standard library we have three subfolders

• Relation
  • Nullary
  • Unary
  • Binary

where Nullary relations are sets, Unary relations are predicates on sets and Binary relations are standard binary relations. In the standard library these contain many of the definitions that are currently found in various places in this library (e.g. notions of equality, definitions of propositional types etc.).

from cubical.

We could keep Cubical.HITs for "HITs" as that's what they are called, but I think having them in Cubical.Data would also be fine.

About Relation it seems a good place to put properties of relations or relation transformers, but less so for specific relations.

from cubical.

I kind of like the idea of calling the HITs folder Cubical.HigherData to empasize to newcomers that they are just "higher" datatypes. But I guess calling them "HITs" like everyone else is fine as well.

@MatthewDaggitt Where does "types with decidable equality" go in the standard library? I'm not sure where to put for example Hedberg's theorem (types with dec eq satisfy UIP, i.e. are h-sets).

from cubical.

@MatthewDaggitt Where does "types with decidable equality" go in the standard library? I'm not sure where to put for example Hedberg's theorem (types with dec eq satisfy UIP, i.e. are h-sets).

They're in Relation.Nullary and Relation.Nullary.Decidable.

from cubical.

Thanks, I think it makes sense to have a Relation folder as well. I can implement a suggestion for a solution to this issue.

from cubical.

What about Relation.Cubical.* instead of Cubical.Relation.*?

from cubical.

What about Relation.Cubical.* instead of Cubical.Relation.*?

Why?

from cubical.

Why?

Because things are already classified by Data, Relation and Codata while this library is just providing an alternative version of them.
I'm not trying to persuade you, but just coming up with some arbitrary suggestions so we can discuss

from cubical.

What about Relation.Cubical.* instead of Cubical.Relation.*?

I think keeping everything under Cubical is the best idea. The module hierarchy should go from most general classification to least general, and the fact that everything is using Cubical agda is definitely the most general classification.

from cubical.

Sounds good to me.

from cubical.

I did a similar reorganization of the HITs folder now: #50

I also asked a general question about how to organize things in the PR

from cubical.

Any more changes that I should do before closing this?

Maybe I could make a Cubical.Function folder and move equivalences there?

from cubical.

Maybe I could make a Cubical.Function folder and move equivalences there?

Sounds good to me. Otherwise, no I don't have any other major comments at the moment. It all looks much better! I'll keep half an eye out and give a shout if I see some dead-end being explored.

from cubical.

Actually, I think equivalences are such a crucial part of the univalent foundations that they should stay in Cubical.Foundations (we cannot even state univalence without it). What I will do instead is to rename the Foundations.Function file to Foundations.FunExtEquiv to better reflect what is in it. Then I might make a separate subdirectory for equivalences in Foundations some day.

So I consider this PR done now.

from cubical.

Thanks for the feedback and recommendations on library design @MatthewDaggitt !

from cubical.