Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: theory: applied category theory

Topic: functors in Haskell


view this post on Zulip Kale Evans (Sep 01 2021 at 06:36):

Anyone here who is familiar with haskell have an example of an instance of a functor whose second argument doesn't have to be type constructor for a collection type?

Essentially, I am trying to see if a functor as defined in haskell is only relevant over collections, as opposed to the category theoretic definition, which of course works across all categories.

In other words, It appears the functor in Haskell only moves you from a particular category to the category of containers of the objects of the first Category.

view this post on Zulip Kale Evans (Sep 01 2021 at 06:36):

I hope this makea sense

view this post on Zulip Jules Hedges (Sep 01 2021 at 09:17):

"Collection" is a bit of an informal word and almost anything can look like a collection if you squint hard enough, but in general you can build examples from function types, for example the reader monad a -> x and the continuation monad (x -> a) -> a (both for fixed a)

view this post on Zulip Nick Hu (Sep 01 2021 at 12:56):

I believe Functor in Haskell only allows you to describe endofunctors of Hask, or something like that

view this post on Zulip Kale Evans (Sep 02 2021 at 03:42):

@Nick Hu Yeah, I've read that a Functor in Haskell is really only an endofunctor.

view this post on Zulip Kale Evans (Sep 03 2021 at 04:52):

0ACD58F1-7FBB-4381-A7CE-D60438F8A436.jpg

view this post on Zulip Kale Evans (Sep 03 2021 at 04:52):

^ I'm trying to understand applicatives and having a tough time. Could someone please explain to me how the above functions are equivalent?

view this post on Zulip Alex Gryzlov (Sep 03 2021 at 09:46):

Presumably foo : a -> b -> c, x : F a, y : F b, then pure foo : F (a -> b -> c), pure foo <*> x : F (b -> c), pure foo <*> x <*> y : F c

view this post on Zulip Kale Evans (Sep 04 2021 at 02:53):

@Alex Gryzlov this is certainly due to my lack of Haskell knowledge, and the order of evaluations for statements I suppose, but I guess I'm getting stuck on the second step. I get pure will apply F to it's argument, but how are you reaching the 2nd step? I.e why is pure foo <*> x : F (b -> c)? <*> takes a a first parameter of type f (a -> b) and foo doesn't fit that signature

view this post on Zulip Kale Evans (Sep 04 2021 at 02:54):

Nor does pure foo

view this post on Zulip Kale Evans (Sep 04 2021 at 04:54):

Or can you apply pattern matching to the signatures? i.e is it true that F ( a-> b -> c) = F (a -> (b -> c)) and so then we can use b -> c as the argument b in <*>? I thought Haskell was exact with the type signatures, so wasn't sure if you could substitute a signature for a function where there is a signature of a single type. If that makes sense

view this post on Zulip Henry Story (Sep 04 2021 at 05:47):

Perhaps this post by Bartosz Milewski on Applicative Functors will help? https://bartoszmilewski.com/2017/02/06/applicative-functors/

view this post on Zulip Alex Gryzlov (Sep 04 2021 at 22:22):

Kale Evans said:

Or can you apply pattern matching to the signatures? i.e is it true that F ( a-> b -> c) = F (a -> (b -> c)) and so then we can use b -> c as the argument b in <*>? I thought Haskell was exact with the type signatures, so wasn't sure if you could substitute a signature for a function where there is a signature of a single type. If that makes sense

It's not pattern matching, but simply a convention of right-associativity.

view this post on Zulip Alex Gryzlov (Sep 04 2021 at 22:24):

A function type is still a type so it can be substituted.

view this post on Zulip Nick Hu (Sep 06 2021 at 15:36):

Just to clarify a bit further, what @Alex Gryzlov means is that the function arrow -> associates to the right. So when you write a -> b -> c you implicitly mean a -> (b -> c) (always)

view this post on Zulip Nick Hu (Sep 06 2021 at 15:37):

Function application associates to the left, so when you write f x y you implicitly mean (f x) y

view this post on Zulip Nick Hu (Sep 06 2021 at 15:43):

As to your original question, here is a skeleton of the answer (fill in the ???) in equational proof style

liftA2 f x y
= { definition of liftA2 (https://hackage.haskell.org/package/base-4.15.0.0/docs/src/GHC-Base.html#liftA2) }
((<*>) (fmap f x)) y
= { <*> infix }
fmap f x <*> y
= { ??? }
pure f <*> x <*> y

view this post on Zulip Kale Evans (Sep 08 2021 at 04:33):

@Nick Hu So fmap f x <*> y :: f c? Using g :: a-> (b->c), I arrive as fmap g :: f a -> f(b->c), then fmap g x :: f(b->c), and finally fmap g x <*> y :: f c

view this post on Zulip Nick Hu (Sep 08 2021 at 07:30):

You can't work out everything just by eyeballing the types (but this is usually good intuition). Every well-formed equation has a term with the same type on both its left and right side. And certainly just because two terms have the same type does not mean that they are equal, e.g. True :: Bool, and False :: Bool, but we would have big problems if True = False

view this post on Zulip Nick Hu (Sep 08 2021 at 07:32):

But fmap isn't just any old function (a -> b) -> f a -> f b; it's a special one that has to satisfy certain equations (called the functor laws). Similarly for pure and <*> too, and this is how you derive the answer to your question.

view this post on Zulip ctt (Feb 14 2022 at 06:47):

I'm trying to figure out what category theory functors correspond to in Haskell. If List is a Functor, does that mean List is a functor? or is its fmap one? or its fmap f (for some f)?

view this post on Zulip Mike Shulman (Feb 14 2022 at 06:54):

A functor in category theory consists of an action on objects and an action on morphisms. The type constructor List is the action on objects of such a functor, while fmap is the corresponding action on morphisms, and fmap f is the image of f under that action on morphisms.

view this post on Zulip ctt (Feb 14 2022 at 06:57):

Got it, thanks