I hang out on reddit quite a bit, probably—or decidedly if I’m being honest—too much. Today a user mused about the nullability of Option, and of how it’s weird that there’s actually three possible states:
None, and of couse
null. Here’s the thread for anyone curious: https://www.reddit.com/r/scala/comments/n8z3lm/scala_noob_question_parameter_of_type_option_why/
Someone brought up the explicit nulls feature of Scala 3 and it got me thinking:
What if, instead of dictating that a variable can not hold null, we declare that a value must fulfil the property of not being null.
They’re quite similar but not the same. Proof-of-property can be used to implement explicit nulls but also more general flow typing. In essence, proof-of-property is less restrictive and more open-ended, but possibly also more inconvenient for the user. Implementation-wise they’re really just a form of tagged erased types.
opaque type Proof[T, P <: Property] = T def strLen(x: Proof[String, NotNull]): Int = … def sqrt(x: Proof[Double, NonNegative & NotNull]): Double = …
Obviously this becomes a bit wordy in its raw form without syntactic sugar.
These proofs could be generated automatically by the compiler as the result of an equality-check, much like what (I believe) happens for explicit nulls at the moment. The effective difference then being that instead of stripping away type information after a check, it is being added.
This scheme can work in tandem with explicit nulls by declaring that a type declaration
x: String = "hello" is actually
x: Proof[String, NotNull] = "hello".
Disclaimer: I’m aware of refinement types and GitHub - fthomas/refined: Simple refinement types for Scala. These thoughts are a play with the idea of how it could function in a more compiler-integrated setting. A lot of important stuff is left out: use-site technicalities and erasure; how a proof actually enables specific operations on a value; if and if so how they could be user-defined; etc. Also I am not formally educated so everything I’ve just said could be the worst idea ever.