This is yet another Haskell-through-category-theory question.
Let's take something simple and well-known as an example. fmap
?
So fmap :: (a -> b) -> f a -> f b
, omitting the fact that f
is actually a Functor
. As far as I understand, (a -> b) -> f a -> f b
is nothing but a syntax sugar for the (a -> b) -> (f a -> f b)
; hence conclusion:
(1) fmap
is a function producing a function.
Now, Hask contains functions as well, so (a -> b)
and, in particular, (f a -> f b)
is an object of the Hask (because objects of the Hask are well-defined Haskell types - a-ka mathematical sets - and there indeed exists set of type (a -> b)
for each possible a
, right?). So, once again:
(2) (a -> b)
is an object of the Hask.
Now weird thing happens: fmap
, obviously, is a morphism of the Hask, so it is a function, that takes another function and transform it to a yet another function; final function hasn't been applied yet.
Hence, one needs one more Hask's morphism to get from the (f a -> f b)
to the f b
. For each item i
of type a
there exists a morphism apply_i :: (f a -> f b) -> f b
defined as \f -> f (lift i)
, where lift i
is a way to build an f a
with particular i
inside.
The other way to see it is GHC
-style: (a -> b) -> f a -> f b
. On the contrast with what I've written above, (a -> b) -> f a
is mapping to the regular object of the Hask. But such a view contradicts fundamental Haskell's axiom - no multivariate functions, but applied (curried) alternatives.
I'd like to ask at this point: is (a -> b) -> f a -> f b
suppose to be an (a -> b) -> (f a -> f b) -> f b
, sugared for simplicity, or am I missing something really, really important there?
is
(a -> b) -> f a -> f b
suppose to be an(a -> b) -> (f a -> f b) -> f b
, sugared for simplicity
No. I think what you're missing, and it's not really your fault, is that it's only a very special case that the middle arrow in (a -> b) -> (f a -> f b)
can be called morphism in the same way as the outer (a -> b) -> (f a -> f b)
can. The general case of a Functor class would be (in pseudo-syntax)
class (Category (──>), Category (~>)) => Functor f (──>) (~>) where
fmap :: (a ──> b) -> f a ~> f b
So, it maps morphisms in the category whose arrows are denoted ──>
to morphisms in the category ~>
, but this morphism-mapping itself is just plainly a function. Your right, in Hask specifically function-arrows are the same sort of arrows as the morphism arrows, but this is mathematically speaking a rather degenerate scenario.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With