|
| |||
|
|
Exponential-polynomial profunctors II. Modularity with respect to a monoid We have established that all exponential-polynomial type constructors are profunctors. Now, profunctors are certainly weaker than functors, but perhaps there are type constructors that are still less powerful. One possibly interesting property is "modularity with respect to a category-level monoid". This consideration was inspired by a conversation with posic.I call a "category-level monoid" an associative binary operation defined on any pair of types and yielding another type, in other words, a functor P: C ⨉ C - > C and a fixed "zero object" Z ∈ C with the properties P(Z, t) = t; P(t, Z) = t; (left and right identity laws) P(x, P(y, z)) = P(P(x,y),z); (associativity) Since we are working in a Cartesian closed category C, there are at least two category-level monoids, corresponding to the product, P(x,y)=x*y, Z = 1 and the co-product, P(x,y)=x+y, Z = 0. There might be other category-level monoids, but so far I haven't been able to find any others, just by trial and error. For example, the "weak pair" P(x,y) = (x -> y) * (y -> x) satisfies the identity laws but not the associativity law (although it comes close to satisfying it too). Given a category-level monoid (P,Z), we can define a "module over (P,Z)", which is a type constructor F(t) with an operation of "multiplication by other types". Let me first remind myself what a "module" is. Let us temporarily denote by "⊙" the operation of the monoid and by " |
||||||||||||||