12

In Haskell, the Functor typeclass functor is defined as follows (see e.g. Haskell wiki):

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b 

As far as I understand (please correct me if I am wrong), such a functor can only have as target category a category constructed using a type constructor, e.g. [], Maybe, etc. On the other hand, one may think of functors having any category as target of a functor, e.g. the category of all Haskell types. For example, Int could be an object in the target category of a functor, not just Maybe Int or [Int].

What is the motivation for this restriction on Haskell functors?

  • 4
    Simplicity? Haskell doesn't have first class type functions so all functions are really just type constructors. – jozefg Jul 20 '14 at 4:07
  • 2
    @jozefg: Pardon my ignorance: what are "first class type functions"? – Giorgio Jul 20 '14 at 9:31
  • 4
    So in that function we're tossing around an f right? And in your scenario, f should be just like a normal Haskell function and map types to types. In Haskell, the only things that are allowed to have the kind * -> * are type constructors. Type families are more general, but they must always be fully applied – jozefg Jul 20 '14 at 13:00
  • This question is related. – Ptharien's Flame Jul 20 '14 at 17:23
  • @jozefg: I occasionally think about this question again and again. I suppose the Haskell restriction does not affect the expressive power of functors. For example, suppose that we have a functor that is isomorphic to the list functor, but does not map, say, Int -> [Int] but Int -> <fancy type using no type constructor>. Then I guess one could prove that <fancy type using no type constructor> is isomorphic to [Int]. So choosing objects that are defined using a type constructor is just convenient and does not sacrifice the expressive power. – Giorgio Aug 13 '15 at 21:12
1

There's no restriction at all! When I started learning the category-theoretic basis for type constructors, this very point confused me as well. We'll get to that. But first, let me clear up some confusion. These two quotes:

such a functor can only have as target category a category constructed using a type constructor

and

one may think of functors having any category as target of a functor, e.g. the category of all Haskell types

show that you are misunderstanding what a functor is (or at the very least, you are misusing terminology).

Functors do not construct categories. A functor is a mapping between categories. Functors bring objects and morphisms (types and functions) in the source category to object and morphisms in the target category.

Note that this means a functor is really a pair of mappings: a mapping on objects F_obj and mapping on morphisms F_morph. In Haskell, the object part F_obj of the functor is the name of the type constructor (e.g. List), while the morphism part is the function fmap (it is up to the Haskell compiler to sort out which fmap we are referring to in any given expression). Thus, we cannot say that List is a functor; only the combination of List and fmap is a functor. Still, people abuse notation; programmers call List a functor, while category theorists use the same symbol to refer to both parts of the functor.

Furthermore, in programming, almost all functors are endofunctors, that is, the source and target category are the same - the category of all types in our language. Let's call this category Type. An endofunctor F on Type maps a type T to another type FT and a function T -> S to another function FT -> FS. This mapping must of course obey the functor laws.

Using List as an example: we have a type constructor List : Type -> Type, and a function fmap: (a -> b) -> (List a -> List b), that together form a functor. T

There is one final point to clear up. Writing List int does not create a new type of lists of integers. This type already existed. It was an object in our category Type. List Int is simply a way to refer to it.

Now, you're wondering why a functor can't map a type to, say, Int or String. But, it can! One just has to use the identity functor. For any category C, the identity functor maps every object to itself and morphism to itself. It is straightforward to verify this mapping satisfies the functor laws. In Haskell, this would be a type constructor id : * -> * that maps every type to itself. For example, id int evaluates to int.

Moreover, one can even create constant functors, that map all types to a single type. For example, the functor ToInt : * -> *, where ToInt a = int for all types a, and maps all morphisms to the integer identity function: fmap f = \x -> x

  • Thanks for your answer, this question is over two years old. "Functors do not construct categories.": I did not say that. I said that functors map two categories, where the target category must have the form f a, where f is, as far as I know, a type constructor. From what I remember from category theory, this must be some kind of canonical representation (initial object in a category of categories? maybe I am misusing the terminology.) Anyway, I will read your answer carefully. Many thanks. – Giorgio Oct 5 '16 at 16:56
  • @Giorgio whoops, I didn't notice how old it was haha. It just showed up in "unanswered questions". I'm not sure what you mean by "canonical representation". As far as I know (and I could be wrong here), there is not a relationship between functors and initial/terminal objects. – gardenhead Oct 5 '16 at 17:51
  • I mean this: en.wikipedia.org/wiki/Initial_algebra (see Use in computer science). In Haskell (most) functors are defined on an algebraic data types. The target object of such a functor is an initial algebra. The initial algebra is isomorphic to the set of terms built using the value constructors. E.g., for lists, [] and :. I meant this by canonical representation. – Giorgio Oct 5 '16 at 20:49
  • Yeah, I know what an initial object is, and that inductive datatypes are initial objects in the F-algebra of a category. You're correct that many type-constructors are defined inductively. But this is not strictly necessary. For example, the functor (_, int) that takes a type a to the product type (a, int) and a function f : 'a -> 'b to g : 'a * int -> 'a * int is not inductive. – gardenhead Oct 5 '16 at 22:52
  • Did you mean: "takes ... a function f : 'a -> 'b to g : 'a * int -> 'b * int? – Giorgio Oct 6 '16 at 6:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.