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: What are "structs" in Category Theory?


view this post on Zulip Davi Sales Barreira (Mar 10 2023 at 11:43):

Hello, friends. I'm trying to interpret Category Theory within Julia language. One common construction we have is that of a struct. For example:

struct F
  a::Int
  b::String
end

I was previously interpreting such structs as a Functor once I've defined an fmap function and overloaded the constructor to send types to the F type, like this:

F(T::Type) = F
fmap(f,A::F) = F(f(A.a),f(A.b))

Is there other interpretation for what these struct are within Category Theory? I haven't figured out what is the equivalent of a struct in Haskell, perhaps this would clear somethings.

view this post on Zulip Ralph Sarkis (Mar 10 2023 at 11:50):

Maybe a product?

view this post on Zulip Davi Sales Barreira (Mar 10 2023 at 12:00):

Ralph Sarkis said:

Maybe a product?

Makes sense... Although it is encapsulating the product within another type (object), which is necessary to dispatch functions. What about the fact that fields are named? Do you see any technicallities on that?

view this post on Zulip Ralph Sarkis (Mar 10 2023 at 12:09):

I think F is the object which is the product of Int and String.

I don't what to do about names. If you define F' with different names, then F and F' will be the same product, but they are different in the way you use it. Maybe if the possible tokens (a and b are what I call tokens) are described in your category in some way, then you could try something.

view this post on Zulip Nathanael Arkor (Mar 10 2023 at 14:51):

You can index the product by the set of field names, though this is equivalent to simply indexing by natural numbers.

view this post on Zulip Ryan Wisnesky (Mar 10 2023 at 16:49):

Via the Curry Howard Lambek Correspondence, https://en.wikipedia.org/wiki/Curry–Howard_correspondence#Curry–Howard–Lambek_correspondence, structs/projections become products, tagged unions/case statements become co-products, lambdas and application become exponentials, and recursive/co-recursive types (typically) become the initial algebras/final co-algebras for polynomial endofunctors. As usual, for products/coproducts you can have binary ones, or use a set of labels to index the field names.

view this post on Zulip Keith Elliott Peterson (Mar 11 2023 at 09:52):

"Structs" aka record types, are (co)presheaves.

view this post on Zulip Ryan Wisnesky (Mar 11 2023 at 18:33):

I'd probably set that a set of values on the same struct defines a co-presheaf out of a category with products (the struct/type itself).