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.
Davi Sales Barreira (Feb 11 2023 at 17:31):Hello, everyone. I've studyied Category Theory for a while now, and I've also read books (Bartoz and Brendan Fong) on Category Theory for Programming. I've been trying to "port" the theoretical claims to the Julia programming language. Since Julia is not a pure FP language as Haskell, I have been battling to properly impor the concepts.
One of my hardships have benn with Functors. In the Julia community, the definition of a functor in Julia is a bit all over the place.
I think I might have been able to unpack some of my own confusion, and I'd love some feedback to know if I'm moving in the right direction.
So in programming, our types are the objects and functions are morphisms. In Julia we have types and functions, so this is fine. But what about a value? Lile 1? If I understood correctly, a value is isomorphic to a function (morphism) going from the terminal type (object) to type T of fthe value, for example, 1 is equivalent to 1(::Nothing)::Int, where Nothing is a terminal type in Julia.
Ok, so values are functions and we can compose them with "ordinary" functions which would be the same as applying the function to a value x, e.g. f (x) == f ( x()).
Now, in Julia we have structs that define new types. For example:
struct MyType
x
end
I want to define a functor that takes every type and turns them into type MyType.
F(T::Type) = MyType
F(f::Function) = a::MyType -> F(f(a.x))
Ok, so my functor acts on types to types, and on functions to functions. And it commutes properly... Yet,
since values are also functions, I need to define how F(x) works. The simplest idea would be
F(x) = MyType(x) which creates an instance of type MyType. But this is not right, because
x is a function from Nothing to a type T. So F(x) must also be a function, and moreover, a
function of type MyType to MyType. So here is how it would be:
F(x) = a::MyType -> MyType(x).
I guess this is all correct now, but a bit useless. I don't want F(x) to be this weird function.
Here is what I then thought, which I'd like some feedback.
Since MyType has acutally only field x, this means that every instance of this type is actually
isomorphic to a function a ::MyType-> MyType(x). Hence, we can drop all this shinnenigans and just write
F(x) = MyType(x)...
Is this correct? Please let me know if any of my understanding is incorrect. Eventhough I've been studying this for a while, things still are convoluted from time to time.
Ryan Wisnesky (Feb 11 2023 at 17:47):What is the corresponding construction in Haskell? Is it "existential types"?
Davi Sales Barreira (Feb 11 2023 at 17:57):I don't actually know :|
Ryan Wisnesky (Feb 11 2023 at 18:15):I would suggest formulating it in Haskell first, then trying to port that over to Julia, because I think some of the issues you are grappling with are actually type theoretic in nature and already defined/solved in type theory. In particular, your construction of trying to "hide" arbitrary types behind a fixed type is very reminiscent of existential types, and as such care is required - it's easy to go too far and get unsoundness (see "strong/transulcent sums" for an example of how existential can be taken too far), so I'd definitely suggest a port rather than re-invention.
Davi Sales Barreira (Feb 11 2023 at 18:19):The thing is that I actually am not proficient in Haskell. When reading Bartoz book, my goal of porting to Julia is exactly in trying to understand things better.
Ryan Wisnesky (Feb 11 2023 at 18:34):What is your background, btw? I can try to find references on existential types that are appropriate for it (e.g. if you are familiar with locally cartesian closed categories, existential types can be thought of in that context)
Ryan Wisnesky (Feb 11 2023 at 18:37):a general reference is https://stackoverflow.com/questions/10753073/whats-the-theoretical-basis-for-existential-types
Davi Sales Barreira (Feb 11 2023 at 18:45):Applied Mathematics. I've been studying Category Theory since the beginning of last year.
Don't know Type Theory. I'm a PhD student, and my thesis is in trying to apply Category Theory.
Ryan Wisnesky (Feb 11 2023 at 18:55):existential types may be a tough place to start; you're defining a type, MyType, that admits an injection from all types, including itself. Similar problems are found with universal types, which admit projections to all types, requiring the machinery of locally cartesian closed categories to define. Perhaps try defining functors for products, co-products, function types, stuff like that first?
Davi Sales Barreira (Feb 11 2023 at 18:57):Yeah, the whole self-referential thing is a bit overwhealming. I was able to define the other functors already. I was trying to figure this one out now.
David Egolf (Feb 11 2023 at 18:58):I don't know if this is relevant to you: https://algebraicjulia.github.io/Catlab.jl/dev/
Ryan Wisnesky (Feb 11 2023 at 19:00):heh, I think I understand. Yeah, the issue here probably isn't Julia or Haskell, but that existential (and universal) types are hard to define, period. To understand papers in categorical type theory, this is a good baseline (semantics of STLC in a CCC): https://www.cl.cam.ac.uk/teaching/1617/L108/catl-notes.pdf . If you can read that paper, you can tackle the kinds of papers that would tell you how to define your functor (eg https://dl.acm.org/doi/10.1145/44501.45065)
Davi Sales Barreira (Feb 11 2023 at 19:42):David Egolf said:
I don't know if this is relevant to you: https://algebraicjulia.github.io/Catlab.jl/dev/
Not really :(