Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

`(a -> b) -> (c -> d)` in Haskell?

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?

like image 800
Zazeil Avatar asked Dec 21 '18 14:12

Zazeil


Video Answer


1 Answers

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.

like image 89
leftaroundabout Avatar answered Nov 15 '22 10:11

leftaroundabout