8
$\begingroup$

By a “structure category” I mean a concrete category that contains as objects all spaces of a particular type of structure, and as morphisms, functions that preserve that type of structure. I.e. the standard categories like Grp, Top, Cat, Ab, Vec, ... etc.

A “parametric polymorphic function” is a concept from type theory and functional programming, which says intuitively that

parametric polymorphic function: a function $f_X$ that is parameterized by type (object) $X$, but where the computation it performs is independent of $X$.

Obviously, a parametric polymorphic function is a natural transformation in a category where objects are types (if the underlying functors are also well-behaved, e.g. are also parametric polymorphic). This is because of some “theorems for free” result.

But natural transformations are defined categorically, rather than type theoretically. So in arbitrary categories, a natural transformation does not need to correspond to any parametric polymorphic function.

I am wondering whether in “structure categories”, the “naturality” of $f_X$ (i.e. of a pre-natural transformation), coincides with “parametric polymorphism”, and how this can be seen from the definition.

  • Are there (natural?) examples of natural transformations $f_X$ in structure categories that are not “parametrically polymorphic”? I.e. whose formula/computation depends on the object $X$?

  • If not, how can we see from the commuting diagram property of natural transformations $f_X$ that “they do the same computation regardless of $X$”?

  • Can we prove the inverse of the “theorems for free” result? i.e. Can we prove that, if a transformation is natural in the category of a ”sufficiently general” type system, then it must be somehow equivalent to a parametrically polymorphic function (possibly given some conditions on the underlying functors)?

$\endgroup$
  • 1
    $\begingroup$ I think this is an interesting question. One potentially important issue I see is that there's no sense in which morphisms in these categories are computations which have formulas or programs. For instance, there exists a natural isomorphism out of the identity endofunctor of sets which acts as an arbitrary isomorphism from any given set to a fixed set of the same cardinality, and I think this really does depend on the object, intuitively. But on the other hand I have a sense that parametric polymorphism is getting at a similar intuition to naturality. $\endgroup$ – Kevin Carlson Mar 10 at 16:38
  • $\begingroup$ @KevinCarlson, Thank you for your comment! There is a sense in which the natural isomorphism you describe depends only on the object “via the information contained in the functor”. What if we also force the functor to be parametric polymorphic though? $\endgroup$ – user56834 Mar 10 at 18:20
  • $\begingroup$ Good point. I'm not really sure how to interpret parametric polymorphicity for a functor. For instance, can such a functor use the cardinality of its inputs, or does it have to be "even more uniform" than that? $\endgroup$ – Kevin Carlson Mar 10 at 22:50
  • 1
    $\begingroup$ @KevinCarlson, I am not sure what the best way to restrict it is. Perhaps the following: strictly speaking, I would say a functor is paremetric polymorphic if it is paremtric polymorphic in it's operation on morphisms. i.e. Given a morphism $f:X\to Y$, it should map to a morphism $F(f):F(X)\to F(Y)$ without using any information about $X$ and $Y$, only using the information that all objects in the category have in common. Hence it cannot use the information about $X,Y$'s cardinality. But e.g. in the category of groups, it can use the face that every element of every groups have inverses. $\endgroup$ – user56834 Mar 11 at 12:30
  • 1
    $\begingroup$ That is an interesting question, I would also like to point out an additional fact: if you deal with not parametric functors, i.e. functors whose arrows functions depends on the objects the free theorem trick does not apply and there are polymorphic functions that are not natural transformations. $\endgroup$ – Giorgio Mossa May 2 at 14:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.