[kmill]

Functors don't include tmap. Yes, a functor maps objects from one category to objects of the second, but it does so on the sets of objects. There might not be a corresponding morphism between "a" and "f a".

The typeclass you created would be a functor along with a natural transformation from the identity functor to f. I don't think these always exist, but they do for applicative functors (pure/return).

The object mapping is reflected at the type level. "f a" is the object that "f" sends "a" to.

In Haskell, functors are all endofunctors. In math, functors can be between categories, and in such a case a -> f a might not make any sense because there are no morphisms between categories.

Using some quasi-Agda syntax, here would be a full definition of a functor between two categories. Maybe you could overload "->" so that "X -> Y" could mean "Mor X Y" for the set of morphisms between X and Y in C or D (depending on context). Curly brackets mean optional parameters, which Haskell approximates via typeclasses.

  record Functor where
    field
      C, D : Cat
      F : Ob C -> Ob D
      fmap : {X Y : Ob C} -> Mor{C} X Y -> Mor{D} (F X) (F Y)

      fmapId : {X : Ob C} -> fmap id == id
      fmapComp : {X Y Z : Ob C} -> {f : Mor X Y} -> {g : Mor Y Z}
                 -> fmap g . fmap f == fmap (g . f)

[crimsonalucard]

>and in such a case a -> f a might not make any sense because there are no morphisms between categories

In CAT the category of small categories objects are categories and morphisms are functors. Haskell types can be thought of as a small categories so I don't think this statement is correct? I'm no expert but can you clarify, the definition on wikipedia says that functors are morphisms between categories in CAT.

>There might not be a corresponding morphism between "a" and "f a".

Hmm. if haskell types make up a small category that means 'a' and 'f a' are sets. I can't imagine a case where two sets cannot have a mapping between them. Can you give a specific example?

>The typeclass you created would be a functor along with a natural transformation from the identity functor to f.

I'm confused about this. Isn't the natural transformation from identity to another category (at least for small categories) equivalent to a functor? In my head they look identical.

https://en.wikipedia.org/wiki/Natural_transformation

If you look at the commutative diagram on this page and replace F(X) and G(X) with identity X and G the natural transformation diagram looks just like a diagram for a functor.

btw I'm not an expert in haskell (let alone agda) or category theory so forgive me if the stuff I talk about is totally off.

[kmill]

Are you familiar with how the word "vector" changes meaning depending on which vector space your talking about? The same goes for "morphism," which depends on the category. In your example of "tmap : a -> f a", the only way this would make sense is as a morphism from object 'a' of the first category to an object 'f a' of the second, but this is a semantic error (a categorical error, if you will).

It is true that functors are morphisms between categories, but that's a morphism in CAT.

> I'm confused about this.

That's how these things go :-) Anyway, natural transformations are between two functors C -> D. This is an example of a 2-morphism in a 2-category. It's hard to come up with something to say other than they're just different, but think about this: a natural transformation is a consistent choice of morphisms F X -> G X (in D) for each object X (in C), but a functor needs to know where the morphisms of C go, too.

(An intuition is a natural transformations is kind of like a continuous path transforming one functor into another. This might just make things confusing, though.)

[Sniffnoy]

> Hmm. if haskell types make up a small category that means 'a' and 'f a' are sets. I can't imagine a case where two sets cannot have a mapping between them.

This is irrelevant. The question isn't, does there exist a function, it's does the functor determine one. (Given any sets A and B there is always a function from A to B unless B is empty and A is nonempty. But that's not very helpful, is it?)

> I'm confused about this. Isn't the natural transformation from identity to another category (at least for small categories) equivalent to a functor?

This doesn't mean anything. A natural transformation is from one functor F:C->D to another functor G:C->D. Not from a functor to... a category? Huh?

Also smallness is irrelevant to all of this.

[crimsonalucard]

>(Given any sets A and B there is always a function from A to B unless B is empty and A is nonempty. But that's not very helpful, is it?)

Can you clarify this? I can't define a -> f a because the functor can't determine one?

What about like for list functor?

   Int -> [Int]

Doesn't this work?

>This doesn't mean anything. A natural transformation is from one functor F:C->D to another functor G:C->D. Not from a functor to... a category? Huh?

I'm still kind of confused. Yeah you're right it doesn't make sense. But then the parent poster is saying that

    a -> f a

is the natural transformation from identity functor to f it seems off to me. It looks to me like it's just a functor from a to f a. So I'm confused with the nomenclature here. a is a category and f a is another category how is a mapping between categories a natural transformation?

Isn't this type signature the natural transformation from identity to f?:

   (a -> a) -> f a

--edit:

I think I see where I'm confused. Your last comment on the parent helped. Thanks.

[kmill]

> is the natural transformation from identity functor

Sorry I confused you here. I meant, if you had a function of that type (a -> f a), you would want a naturality relation to hold for it, like how 'return' for monads is meant to relate to fmap.

As it is, just having a map "a -> f a" is not a natural transformation.

(I think you might be confusing objects of Hask with the category Hask itself. Remember that "a -> f a" means "for each object 'a' of Hask, a function that takes an element of 'a' to an element of 'f a'. The functor is f : Hask -> Hask, an endofunctor. (In haskell, Hask is replaced by stars.) "f a" is the object of Hask that F sends "a" to.)

[Sniffnoy]

> Can you clarify this? I can't define a -> f a because the functor can't determine one?

In mathematics, it's important to distinguish between "an X such that there exists a Y" and "an X together with a Y".

We are discussing, what data determines a functor? You seem to be asserting that part of this is something you're calling tmap, which for a specific functor F would have type a -> F a.

This is mistaken; no such thing is part of the definition of a functor.

But you are confusing the issue of whether such a map is part of the definition of a functor (or is determined by the functor and so could be included in the definition with no change in the actual meaning; let's just group these two cases together as "part of the functor"), with the issue of whether such a map exists.

You pointed out that such a map exists -- as if that made it part of the functor. I pointed out that such a map does exist, but that's not helpful, because this has no relation to the functor, and that it's not part of the functor.

Your reply confuses these issues again, suggesting that because it's not part of the functor like I said (true), therefore it doesn't exist (false). No. It does exist, but it's not part of the functor.

Because it's not part of the functor -- not determined by the functor -- that means that, if you were to tack it on to the definition of the functor -- let's call this new object you're defining a functor' -- then, for any one functor, there would be multiple possible functor' that result, because of the different choices that can be made. This demonstrates that a functor and a functor' are not in fact the same thing; the functor' contains extra information that the functor does not, information that cannot be determined from the functor alone.

> Isn't this type signature the natural transformation from identity to f?: > (a -> a) -> f a

No. You are mixing things in ways that do not make sense.

Look, apologies, but I think you're in over your head here. And I'm afraid your notation is confusing the issue by mixing things inappropriately. There are too many errors here to fix individually; if you want to get this right, you're going to have to take it from the top. I could try to write an explanation that I'd hope you might understand, but my point is that that's what I'd have to do, write a whole explanation from the top. I don't see this conversation going anywhere otherwise.

[crimsonalucard]

It's fine, no need to come from the top, thanks for the explanation. I mean if you want to take it from the top I'll read it really carefully, just saying I'm grateful that you both even take the time to explain what you guys already have.

I'm out of responses here on HN so I'll respond tomorrow.

I'm not a mathematician, so yeah I am a bit over my head.

[tel]

> Hmm. if haskell types make up a small category that means 'a' and 'f a' are sets. I can't imagine a case where two sets cannot have a mapping between them. Can you give a specific example?

This is incorrect in a bunch of ways. First, Haskell types aren't truly just sets. As a simple, practical example you might have

    module Container (makeInt, Container, getValue) where
  
    data Container a 
      = Container { getValue :: a }
      deriving Functor

    makeInt :: Int -> Container
    makeInt = Container

And now we've got (externally) a type which is equivalent to the identity functor in structure, but has a weird interface which disallows tmap.

More powerfully, we're only actually interested in discussing an interface in and of itself. A type may instantiate many interfaces of varying levels of power, but each interface needs to be well-defined and well-behaved on its own. Then their compositions need to be "glued together" properly.

So even if all Haskell Functors were actually TMapFunctors, it's still important to note that the interface TMapFunctor is a sub interface to Functor which allows more operations and has more laws.

An even stronger example of this is the fact that due to the way Haskell arrows work, all Haskell Functors are actually "strong" functors in the sense that we cannot even truly specify a non-string functor.

Strength is a way that fmap and products (or, really, category tensors) interact.

    strength :: Functor f => (a, f b) -> f (a, b)
    strength (a, fb) = fmap (\b -> (a, b)) fb

This seems completely obviously possible, but it's only because we can crack open products in building general anonymous arrows. That's not supported in every category and a generic functor should not be expected to satisfy it.

[crimsonalucard]

>An even stronger example of this is the fact that due to the way Haskell arrows work, all Haskell Functors are actually "strong" functors in the sense that we cannot even truly specify a non-string functor.

Can you explain this? What is a strong functor and how does it have to do with arrows? Also what do you mean by non-string functor?

[tel]

A strong functor is one which supports the strength operation above. Haskell -> arrows being based on any lambda term are rich enough to make all Haskell functors strong. But not all functors are!

And “non-string” was just a typo.

[a1369209993]

FWIW,

  Const q a = Const q
  fmap _ (Const q) = Const q

is a perfectly viable Functor on a. Good luck converting a a into one of those.

[tel]

What's hard about that? C and D are Hask. F_Q maps objects A to objects Const Q A, and fmap takes functions in Hom(a, b) to Hom(Const Q a, Const Q b). We identify that Const Q a is just a little subset of Hask, so Hom(Const Q a, Const Q b) is Hom(Q, Q) and fmap works by mapping all functions to id_Q. Now fmapId and fmapComp are satisfied trivially.

[kmill]

a1369209993 was answering my "I don't think [natural transformations from the identity functor] always exist" with "no, they don't."

The natural transformation would be a function "a -> Const q a" for all a. There can't be a way to do this for all q that is somehow natural in q, since this would have to construct a value of q to put into the Const constructor. Worse, (even though vanilla Haskell doesn't allow it), q might be the empty type, so there might be no functions "a -> Const q a" whatsoever. I think the point of the example is that keeping q polymorphic is a simulation of the empty type.

Allowing empty types, I'm happy with the example. However, this is technically a natural transformation in Haskell:

  f :: a -> Const q a
  f x = Const undefined x

since every type contains bottom (undefined).

[tel]

Ah, I misunderstood! And yes, absolutely. An even easier example

    data Nullity a

This is a perfectly valid functor, too. Ignoring undefined, there are no values of it, but fmap cannot be used to create values of the mapped type, just manipulate them.

[crimsonalucard]

I wrote something to refute your example, but then I realized that you're right.