• PortugalSpaceMoon@infosec.pub
    link
    fedilink
    arrow-up
    10
    ·
    1 year ago

    I’m not sure I agree that Void is a bottom type. If so, void-functions would never be able to return/terminate. Java’s void is probably more of a unit type.

      • Aloso@programming.dev
        link
        fedilink
        arrow-up
        4
        ·
        1 year ago

        No it’s not, it is 100% a unit type (except it’s not really a type, since you can only use it as return type and nowhere else)

        • BatmanAoD@programming.dev
          link
          fedilink
          arrow-up
          5
          ·
          1 year ago

          It’s not possible to instantiate or assign, which is more like a never type than a unit; and it is not possible to define new types with the same properties, which is also more like bottom than unit. But you’re right that it’s not actually a true never type since it can’t represent function divergence.

          I think the truth is just that Java’s type system isn’t very mathematically disciplined.

          • Aloso@programming.dev
            link
            fedilink
            arrow-up
            1
            ·
            edit-2
            1 year ago

            It’s not possible to instantiate or assign, which is more like a never type than a unit

            Actually, this is because void is not a type, it is just a keyword, a placeholder used instead of the return type when a function doesn’t return anything.

            If it were a bottom type, that would mean that a method returning void must diverge, which is simply not true.

            Also, if it were a bottom type, it would be possible to write an “unreachable” method

            void unreachable(void bottom) {
                return bottom;
            }
            

            Even though it couldn’t be called, it should be possible to define it, if void was a bottom type. But it is not, because void isn’t a bottom type, it’s no type at all.

            • BatmanAoD@programming.dev
              link
              fedilink
              arrow-up
              1
              ·
              1 year ago

              The post has been edited; it looks like someone on reddit made essentially the same point. You’re right of course that void isn’t a true type in Java, but the post now also discusses Void, which I suppose just shows how void infects the type system despite not being a type.