
Hi All, I'm trying to merge in my head the concepts of: - functors from category theory; with, - the Functor typeclass in haskell. Here's what I have come up with: A Functor F in haskell is a type constructor that provides a functor map (fmap) and that maps Hask (the category of haskell types) into a category generated by the Functor. For example, Maybe maps the category of all haskell types "a" (i.e. Hask) into the category of all types of the form "Maybe a" by providing an implementation of fmap. Neglecting the fact that apparently Hask isn't a category, does this sound reasonable? I think the insight for me here is that functors in haskell are type constructors mapping Hask into another category. Is that a good way to think about it? Thanks! Dimitri

Yes, this is reasonable, but it might be useful to be a bit more explicit about the categories involved. An instance of Functor is a functor which maps objects and arrows in the category of Hask (of Haskell types and functions) to... objects and arrows in the category of Hask. It is an endofunctor. The object mapping must map a type to a type and therefore must have the kind * -> *. This means that it is a type constructor, e.g., Maybe. The arrow mapping must map arrows to arrows, which means it must map functions to functions. fmap provides this mapping and the Functor laws in Haskell are of course equivalent to the laws from category theory. And while the inclusion of bottom is problematic for Hask, it is still possible to reason about it in a "morally correct" way ( http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.pdf).

Wow, this makes it very clear! So, the object mapping is provided by the type constructor and the arrow mapping by fmap. Thanks :-) Em 29/04/14 12:35, Rein Henrichs escreveu:
Yes, this is reasonable, but it might be useful to be a bit more explicit about the categories involved.
An instance of Functor is a functor which maps objects and arrows in the category of Hask (of Haskell types and functions) to... objects and arrows in the category of Hask. It is an endofunctor. The object mapping must map a type to a type and therefore must have the kind * -> *. This means that it is a type constructor, e.g., Maybe. The arrow mapping must map arrows to arrows, which means it must map functions to functions. fmap provides this mapping and the Functor laws in Haskell are of course equivalent to the laws from category theory.
And while the inclusion of bottom is problematic for Hask, it is still possible to reason about it in a "morally correct" way (http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.pdf http://www.cse.chalmers.se/%7Enad/publications/danielsson-et-al-popl2006.pdf).
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

Right. Note, your original formulation---saying that a Functor instance maps from Hask to some subcategory of Hask (e.g. all types of the form Maybe X) was not wrong. It's just not a very useful way to think about it; as Rein described it's more useful to think of Functor instances as functors Hask -> Hask. -Brent On Tue, Apr 29, 2014 at 01:05:13PM -0600, Dimitri DeFigueiredo wrote:
Wow, this makes it very clear!
So, the object mapping is provided by the type constructor and the arrow mapping by fmap.
Thanks :-)
Em 29/04/14 12:35, Rein Henrichs escreveu:
Yes, this is reasonable, but it might be useful to be a bit more explicit about the categories involved.
An instance of Functor is a functor which maps objects and arrows in the category of Hask (of Haskell types and functions) to... objects and arrows in the category of Hask. It is an endofunctor. The object mapping must map a type to a type and therefore must have the kind * -> *. This means that it is a type constructor, e.g., Maybe. The arrow mapping must map arrows to arrows, which means it must map functions to functions. fmap provides this mapping and the Functor laws in Haskell are of course equivalent to the laws from category theory.
And while the inclusion of bottom is problematic for Hask, it is still possible to reason about it in a "morally correct" way (http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.pdf http://www.cse.chalmers.se/%7Enad/publications/danielsson-et-al-popl2006.pdf).
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

Hi All, My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap. My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category Z. As long as the "homomorphism" law holds: F(f:X->Y) = F(f):F(X)->F(Y) However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Fload yield Maybe Int and Maybe) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something? Thanks! Dimitri

Oops! Sorry for the typos! Fixing that below. Hi All, My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap. My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category D. As long as the "homomorphism" law holds: F(f:X->Y) = F(f):F(X)->F(Y) However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Double yield Maybe Int and Maybe Double) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something? Thanks! Dimitri Em 05/07/14 02:42, Dimitri DeFigueiredo escreveu:
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category Z. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Fload yield Maybe Int and Maybe) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

(Another beginner here)
That's my understanding too. Functors in Haskell have to operate on the
whole of Hask, which isn't true of functors in general. Equally, they have
to map to a subset of Haskell (although that mapping could be isomorphic to
Hask e.g. Identity Functor). It's the first restriction that's the most
problematic, since it prevents set from being a Functor. This is fixable (
http://okmij.org/ftp/Haskell/RestrictedMonad.lhs) but not part of "standard
Haskell". The second restriction basically just means you've got to do
some book-keeping to get back to the original type.
Julian
On 5 July 2014 06:51, Dimitri DeFigueiredo
Oops! Sorry for the typos! Fixing that below.
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category D. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two **distinct** types. (E.g. Int and Double yield Maybe Int and Maybe Double) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
Em 05/07/14 02:42, Dimitri DeFigueiredo escreveu:
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category Z. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Fload yield Maybe Int and Maybe) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

On Sat, Jul 05, 2014 at 11:51:10AM +0100, Julian Birch wrote:
(Another beginner here)
That's my understanding too. Functors in Haskell have to operate on the whole of Hask, which isn't true of functors in general.
As stated, this is not true: a functor F : C -> D must be defined on *all* the objects of the category C. I.e., it is still true that functors in general must operate on the whole of their domain category. I think what you are getting at is that there are (lowercase-f) functors whose domain is a *sub*category of Hask (such as the category of all types having an Ord instance, with order-preserving functions as morphisms) which cannot be extended to functors on all of Hask, and so they are not (capital-F) Functors. -Brent
Equally, they have to map to a subset of Haskell (although that mapping could be isomorphic to Hask e.g. Identity Functor). It's the first restriction that's the most problematic, since it prevents set from being a Functor. This is fixable ( http://okmij.org/ftp/Haskell/RestrictedMonad.lhs) but not part of "standard Haskell". The second restriction basically just means you've got to do some book-keeping to get back to the original type.
Julian
On 5 July 2014 06:51, Dimitri DeFigueiredo
wrote: Oops! Sorry for the typos! Fixing that below.
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category D. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two **distinct** types. (E.g. Int and Double yield Maybe Int and Maybe Double) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
Em 05/07/14 02:42, Dimitri DeFigueiredo escreveu:
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category Z. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Fload yield Maybe Int and Maybe) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

As stated, it seems precisely true. There was no implication that the
domain still be Hask.
On Sat, Jul 5, 2014 at 10:34 AM, Brent Yorgey
On Sat, Jul 05, 2014 at 11:51:10AM +0100, Julian Birch wrote:
(Another beginner here)
That's my understanding too. Functors in Haskell have to operate on the whole of Hask, which isn't true of functors in general.
As stated, this is not true: a functor F : C -> D must be defined on *all* the objects of the category C. I.e., it is still true that functors in general must operate on the whole of their domain category. I think what you are getting at is that there are (lowercase-f) functors whose domain is a *sub*category of Hask (such as the category of all types having an Ord instance, with order-preserving functions as morphisms) which cannot be extended to functors on all of Hask, and so they are not (capital-F) Functors.
-Brent
Equally, they have to map to a subset of Haskell (although that mapping could be isomorphic to Hask e.g. Identity Functor). It's the first restriction that's the most problematic, since it prevents set from being a Functor. This is fixable ( http://okmij.org/ftp/Haskell/RestrictedMonad.lhs) but not part of "standard Haskell". The second restriction basically just means you've got to do some book-keeping to get back to the original type.
Julian
On 5 July 2014 06:51, Dimitri DeFigueiredo
wrote: Oops! Sorry for the typos! Fixing that below.
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category D. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two **distinct** types. (E.g. Int and Double yield Maybe Int and Maybe Double) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
Em 05/07/14 02:42, Dimitri DeFigueiredo escreveu:
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category Z. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Fload yield Maybe Int and Maybe) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

Ah, I suppose there are several ways to interpret the original statement. Natural language is ambiguous like that. In any case, to sum up: * Mathematical functors from C to D must be defined on all objects and morphisms of C. * In Haskell, instances of the Functor class are restricted to mathematical functors whose domain and codomain are both Hask. * A consequence of Dimitri's observation is that there are even some mathematical Hask -> Hask functors which are not Functor instances! For example, any non-injective Hask -> Hask functor cannot be represented in Haskell. Consider data ConstInt a = CI Int ConstInt may "seem" like it is not injective (it maps everything to Int) but that is not quite true. In fact, it does not map everything to Int. It maps, say, Bool to ConstInt Bool, and Char to ConstInt Char. Despite being isomorphic (indeed, having exactly the same representation), ConstInt Bool and ConstInt Char are not equal types. On the other hand, a type synonym like type ConstInt a = Int really is non-injective; but it cannot be made an instance of Functor. -Brent On Sat, Jul 05, 2014 at 12:21:52PM -0700, David Thomas wrote:
As stated, it seems precisely true. There was no implication that the domain still be Hask.
On Sat, Jul 5, 2014 at 10:34 AM, Brent Yorgey
wrote: On Sat, Jul 05, 2014 at 11:51:10AM +0100, Julian Birch wrote:
(Another beginner here)
That's my understanding too. Functors in Haskell have to operate on the whole of Hask, which isn't true of functors in general.
As stated, this is not true: a functor F : C -> D must be defined on *all* the objects of the category C. I.e., it is still true that functors in general must operate on the whole of their domain category. I think what you are getting at is that there are (lowercase-f) functors whose domain is a *sub*category of Hask (such as the category of all types having an Ord instance, with order-preserving functions as morphisms) which cannot be extended to functors on all of Hask, and so they are not (capital-F) Functors.
-Brent
Equally, they have to map to a subset of Haskell (although that mapping could be isomorphic to Hask e.g. Identity Functor). It's the first restriction that's the most problematic, since it prevents set from being a Functor. This is fixable ( http://okmij.org/ftp/Haskell/RestrictedMonad.lhs) but not part of "standard Haskell". The second restriction basically just means you've got to do some book-keeping to get back to the original type.
Julian
On 5 July 2014 06:51, Dimitri DeFigueiredo
wrote: Oops! Sorry for the typos! Fixing that below.
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category D. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two **distinct** types. (E.g. Int and Double yield Maybe Int and Maybe Double) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
Em 05/07/14 02:42, Dimitri DeFigueiredo escreveu:
Hi All,
My understanding is that a functor in Haskell is made of two "maps". One that maps objects to objects that in Hask means types into types (i.e. a type constructor) And one that maps arrows into arrows, i.e. fmap.
My understanding is that a functor F in category theory is required to preserve the domain and codomain of arrows, but it doesn't have to be injective. In other words, two objects X and Y of category C (i.e. two types in Hask) can be mapped into the same object Z (same type) in category Z. As long as the "homomorphism" law holds:
F(f:X->Y) = F(f):F(X)->F(Y)
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Fload yield Maybe Int and Maybe) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Thanks!
Dimitri
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

On Sat, Jul 05, 2014 at 02:51:07AM -0300, Dimitri DeFigueiredo wrote:
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Double yield Maybe Int and Maybe Double) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Yes, that's correct. -Brent

On Sun, Jul 6, 2014 at 12:27 AM, Brent Yorgey
On Sat, Jul 05, 2014 at 02:51:07AM -0300, Dimitri DeFigueiredo wrote:
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Double yield Maybe Int and Maybe Double) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Yes, that's correct.
Why is that correct? How would you show that? -- Kim-Ee

On Sun, Jul 06, 2014 at 06:38:57AM +0700, Kim-Ee Yeoh wrote:
On Sun, Jul 6, 2014 at 12:27 AM, Brent Yorgey
wrote: On Sat, Jul 05, 2014 at 02:51:07AM -0300, Dimitri DeFigueiredo wrote:
However, I don't think there is any way this mapping of types cannot be injective in Haskell. It seems that a type constructor, when called with two distinct type will always yield another two *distinct* types. (E.g. Int and Double yield Maybe Int and Maybe Double) So, it seems that Functors in Haskell are actually more restrictive than functors can be in general. Is this observation correct or did I misunderstand something?
Yes, that's correct.
Why is that correct? How would you show that?
The fact that type constructors are injective is encoded directly into the equality rules for the type system. In the original paper on System FC, the formal system underlying GHC's core language, http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/fc-tldi.p... this is the rule labeled "Right" in Figure 2 on page 5. It says that if we have a proof that s1 s2 ~ t1 t2, then it is also the case that s2 ~ t2. (In fact, it is also the case that s1 ~ t1---this is the "Left" rule and could be referred to as "generativity" of type constructors; different type constructors always construct distinct types.) Things have changed a bit since that paper (in fact, I don't recommend reading it), but there is still a similar "right" rule used in GHC's constraint solver. -Brent
participants (6)
-
Brent Yorgey
-
David Thomas
-
Dimitri DeFigueiredo
-
Julian Birch
-
Kim-Ee Yeoh
-
Rein Henrichs