ohnosequences / stuff

Useful stuff.
GNU Affero General Public License v3.0
1 stars 0 forks source link

experiment with local-implicits style syntax #15

Closed eparejatobes closed 7 years ago

eparejatobes commented 8 years ago

I want to write something about this before I forget. First, a bit of context: If we have a monoidal category, we want to have as syntax for morphisms not only f ⊗ g, but also composition, etc. For that, we can

  1. Leave all structures and types as they are, without extending anything (this implies for example that a monad is not a functor; it's a structure on a functor)
  2. define all syntax as traits which extend Any, with the implicit parameter being by default an abstract method

That way syntax for a 2-rig-category could include all that it should have.

eparejatobes commented 8 years ago

After several experiments with this, my notes are

  1. imply works, and if we do the hierarchies well we should be able to use just one implicit for all syntax on a morphism
  2. It looks like in a weird case we need to require structures on a given category to be Singletons in the parameters of MorphismSyntax. Strange.

The approach outlined in tests looks good. Will work on this tomorrow at some point.