The first thing to notice is that functors in category theory are not functors in Haskell.
In category theory a functor from one category means that you can move objects and arrows from one category into another, such that they keep behaving in the same way as they did in the original category. Note that there’s no notion of type or function there as category theory treats these ideas on more abstract level than a programming language does.
In Haskell functor means for a construct that can upgrade a type into something, and then upgrade a function acting on that type to something. There’s no requirement that it keeps behaving the same afterwards. Also sometimes it’s not required that you can lift any object.
Examples of ‘haskell’ functors you may have:
The functor on the first item of a pair, where some ‘b’ is on the right side. There’s a similar “functor” for the second item of a pair.
(a → c) → (a,b) →(c,b)
The functor on the codomain of a function:
(a → c) → (c → b) → (a → b)
The functor on the list:
(a → b) → List a → List b
Functors in Haskell means for structures where you can “apply” types into a function. Eg. List (toString . (+1)) would produce List Number → List String and the thing you probably get is it adds 1 to each number inside list and stringifies each, giving you list of strings. Actually in Haskell you’d do fmap (show . (+1)) and you can inhabit the type [Integer] -> [String] with it.
An example of a category theory functor: A functor from category C to a pair category (C,C). If you take object from C, there’s object in (C,C), eg. for a there is (a,a). Likewise you give it an arrow a → b, you get arrow (a,a) → (b,b). And these things behave in same way they behaved in the original category, except that after the functor they’re in a category that’s larger by a square.
In category theory the functor is a stepping-stone to describe natural transformation. Also you get a concept of adjoint functors. The aforementioned functor to pair category gives you products and sums for any category, as adjoints that you can take from the functor.
Most languages’ endofunctors are reasonable functors. Only Haskell is strange, and only because its semantics are extremely quirky. For this reason, many people will tend to work in a “platonic Hask” rather than in Haskell’s actual category of types. The upshot of this is that many Haskellers believe their code to be proven correct when it has only merely type-checked.
In other MLs, functors go between modules; we may thus imagine each module as a sort of category, and functors as sending modules to other modules. Modules don’t exactly have the inner structure of a category, though. This is just as well, as the typical ML (in fact, all of the ones I know of!) have weak type systems not capable of expressing functors between genuine categories in toto, just categories which are small enough to fit into the type system containing it. (It may sound like I am being petty here, but I do have to go to untyped languages just to express ∞-categories.)
While I like the invocation of the Hollywood Principle, functors are really about composition, not just embedding. It’s very cool that we can write a minimal object and embed it within a richer API, but cooler that we can compose our minimal object out of other, even smaller subobjects.
The first thing to notice is that functors in category theory are not functors in Haskell
In category theory a functor from one category means that you can move objects and arrows from one category into another, such that they keep behaving in the same way as they did in the original category. Note that there’s no notion of type or function there as category theory treats these ideas on more abstract level than a programming language does.
In Haskell functor means for a construct that can upgrade a type into something, and then upgrade a function acting on that type to something. There’s no requirement that it keeps behaving the same afterwards. Also sometimes it’s not required that you can lift any object.
I’m aware that there is a difference between Haskell’s functors and category theory’s functors.
IIRC, the connection is that Haskell’s functors are really endofunctors in the category Hask of Haskell types, and arrows are then functions.
The functor laws should make sure arrows are mapped correctly (i.e., behave in the same way regarding composition).
Please correct me if I’m wrong, I’m still learning.
Incorrect technically and practically.
Could you expand on this?
I admit that the title of my post is not technically correct, but I don’t see where its contents disagree with what you wrote.
Haskell people tend to pay attention to functor laws, but this is not necessarily what happens in the code because the Haskell environment doesn’t require the functor laws. Likewise the constructs can be useful even if the laws didn’t always satisfy. Also I remember at least one dude who has stated that hask is not a category.
Functors are not comparable to frameworks. You don’t give up or invert any sort of control there. If things happening here would be sufficient for that interpretation, you could think of any higher order function as a framework because you pass a function in. Although it matches in that you pass a thing to call. But I think being a framework would require you to at least write the phone number down, let function complete, and then arbitrarily call it when you’re already forgotten about the whole thing.
you could think of any higher order function as a framework because you pass a function in.
I see.
That makes total sense.
But I think being a framework would require you to at least write the phone number down, let function complete, and then arbitrarily call it when you’re already forgotten about the whole thing.
Isn’t that what happens in asynchronous effect monads?
Incorrect technically and practically.
The first thing to notice is that functors in category theory are not functors in Haskell.
In category theory a functor from one category means that you can move objects and arrows from one category into another, such that they keep behaving in the same way as they did in the original category. Note that there’s no notion of type or function there as category theory treats these ideas on more abstract level than a programming language does.
In Haskell functor means for a construct that can upgrade a type into something, and then upgrade a function acting on that type to something. There’s no requirement that it keeps behaving the same afterwards. Also sometimes it’s not required that you can lift any object.
Examples of ‘haskell’ functors you may have:
The functor on the first item of a pair, where some ‘b’ is on the right side. There’s a similar “functor” for the second item of a pair.
The functor on the codomain of a function:
The functor on the list:
Functors in Haskell means for structures where you can “apply” types into a function. Eg.
List (toString . (+1))would produceList Number → List Stringand the thing you probably get is it adds 1 to each number inside list and stringifies each, giving you list of strings. Actually in Haskell you’d dofmap (show . (+1))and you can inhabit the type[Integer] -> [String]with it.An example of a category theory functor: A functor from category C to a pair category (C,C). If you take object from C, there’s object in (C,C), eg. for
athere is(a,a). Likewise you give it an arrowa → b, you get arrow(a,a) → (b,b). And these things behave in same way they behaved in the original category, except that after the functor they’re in a category that’s larger by a square.In category theory the functor is a stepping-stone to describe natural transformation. Also you get a concept of adjoint functors. The aforementioned functor to pair category gives you products and sums for any category, as adjoints that you can take from the functor.
Most languages’ endofunctors are reasonable functors. Only Haskell is strange, and only because its semantics are extremely quirky. For this reason, many people will tend to work in a “platonic Hask” rather than in Haskell’s actual category of types. The upshot of this is that many Haskellers believe their code to be proven correct when it has only merely type-checked.
In other MLs, functors go between modules; we may thus imagine each module as a sort of category, and functors as sending modules to other modules. Modules don’t exactly have the inner structure of a category, though. This is just as well, as the typical ML (in fact, all of the ones I know of!) have weak type systems not capable of expressing functors between genuine categories in toto, just categories which are small enough to fit into the type system containing it. (It may sound like I am being petty here, but I do have to go to untyped languages just to express ∞-categories.)
While I like the invocation of the Hollywood Principle, functors are really about composition, not just embedding. It’s very cool that we can write a minimal object and embed it within a richer API, but cooler that we can compose our minimal object out of other, even smaller subobjects.
I’m aware that there is a difference between Haskell’s functors and category theory’s functors. IIRC, the connection is that Haskell’s functors are really endofunctors in the category
Haskof Haskell types, and arrows are then functions. The functor laws should make sure arrows are mapped correctly (i.e., behave in the same way regarding composition). Please correct me if I’m wrong, I’m still learning.Could you expand on this? I admit that the title of my post is not technically correct, but I don’t see where its contents disagree with what you wrote.
Haskell people tend to pay attention to functor laws, but this is not necessarily what happens in the code because the Haskell environment doesn’t require the functor laws. Likewise the constructs can be useful even if the laws didn’t always satisfy. Also I remember at least one dude who has stated that hask is not a category.
Functors are not comparable to frameworks. You don’t give up or invert any sort of control there. If things happening here would be sufficient for that interpretation, you could think of any higher order function as a framework because you pass a function in. Although it matches in that you pass a thing to call. But I think being a framework would require you to at least write the phone number down, let function complete, and then arbitrarily call it when you’re already forgotten about the whole thing.
I see. That makes total sense.
Isn’t that what happens in asynchronous effect monads?