3 ms·

Well it is always a bit tricky to translate concepts between math and different programming languages, but null is a value not a type. Although null can be a me

Well it is always a bit tricky to translate concepts between math and different programming languages, but null is a value not a type. Although null can be a member of all/many types, but I think mathematically it's more like all those types simply have a special value called 'null', look up pointed spaces. 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.

xupybd 6y ago
Interesting. Any tips on what to read up on to get a background on this sort of math?
- jhanschoo 6y ago
  A good introduction on programming language theory should get you there. You can google around for recommendations.
- contravariant 6y ago
  This falls under Category theory, but it can be a bit tricky to find a good place to start reading. It helps if you have some mathematical background on the subject, if only to know what parts are Category theory and which are restrictions of the programming language. 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.
  - creata 6y ago
    > 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). 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/ http://math.andrej.com/2016/08/06/hask-is-not-a-category/
    - contravariant 6y ago
      Well you need to dive quite deep into Category theory before you learn what exponential objects are, which are the constructs you need to have: 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.
- mdm12 6y ago
  Bartozs Milewski wrote a book called Category Theory for Programmers and has a series of lectures on YouTube https://www.youtube.com/user/DrBartosz https://www.youtube.com/user/DrBartosz I found it to be thorough and relatively gentle (for something as abstract as category theory anyways!)
eithed 6y ago
Could you please explain the difference between f: X -> void and f: X -> Bottom? If there was a void type in C, would void be Bottom?
- masklinn 6y ago
  Conceptually, void is a singleton type: it has one value. So a function which returns void does return, just without anything useful. 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.
- contravariant 6y ago
  No the Bottom type has no values, while the void type has exactly 1 (which doesn't have a name, but you can return it by writing `return;`). 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.
  - eithed 6y ago
    Oh, so you have the distinction between `function foo() { return; }` and `function bar() {}`. From the languages I'm accustomed to, yes, second syntax is first syntax under the hood. Thanks for the explanation!
    - masklinn 6y ago
      > Oh, so you have the distinction between `function foo() { return; }` and `function bar() {}`. From the languages I'm accustomed to, yes, second syntax is first syntax under the hood. 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.

xupybd 6y ago

Interesting. Any tips on what to read up on to get a background on this sort of math?

jhanschoo 6y ago
A good introduction on programming language theory should get you there. You can google around for recommendations.
contravariant 6y ago
This falls under Category theory, but it can be a bit tricky to find a good place to start reading. It helps if you have some mathematical background on the subject, if only to know what parts are Category theory and which are restrictions of the programming language. 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.
- creata 6y ago
  > 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). 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/ http://math.andrej.com/2016/08/06/hask-is-not-a-category/
  - contravariant 6y ago
    Well you need to dive quite deep into Category theory before you learn what exponential objects are, which are the constructs you need to have: 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.
mdm12 6y ago
Bartozs Milewski wrote a book called Category Theory for Programmers and has a series of lectures on YouTube https://www.youtube.com/user/DrBartosz https://www.youtube.com/user/DrBartosz I found it to be thorough and relatively gentle (for something as abstract as category theory anyways!)

eithed 6y ago

Could you please explain the difference between f: X -> void and f: X -> Bottom? If there was a void type in C, would void be Bottom?

masklinn 6y ago
Conceptually, void is a singleton type: it has one value. So a function which returns void does return, just without anything useful. 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.
contravariant 6y ago
No the Bottom type has no values, while the void type has exactly 1 (which doesn't have a name, but you can return it by writing `return;`). 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.
- eithed 6y ago
  Oh, so you have the distinction between `function foo() { return; }` and `function bar() {}`. From the languages I'm accustomed to, yes, second syntax is first syntax under the hood. Thanks for the explanation!
  - masklinn 6y ago
    > Oh, so you have the distinction between `function foo() { return; }` and `function bar() {}`. From the languages I'm accustomed to, yes, second syntax is first syntax under the hood. 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.