Tradeoffs behind Control.Category.Constrained.Reified?

[emeinhardt]

Could you explain the design behind Control.Category.Constrained.Reified — what use cases you have in mind and what salient alternatives are?

My context for asking is that

1. I am used to encountering statements like "Type t is isomorphic to the free f over some type constructor g", where such statements undergird useful constructions for working with DSLs defined by some g — free (co)monads over a polynomial functor, etc.
2. I understand GHC's type inference about things as complex as the types introduced in this package is not quite as powerful as one might like, and that means there are some things one might be able to express but which might be awkward or difficult to use.
3. The constraints on the constructors of all the reified free types in Control.Category.Constrained.Reified presuppose that the category type you're constructing a free x structure over already have an x instance: e.g. the Object constraints on CategoryId and CategoryCompo entail that you can only construct an ReCategory k value for a k that already has a Category instance.

Unless I'm missing something, item 3 means that the types in the Reified module may still be useful for constructing "unevaluated" DSL fragments that can then be interpreted in different ways provided you do all the work to define an x instance in the first place, but there's no support for the class of use cases in item 1: there's no support for freely lifting a primitive type k into a Category (or a Cartesian one, etc.). What's the story as to why?

I'd guess the answer has to do with object + morphism constraints and some combination of type safety + ergonomics, but I'd appreciate having some of that spelled out.

[leftaroundabout]

I first came up with the Reified module when I implemented a category of affine mappings between vector spaces. The rationale was, a general affine map requires storing a transformation matrix, requiring both that a basis on the spaces is available and then O(n²) space where n is the dimension of the spaces - quite restrictive and expensive, which is annoying in particular for large spaces and when oftentimes one deals with simple transformations that do something simple like swapping a tuple, which can be done far more efficiently and without any requirements on the tuple elements. ReMorphism can express such special cases in O(1). But the whole approach turned out to not really scale, it ended up either deferring everythig to an ad-hoc DSL that you then carry around without actually performing any computations, or convert to dense matrices most of the time anyway.

By now I implemented far more specialised approaches in the linearmap-category package, which makes the whole Reified module obsolete for my use case. I'm not sure if it can be useful for something else, so perhaps I should just deprecate it.