Example of using dependent types in Scala to verify code at compile time

Dependent types is a term that describes using values as types.  This means you can encode some properties of an object in its type. Once you do that, it allows a type checker (a compiler) to verify that the object (type) is used in a suitable way.


For a trivial example, imagine that Scala's AnyRef would have been defined as: 

AnyRef[Null <: TBoolean]


Where TBoolean is:

trait TBoolean
trait TTrue extends TBoolean
trait TFalse extends TBoolean


So we encode values 'true' and 'false' as types TTrue and TFalse


Imagine further, that all classes would automatically be encoded this way (the compiler could add the [Null <: TBoolean] part to a class definition)


While imagining, we can also imagine the compiler is enhanced so that if it sees 'null' as return value from a method returning Something, it immediately infers the return type as Something[TTrue]


Now if I define a method as:

def workWithSomething(s: Something[TFalse]) = ...


Then trying to call it with a method that returns Something[TTrue] would fail at compile time.


The result: No NullPointersException any more! (note: obviously, a smarter thing would have to remove 'null' altogether from the language, and use Option instead...)


Here's another blog post that shows a concrete example without the need for compiler magic: http://raichoo.blogspot.com/2011/08/taste-of-dependent-types-in-scala.html