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: If types are objects, that what are values?

Davi Sales Barreira (Sep 18 2022 at 14:29):

Hey everyone. I've been reading Bartoz "Category Theory for Programmers" and I've been trying to code things in Julia. So far it has been a truly great experience, since Julia is more "grounded" than Haskell, and it has enabled me to truly understand the concepts, since I cannot just copy the code.
Yet, this has led me to some (weird) questions. One of the is the following. In programming, one thinks of types as the objects, and functions as morphisms. Now, to implement a functor we implement a parametric struct, and an fmap that tells how to map a function from type T->M to a type F T -> FM. Here is an example in Julia:

struct F{T}
  x::T
  y::T
end

F(T::Type) = F{T}
fmap(f::Function, a::F{T}) where T = F(f(a.x), f(a.y))

# Note that from fmap we can do
F(f::Function) = a -> fmap(f,a);

Great, so in the example above, F(T) acts on object T and returns an object of type F{T}. Also, we've overloaded F
so that it now can take a function as input and returns a new function Ff which one can check that satisfies the definition of a functor.

All good. But there is one caveat. I've actually defined more than a simple functor. I've also defined how to select a "value" of type F{T}.
If I do F(1,2) I get a value of type F{Int}... Now, what is going on here in terms of Category Theory? How am I to interpret this F(1,2), which actually is an "element" of F{Int}.

My guess is that this F(1,2) is something like a natural transformation ... Is it? And if so, between which functors? How should one interpret it?

Spencer Breiner (Sep 18 2022 at 18:07):

Hi @Davi Sales Barreira

In this kind of a story, individual elements are usually represented as maps out of the terminal object $\top$. In this case, your constructor is a function $\tt Int\times Int\to F\{Int\}$. The pair corresponds to a map $(1,2): \top \to \tt Int \times Int$, and the composite is your element $\tt F(1,2)$.

For a natural transformation, you need to provide an arrow for every type, but here you've just got one for $\tt Int$. A typical example would be something like the "diagonal" function $\tt t::T\mapsto F(t,t)$, which makes sense for any type $\tt T$. In Julia, you would implement this using a where:

diag(t::T) where T = F(t)

Note that sometimes the where statement can be implicit in the type arguments, e.g.,

proj1(p::F) = p.x

vs.

proj2(p::F{T} where T) = p.y

Davi Sales Barreira (Sep 18 2022 at 22:10):

Thanks for the answer @Spencer Breiner ! when you say that the composite is my element F(1,2), what do you mean?

Davi Sales Barreira (Sep 18 2022 at 22:27):

Just so I see if I understood.

struct T
    x::Int
    y::Int
end

T(a)

When we created such struct, Julia implicitly created a "value" constructor, i.e.
a function T(a::Tuple{Int,Int}) that returns values of type T.
Since a value a::Tuple{Int,Int} is just a function a(x::Terminal)::Tuple{Int,Int},
then T(a) is actually a function composition T ∘ a in the category $\mathbf{Types}$.

Thus, we are able to talk about T(1,2) as a morphism (function), without requiring to talk
about elements of sets.

Is this correct?

Spencer Breiner (Sep 18 2022 at 23:26):

That's it. There are subtleties, like the distinction between a value x::X and a function x() that returns an X, but that's the basic idea