Miles Sabin's type negation in practice

There was a discussion recently on scala-lang regarding how to ensure that your function returns a non-null value. Here's a solution from Miles Sabin, with my comments.

the source

// Encoding for "A is not a subtype of B"
trait <:!<[A, B]

// Uses ambiguity to rule out the cases we're trying to exclude
implicit def nsub[A, B] : A <:!< B = null
implicit def nsubAmbig1[A, B >: A] : A <:!< B = null
implicit def nsubAmbig2[A, B >: A] : A <:!< B = null

// Type alias for context bound
type |¬|[T] = {
  type λ[U] = U <:!< T
}


def foo[T, R : |¬|[Unit]#λ](t : T)(f : T => R) = f(t)

foo(23)(_ + 1) // OK
foo(23)(println) // Doesn't compile

So, how it works.

First we define the trait <:!< which looks like a negation of <:< - in Scala this notation means that one type can be, via implicits or whatever, converted into another.
Note that when you declare a type, and the type depends on two parameters, you can write the type in the infix form, e.g. String Map Int; in our case, instead of val x: <:!<[A, B] we can write val x: A <:!< B

E.g.

scala> def f(m: String Map Int) = Map("one" -> 1)
f: (m: Map[java.lang.String,Int])scala.collection.immutable.Map[java.lang.String,Int]

Why do we need a trait that does not specify any functionality? See below.

We define three implicits. The first one, implicit def nsub[A, B] : A <:!< B = null, is applicable in a case of any two types A and B; if we had just this one, the compiler would be never confused. Now we add two more to confuse the cat the compiler:

implicit def nsubAmbig1[A, B >: A] : A <:!< B = null
implicit def nsubAmbig2[A, B >: A] : A <:!< B = null

Their role is that whenever we encounter a context where <:!<[A, B] is required, and B is a supertype of A, the cat the compiler gets confused. It does not get confused if there is no such relationship between the two types. Namely, we get this error:

:27: error: ambiguous implicit values:
both method nsubAmbig1 in object $iw of type [A, B >: A]=> <:!<[A,B]
 and method nsubAmbig2 in object $iw of type [A, B >: A]=> <:!<[A,B]
 match expected type <:!<[Unit,Unit]

So, what do we do to use this feature? We declare a type function (seems like a new term) that is negation type for type T: whenever we apply this function to type U, it only allows to compile if U is not a subtype of T.

type |¬|[T] = {
  type λ[U] = U <:!< T
}

This is a kind of a type trap; let's see how we use it.

Declare a function foo that takes first parameter of type T, and second parameter a function from T to R:

def foo[T, R](t : T)(f : T => R) = f(t)

We can call it as val n24 = foo(23)(_ + 1) or as foo(23)(println). Now how do we make sure that it does not take a function that returns Unit? We have to delimit the second type parameter, R, so that it's never a Unit or a subclass of Unit. This is how we do it:

def foo[T, R : |¬|[Unit]#λ](t : T)(f : T => R) = f(t)

Now the second example, foo(23)(println), won't compile. Ta-da!

Questions?