Domain of identity function as the largest "collections" of all mathematical objects

50 Views Asked by At

Consider in a usual functional programming language, like Haskell, that supports parametric polymorphism. Usually, we can define a function as follows:

id :: a -> a
id x = x

It seems that we can just put whatever it is as the input of the function. My question is:

Does the domain of id function define the largest collection of mathematical objects?

In category theory, very similar ideas for other functors such as product, co-product, where no requirement on the domain is imposed. However, in category theory, we talk about functors as morphisms between specific categories. But really for functors such as id, wouldn't it be true that their domains define an actual top structure in the mathematical world, by which I mean exactly whatever we give can be accepted as being somehow contained in that top structure?

However, on the other hand, from the type theories that I, as a laymen, understand, it seems inevitable that we would end up with an infinite hierarchy of type, type of type, kind, sort, .etc. This makes me wonder what problem it would cause to have the domain of id function as the top structure of the mathematical world.

Edit1:

  1. What does it mean by the mathematical world?
  • Indeed my question is rather vague at the beginning, because first of all I am not very sure where this thought should be categorized into. So, to be more specific my thinking is mostly about programming.
  • In programming language like Haskell, even though id function is definable, but still, there are structures that cannot be accepted as the argument of id (that I believe is because of the type hierarchy artifact?). But it seems to me such universal function (that accepts whatever is given) is achievable in theory. Take a Python example: def id(x): return x. This accepts anything that I can think of as Python expression. As @David Sheard mentioned, for a given programming language, an ideal id can accept all wffs as its input, does this mean that we can actually have a type system with wff as a top "type"?
  • Coming back to mathematics, we can always for whatever category talk about the identity functor. Wouldn't we be justified to say that whatever category belongs to the domain of the identity functor in an extended definition of a functor? If this is the case, wouldn't it be possible to say this as "totality of all categories"?