3 ms·
Other commenters have already pointed out some of the ways you're confused about categories, but let me explicitly answer your question of, why doesn't the func
by Sniffnoy 7y ago
Other commenters have already pointed out some of the ways you're confused about categories, but let me explicitly answer your question of, why doesn't the functor include the mapping on the objects and not just on the morphisms?
The answer is it does. In this context, the types are the objects. So if F is your functor, then F itself -- which does not have a type, but has kind * -> * -- is the mapping on the objects.
- crimsonalucard 7y agoSo you're saying the constructor of the type itself is a -> f a. Right? I think I get it. Thanks.
- Sniffnoy 7y agoNo. It's not a -> f a. It's * -> *. There is no a -> f a here. You are simply mistaken in thinking that any such thing is part of the definition of a functor.
- kmill 7y agoI put this in another comment, but I think you're thinking 'a' is a category, but it's an object in a category. The type for a functor (in Haskell) is Hask -> Hask, which is represented by the star notation Sniffnoy uses. That is, it sends objects of Hask to objects of Hask. The object mapping for a functor in Haskell is defined by its "data" or "type" definition. The notation "a -> f a" means a function that sends elements of 'a' to elements of 'f a', where 'a' is an object of the category Hask. (Functors don't look into the objects at the element level.)
- crimsonalucard 7y agoThanks for the clarification. I think I get it despite the incorrect notation. You guys are talking about some sort of type of types?
- kmill 7y agoYeah, the "type of types" is called a kind in Haskell https://wiki.haskell.org/Kind https://wiki.haskell.org/Kind https://en.wikipedia.org/wiki/Kind_(type_theory) https://en.wikipedia.org/wiki/Kind_(type_theory) Caveat: there seems to be some reason not to think of kinds as actually being the types of datatypes, but I don't understand why that is.