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: learning: questions

Topic: Extending "Functors" that act on a subset of Set


view this post on Zulip Davi Sales Barreira (Mar 17 2023 at 16:01):

Hello, friends. I'm trying to translate the concepts of Category Theory to Julia programming. In Julia, we have strcutcs which are containers that can be turned into a functor by defining an fmap on it. We can make structs parametric, e.g.

struct F{T} where T
 a::T
end
fmap(f, A::F) = F(f(A.a))
F(f::Function) = x::F -> fmap(f,x)

Thus, we have defined a functor F that takes types T to F{T}, and the morphism mapping is given by the fmap.
Now, sometimes we define a struct in which the subtype is fixed:

struct F****
 a::String
end
fmap(f, A::F) = F(f(A.a))

Hence, our F is not a functor in this case, since it is not properly defined for every possible object (type). Is there a canonical extension of this type of "semi"-functor? I mean, if we have a "semi-endofunctor" $F:\mathbf{Set} \to \mathbf{Set}$ where it is actually defined only in a subset of $\mathbf{Set}$. Is there a canonical extension for such thing? Is there even a name for this stuff?

view this post on Zulip Josselin Poiret (Mar 17 2023 at 16:18):

Here F (the second one) is just a type isomorphic to String. You're pretty far from a functor, you've just defined one object in the category. Basically, if F is your functor above (the first definition), you computed F(String)

view this post on Zulip Spencer Breiner (Mar 17 2023 at 16:22):

It's worth noting that you can think of a fixed type as a functor.

The type itself is most naturally represented as a functor from the terminal category String:1Type{\tt String}:{\bf 1\to Type} (rather than a functor TypeType\bf Type \to Type).

But then you can compose with the unique map to get back a "constant" functor Type1Type\bf Type \to 1 \to Type

view this post on Zulip Josselin Poiret (Mar 17 2023 at 16:23):

iiuc that composite would be written

struct F{T} where T
 a::String
end

although i don't know anything about julia

view this post on Zulip Spencer Breiner (Mar 17 2023 at 16:24):

That looks right to me

view this post on Zulip Spencer Breiner (Mar 17 2023 at 16:25):

F**** would be the functor 1Type\bf 1\to Type, i.e., just another type.

view this post on Zulip Ralph Sarkis (Mar 17 2023 at 16:26):

Spencer Breiner said:

But then you can compose with the unique map to get back a "constant" functor Type1Type\bf Type \to 1 \to Type

But this sends any functions on strings to the identity function, which I guess is not what Davi is defining. The functor should send any function between strings to itself.

view this post on Zulip Spencer Breiner (Mar 17 2023 at 16:32):

I like Julia a lot, but I do get frustrated by the lack of types on the functions.

I suppose what you're describing would be the inclusion of the endomorphism monoid of String, and the implicit typing on says it should accept a string A.a and return a string (the input to F).

view this post on Zulip Spencer Breiner (Mar 17 2023 at 16:33):

You can still map constantly through the identity function, but you're right that this is not the fmap that Davi defined.