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

Thank you for your interest!

We will contact you as soon as possible.

Send us a message

Oops, something went wrong
Please try again or contact us by email at info@tikalk.com