Is there a formalization of "non-parametric functors"? · learning: questions

So, I've been trying to program so of the Category Theory programming concepts taught by Bartosz, but using Julia. One construction got me puzzled. In Haskell, we define functors by defining things like:

data Maybe a = Nothing | Just a
fmap...

By defining the fmap we get Maybe to be a functor. The thing is, the Maybe functor takes a type T to a type
Maybe T. Now, in Julia, we can construct this Maybe functor with a parametric struct:

struct Just{T}
 a::T
end
struct Nothing end
Maybe{T} = Union{Just{T}, Nothing}
fmap...

Yet, in Julia there is another possible construction. We can define a "functor-like" thing as the following:

struct F
 a
end
fmap(f::Function, x::F) = F(f(x.a))

Such construction is actually called "functor" by programmers... But it seems that it is not an actual functor in terms of Category Theory.
The reason for me saying this is that F takes types (sets) T to F and not to F{T}. Hence, if we think of types as sets, the type F would not be an actual set, as it seems to contain all other types, including itself...

Is there any formal treatment of such construction? Is this actually a functor and I'm with the wrong interpretation?

Jencel Panic (Jun 10 2023 at 06:26):

Don't know Julia, but this looks like a functor that is parametrized by the type of a.

Jencel Panic (Jun 10 2023 at 06:26):

In particular it looks like the identity functor i.e. just a box that contains a value.

Davi Sales Barreira (Jun 10 2023 at 12:11):

It would not be the identity because it actually takes a type T to a type F.

Jencel Panic (Jun 10 2023 at 14:22):

Don’t understand where this T comes from, to me it looks like it takes an argument of type F (called x)

Jencel Panic (Jun 10 2023 at 16:28):

Perhaps you mean to say that the type is polymorphic, but it is de facto polymorphic, it is just not annotated as such.

Jencel Panic (Jun 10 2023 at 16:30):

Jencel Panic (Jun 10 2023 at 19:53):

Actually, they are both recursive types, they don’t contain themselves, I think.

Davi Sales Barreira (Jun 10 2023 at 21:13):

Let me try to clarify my issue. You probably already know how functors are defined in programming, but I'll just recap how I do it in Julia:

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

We can interpret the thing above as a functor F, where an element of type T is taken to an element of type F{T}. For example, an element of type Int becomes of type F{Int}. This example seems to fit nicely with the notion of an endofunctor acting on the category of sets. We just think of types as sets, hence, type Int is just the set of integers, and type F{Int} can be thought of as the set of elements (F, i) where i where i are integers. In other words, the sets Int and F{Int} are isomorphic.

struct F
 a
end
fmap(f::Function, x::F) = F(f(x.a))
F(f::Function) = x-> fmap(f, x)

This is very similar, but now this "functor" takes elements of type Int to type F, and not to F{Int}. But note that this "functor" also takes elements of type String to the type F... Hence, F is not isomorphic to Int. In fact, F actually is larger than all previous types, since for any x of type T we have a representation in F, which would be (F, x).
Thus, what I was thinking was that F is not an endofunctor in Set anymore.

Jencel Panic (Jun 11 2023 at 20:40):

Jencel Panic (Jun 11 2023 at 20:45):

I don't think that the fact that F is larger than some other types raises any contradictions.

Jencel Panic (Jun 11 2023 at 22:04):

If we have to formalize this functor in set theory we might say that there exist a general type, like that contains all values of all other types, like the typeObject in Java (note it contains all types', values, it doesn't contain the types themselves) and that the functor is implicitly parametrized by that type.

James Deikun (Jul 17 2023 at 06:11):

This doesn't seem like a functor because fmap(f,x) produces "type errors" rather than valid results when x isn't originally from the argument type of f. It breaks the abstraction of the source category rather than respecting it.

Jencel Panic (Jul 18 2023 at 11:37):

Yes, it's an untyped functor. In general, functions that may raise errors are impartial functions and those cannot be modeled in CT.

Jencel Panic (Jul 18 2023 at 11:38):

Davi Sales Barreira (Jul 18 2023 at 14:35):

Nathaniel Virgo (Jul 18 2023 at 14:41):

Jencel Panic (Jul 18 2023 at 19:06):

Sorry, bad phrasing, I meant that functors specifically can only be modeled with total functions.

Morgan Rogers (he/him) (Jul 18 2023 at 19:38):

The definition of partial function also lifts to a definition of partial functor!

Jencel Panic (Aug 01 2023 at 08:32):

I guess this answers Davi's original question: What kind of functor is this --- a partial functor