Open emeinhardt opened 8 months ago
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(n2) 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.
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
t
is isomorphic to the freef
over some type constructorg
", where such statements undergird useful constructions for working with DSLs defined by someg
— free (co)monads over a polynomial functor, etc.Control.Category.Constrained.Reified
presuppose that the category type you're constructing a freex
structure over already have anx
instance: e.g. theObject
constraints onCategoryId
andCategoryCompo
entail that you can only construct anReCategory k
value for ak
that already has aCategory
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 anx
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 typek
into aCategory
(or aCartesian
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.