Library organization

[Lysxia]

WIP. Right now I'm just putting the plan up for discussion.

• All implementations and proofs must be (at least) one directory deeper under theories/.

• Modules directly under theories/ will only reexport things from the inner directories.

We should probably undertake the reorganization in this very PR so we can address directly unforeseen practical problems.

---

The rendered plan.

[Lysxia]

As I actually try to implement this, I find I missed three files:

• MFixITree: I have some idea to rewrite it (#35), then it would go under Interpret as a general theory of monads we can interpret ITree into.
• Trace: I feel that it should go under Interpret...
• OpenSum: as is, Indexed would be the most fitting place, but the mechanism implemented there is quite general, and in fact duplicated in Basics_Functions. Maybe it generalizes for all (co)cartesian categories? I'll have to check.

In fact, all four categories in this plan are cocartesian, so it would make sense to describe that in Basics.Categories as well.

[Lysxia]

The InterpretFacts file is going to be quite big, so it might make sense to split things further. *Facts and *Proper modules, perhaps?

[gmalecha]

This seems like a pretty reasonable plan. The contexts of Basics would be nice to move out somewhere else (if people buy into package managers, this shouldn't be a problem). Either ExtLib or some other library. I've been wondering if ExtLib should be more minimal.

[Lysxia]

So far I'm following the approach of "Type classes for Mathematics in Type Theory" to implement categories, http://www.eelis.net/research/math-classes/mscs.pdf and it works pretty well.

[Lysxia]

I'm running into universe inconsistencies while putting the category of effect morphisms E ~> F under the Category interface.

@gmalecha Can you take a look?

I put the current state of my code in branch reorg-category-ui, and the problem comes up in theories/Interp/HandlerFacts.v, line 115.

One workaround is to not have the different categories share the same type classes and live with the duplication.

[Lysxia]

Not using universe polymorphism seems to help (test-no-up branch)

[gmalecha]

I had a busy week last week, so I didn't get a chance to look at this. The current reorg-category-ui doesn't seem to build for me.

COQC theories/Core/KTree.v
File "./theories/Core/KTree.v", line 10, characters 5-16:
Error: Unable to locate library Eq.UpToTaus with prefix ITree.

make[2]: *** [Makefile.coq:663: theories/Core/KTree.vo] Error 1
COQC theories/Core/KTreeFacts.v
File "./theories/Core/KTreeFacts.v", line 12, characters 5-15:
Error: Unable to locate library Core.KTree with prefix ITree.

[Lysxia]

Ah sorry about that, I forgot to add a file. But somehow the error disappeared!?

[gmalecha]

Does this mean you don't see the universe inconsistency anymore?

[Lysxia]

That's right.

[Lysxia]

This is starting to stabilize. The main changes are:

• Remove all Set Universe Polymorphism., somehow things work better without it.

• Unify all four cocartesian categories under a common interface. I'm using the math-classes approach, which I find quite nice.

  There are minor discrepancies between the written plan and the current setup, but I propose to merge this ASAP.

---

The main things left to do after this are:

• Split up Effects.Std.

• Clean up Interp.TranslateFacts, Interp.MorphismsFacts, Interp.FixFacts.

• Factor out the theory of traced monoidal categories (Basics.Category currently stops at symmetric monoidal categories) from KTree and KTreeFacts. This will be useful for Handler.

• Clean up SimUpToTaus, remove UpToTausExplicit (I think we can extract a inversion lemma for eutt out of it).

[Zdancewic]

This looks like it's coming along well!

Do you think that it has stabilized enough for me to start working on the tutorial material? I'll start with something very basic like examples/Factorial.v so I'm not in the way. I'm anxious to start generating documentation about the primary interfaces.

[Lysxia]

Yes I think things are pretty stable now.

[gmalecha]

I'll try to take a look at the universe polymorphism bit. It may just be a matter of adding cumulativity.

[Lysxia]

Ok. I think this is good to merge.

[Zdancewic]

I agree -- we can then work on documentation from there. Thanks!