4 ms·
Actually both the Haskell and type script definitions don't communicate the concept of a functor well. Especially with the way it's used. The interface only re
by crimsonalucard 7y ago
Actually both the Haskell and type script definitions don't communicate the concept of a functor well. Especially with the way it's used.
The interface only requires you to implement the mapping between morphisms, but a mathematical functor also includes mappings between the objects from one category to the next.
Additionally fmap is actually mapping
(a -> b) to (f a -> f b)
but the way it's typically used in haskell breaks this intuition. Most people see it as
((a -> b), f a) to (f b)
as a result of how it's used in FP. Technically the usages are isomorphic but using it this way blocks your intuition from fully understanding the true nature of a functor.
The following would be more a more accurate type class for a functor:
class Functor f where
fmap :: (a -> b) -> (f a -> f b)
tmap :: a -> f a
See here:
https://en.wikipedia.org/wiki/Functor https://en.wikipedia.org/wiki/Functor
Note that there are TWO axioms for functor, I added the second axiom to complete the definition.
I think the reason why tmap doesn't exist is because it's trivial? Not sure maybe some expert can pitch in as I'm certainly not an expert in haskell.
- kmill 7y agoFunctors don't include tmap. Yes, a functor maps objects from one category to objects of the second, but it does so on the sets of objects. There might not be a corresponding morphism between "a" and "f a". The typeclass you created would be a functor along with a natural transformation from the identity functor to f. I don't think these always exist, but they do for applicative functors (pure/return). The object mapping is reflected at the type level. "f a" is the object that "f" sends "a" to. In Haskell, functors are all endofunctors. In math, functors can be between categories, and in such a case a -> f a might not make any sense because there are no morphisms between categories. Using some quasi-Agda syntax, here would be a full definition of a functor between two categories. Maybe you could overload "->" so that "X -> Y" could mean "Mor X Y" for the set of morphisms between X and Y in C or D (depending on context). Curly brackets mean optional parameters, which Haskell approximates via typeclasses. record Functor where field C, D : Cat F : Ob C -> Ob D fmap : {X Y : Ob C} -> Mor{C} X Y -> Mor{D} (F X) (F Y) fmapId : {X : Ob C} -> fmap id == id fmapComp : {X Y Z : Ob C} -> {f : Mor X Y} -> {g : Mor Y Z} -> fmap g . fmap f == fmap (g . f)
- a1369209993 7y agoFWIW, Const q a = Const q fmap _ (Const q) = Const q is a perfectly viable Functor on a. Good luck converting a a into one of those.
- crimsonalucard 7y agoI wrote something to refute your example, but then I realized that you're right.
- tel 7y agoWhat's hard about that? C and D are Hask. F_Q maps objects A to objects Const Q A, and fmap takes functions in Hom(a, b) to Hom(Const Q a, Const Q b). We identify that Const Q a is just a little subset of Hask, so Hom(Const Q a, Const Q b) is Hom(Q, Q) and fmap works by mapping all functions to id_Q. Now fmapId and fmapComp are satisfied trivially.
- kmill 7y agoa1369209993 was answering my "I don't think [natural transformations from the identity functor] always exist" with "no, they don't." The natural transformation would be a function "a -> Const q a" for all a. There can't be a way to do this for all q that is somehow natural in q, since this would have to construct a value of q to put into the Const constructor. Worse, (even though vanilla Haskell doesn't allow it), q might be the empty type, so there might be no functions "a -> Const q a" whatsoever. I think the point of the example is that keeping q polymorphic is a simulation of the empty type. Allowing empty types, I'm happy with the example. However, this is technically a natural transformation in Haskell: f :: a -> Const q a f x = Const undefined x since every type contains bottom (undefined).
- tel 7y agoAh, I misunderstood! And yes, absolutely. An even easier example data Nullity a This is a perfectly valid functor, too. Ignoring undefined, there are no values of it, but fmap cannot be used to create values of the mapped type, just manipulate them.
- Sniffnoy 7y agoOther 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 ago