4 ms·

This is probably a dumb question but isn't this just null by another name?

• guerrilla 6y ago
  Null is a value, not a type. Think of the bottom type more like the empty set rather than the number/address zero although there are similarities to both in type theory.
  • draw_down 6y ago
    In some languages null is the value and the name of the type, JS for example.
• StreamBright 6y ago
  It is not a dumb question. Null has many drawbacks compare to bottom types. In many languages is is part of other types so that your code happily compiles with a function that has String as an input parameter and gets a null. This is why you see in Java a lot of null checking usually. In ML languages people decided to do better and started to use Some / None, etc. which needs to be handled explicitly, so you do not forget null checking accidentally.
• contravariant 6y ago
  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.
• aliceryhl 6y ago
  No because the type bottom has no valid values, whereas null as one valid value, namely null. A function that returns bottom must loop forever, because there are no values that it would be valid for the function to return.
  • Sharlin 6y ago
    Loop forever, or, more commonly in actual use cases, terminate via a nonlocal return (eg. exceptions, `longjmp`, `abort`). 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).
    • aliceryhl 6y ago
      I mean, `T | Bottom` is the same type as `T`, so what you're saying is vacuously true.