1

I know following types of Functors:

  1. Polynomial functor == simple not-nested parameterized datatype
  2. Generalization of 1, by using "parameter removing" newtypes: Fix, Some (existentials), possibly some GADTs
  3. Exponential functor == X -> a for fixed X
  4. Generalization of 2 to all positive-position functions.
  5. Compositions of previous points

It seems like points 2,4,5 can be covered by some conditional instances, like for Data.Functor.Compose.

Question:

  1. Is my statement correct or I am missing something?
  2. Can this be formalized? In particular: what is full list on point 1 and how to fix that points 2,4,5 actually do interfere?
  3. Can this be described using HFunctors?
uhbif19
  • 3,139
  • 3
  • 26
  • 48
  • On (1), the list is missing functors that aren't strictly positive, like `Cont` and `Select`. – duplode Jun 10 '23 at 15:30
  • @duplode I was thinking on `Cont` as (main?) example of point 2. Like `a` in `a -> r -> r` is positive position, right? – uhbif19 Jun 10 '23 at 16:37
  • In `(a -> r) -> r`, the position of `a` is positive, but not strictly positive. I don't quite see how that would fit as a generalisation of point 1. – duplode Jun 10 '23 at 16:49
  • 1
    Point 5 is more a theorem *about* functors than a kind of functor: the composition of two functors is always a functor. It might be interesting to try to define the notion of a "prime" functor, one that cannot be defined as the composition of two other functors. – chepner Jun 10 '23 at 20:20
  • 2
    Also, two contravariant functors [can be composed to give a covariant one](https://hackage.haskell.org/package/contravariant-1.5.5/docs/Data-Functor-Contravariant-Compose.html#t:Compose). This covers *some* of the not strictly positive `Functor`s, such as `Cont`. – duplode Jun 10 '23 at 21:11
  • 1
    I think you are missing an important generalization of `2`, namely, the generalization to fixpoints of more exotic kinds than `* -> *`. – Daniel Wagner Jun 11 '23 at 04:47
  • 1
    You might like [Natural map derivation algorithm](https://stackoverflow.com/q/67314984/791604). – Daniel Wagner Jun 11 '23 at 05:05
  • @chepner > Point 5 is more a theorem about functors than a kind of functor Of course. Still knowing generating set of algebra is useful. – uhbif19 Jun 11 '23 at 11:24
  • @duplode > In (a -> r) -> r, the position of a is positive, but not strictly positive You right, I set parentheses wrong. For CC you need them left-associative. That seems right to have this as separate case, cuz CC is kinda equivalent to classic logic. – uhbif19 Jun 11 '23 at 12:02

0 Answers0