As an aside, in any programming language that does not support/enforce total functions, the return type `T` of any function is actually the sum type `T | Bottom`, which is to say, "this function either returns a value of type `T` or never returns to its caller at all!"
Also used as the type of expressions that do not return a value (things like `break`, `continue`, or `throw` in expression-oriented languages).
You've also got 'void' in C which comes close, but the way I see it this is also different, in the following way:
A function f: X -> void may return, but won't return any (useful) data. Mathematically there is exactly 1 such function.
A function f: X -> Bottom does not exists, if called it is impossible for it to return.
In category theory void would be the terminal object 1 and Bottom would be the initial object 0. It's called initial because there's exactly 1 function f: Bottom -> X. In programming terms this function just crashes.
Bottom has no value, so a function which “returns” bottom can not terminate.
Practically, this means it either loops forever or “breaks” e.g. panics or exits the program.
So a function f: X -> void returns the only (nameless) value in void, depending on the programming language it will return null or equivalent or it'll just return no data (but it'll still return).
A function f: X -> Bottom is different, the type Bottom has no values so it is impossible for the function to ever return. This is not always useful, but in some strongly typed you need it to assign a value to an infinite loop.
Thanks for the explanation!
The second function terminates, same as the first one, there's no real difference between them.
A bottom-returning function would be something like
function foo() { for(;;) {} }
that genuinely never terminates and thus never exits.I found it to be thorough and relatively gentle (for something as abstract as category theory anyways!)
For example, Haskell folks seem to love to make everything about Category theory but they're not necessarily the best example since Haskell is a bit weird from a Category theory standpoint (currying isn't that natural, and is in fact a deeply abstract property that only some categories have). You'll know things have gone off the deep end when you see the word Applicative.
The C# folks tend to be a bit more down to earth with their category theory (with their contravariant / covariant type parameters and SelectMany = Monad), but they write fewer articles on category theory.
Care to expand? As far as I know, the main "weird" thing about Haskell category-theoretically is seq, which is a real pain to reason about[0], but it's strange to me that you see currying as somehow a problem.
[0]: http://math.andrej.com/2016/08/06/hask-is-not-a-category/
a -> (b -> c) ≅ (a, b) -> c
Note that the two aren't equal, merely isomorphic, but Haskell has lots of synctactic sugar that lets you pretend the two are equal.
This leads to a bit of an impedance mismatch when you throw functors in the mix, as functors are a general category theory concept and therefore do not play nice with exponential objects which only some specific categories have. This is not an insurmountable problem, but it means you suddenly need a lot more category theory to do category theory in Haskell.
Without currying as first class citizen you can just lift a function f :: (a,b) -> c as follows:
fmap f :: F (a, b) -> F c
okay you've got a tuple in your functor, but those are simple enough to deal with, however if you try this with the curried variant you get:
fmap f :: F a -> F (b -> c)
okay it takes an 'F a' as input, no surprises there, but it returns you a function wrapped in your Functor, which can be tricky to deal with as most people will expect their constructs to contain data, not functions.
You can then get to grips with this by learning about Appplicative, which you'll then find out turns your functor into a lax monoidal functor. However for someone getting to grips with category theory this is a lot to process.