Hacker News new | ask | show | jobs
by danbruc 3618 days ago
You could say all Java reference types are sum types - either a real instance of that type or a null reference. A function returning a string guarantees that you either get a string or a null reference, I don't think that has (necessarily) implications for soundness. But then again the theory of type systems is not something I have a deep understanding of so I may actually be wrong.
1 comments
catnaroek 3618 days ago
> You could say all Java reference types are sum types - either a real instance of that type or a null reference.

That's not true. There are two fundamental differences:

(0) Options can nest. Nullability doesn't nest.

(1) Options are manipulated by pattern matching (or direct application of their induction principle, that is, Haskell's `maybe` function). In Java, you just assume a nullable variable isn't null, and if it is, well, you get an exception.

link
danbruc 3618 days ago
That is certainly a limitation but I don't think that makes this view wrong. I also can not have List<int> but that does not mean List<T> is not a generic list type just because there are some constraints on what T can be.
link
catnaroek 3618 days ago
In the vast majority of situations, when a Java programmer has a value of type `Foo`, he or she expects it to be a non-`null` reference. Having a `null` one is a possibility, but it's an error. Dictating that reference types are in actuality option types is creating a gigantic mismatch between the prescriptive semantics of the language and the actual model inside the heads of programmers, which is the worst sin a language's semantics can commit. Witness the flame wars about whether it would be a good idea to remove some undefined behavior from C.
link
danbruc 3618 days ago
That is certainly true, but the point was whether nullabilty has any bearing on soundness. I just tried to argue that the fact that a reference may be a null reference does not (necessarily) defy soundness - the compiler guarantees that you get an instance or a null reference and that is exactly what happens at runtime.
link
catnaroek 3618 days ago
If you take the view that object references are options, then it's plain unsound to manipulate object references as though they weren't options! `NullPointerException` is just a dynamic plug on a static type safety hole.

This blog post (I'm not the author) explains the issue (item 3) very well: http://www.sebastiansylvan.com/post/language-design-deal-bre...

link
danbruc 3618 days ago
Maybe I (or you or both of us) have a wrong understanding of soundness. I understand it as follows - the specification of a programming language (or its implementation) is sound if the guarantees made a compile time hold at runtime for all inputs. The guarantee for calling a method on a reference in Java is that you either invoke that method or a NullPointerException gets thrown in case the reference is a null reference.

After thinking about it again, unless you made an error in the specification or implementation, every programming language should actually be sound. You can always weaken your guarantees until they (trivially) hold at runtime. But that actually worries me a bit, soundness suddenly seems not such a useful concept. Maybe because I am wrong with my understanding?

Note that this also possibly contradicts what I wrote previously, I may not have thought carefully enough about some of the things.

link