In Category theory, it is very conspicuous that a definition of a functor should include two functions: on objects and on arrows. However, the usual Haskell Prelude.Functor does not make any mention of the former. Why is that? Would pure be that function on objects?
Specifically, for data F a to be an endofunctor in Hask, there should be given:
-- A function on objects:
omap :: a -> F a
-- A function on arrows:
fmap :: (a -> a') -> (F a -> F a')
For a "small" type function, such as Maybe, it seems safe to name a suitable data constructor, such as Just, as the function on objects. For a type function with more variety — possibly infinite, like [⋅], — I am not so sure. Does it make difference whether I choose \x -> [ ] (a trivial functor), \x -> [x], \x -> [x, x], ..., or \x -> [x, x..]? Or would these be equally rightful, though distinct, instantiations of the "classical" categorial functor?
If so, would it be correct to propose that Prelude.Functor actually defines a whole family of functors at once?
The suggestion, offered in the answers to a question nearby, that the type constructor itself is the function on objects, I am not prepared to accept. We do require that a Functor instance gives lawful evidence to the existence of fmap. In the same way, we should be requiring that a term level function omap on objects is given, should we not? There must be some confusion about the type / term distinction in Hask here, either on my side alone, or in the common knowledge spread around the Haskell community.
To be specific, I may suggest that there are actually two distinct categories we may be talking about:
- Hask — a category which objects are the sets of term level values of particular Haskell types, and arrows are the sets of term level functions.
- Type — a category which objects are sets of types of a particular kind, and arrows are sets of type level functions, that is, types of a kind that has an arrow at the top level of its syntax tree.
Then, fmap is an arrow function for an endofunctor on Hask, while a type constructor is an arrow function for an endofunctor on Type, as it operates on sets of types, rather than values.
P.S. As @pigworker kindly explained in comments, my understanding of Hask is all wrong. However, I wonder if any of the above applies if a different category Term is considered, in which an object is a set of values (conceivably, all possible values of some chosen type), and an arrow is a (monomorphic) function between such sets. Since a hom set would also be an object, both fmap and omap (polymorphic functions — actually, bundles of arrows) would operate on terms. At the same time, my idea is that a subcategory of Term (in which only those sets of values that correspond to actual Haskell types are considered) may be made isomorphic to Hask with an appropriately chosen functor that takes class methods, newtypes and such into account. Are there some obvious problems with a construction along these lines?
Concerning the supposed duplicate question, the answers given there do not satisfy my curiosity, for the reasons outlined above. If Hask is not the appropriate category for my inquiry, than perhaps some other choice of category could be considered. So, I think an answer should necessarily include an argument as to why a certain category is chosen to work with, in the first place.
