scalatype-systems

How can I have a negation type in Scala?

I want to do something like this:

def iDontLikeStrings(arg: Not[String]) = {....}

Basically, this should compile:

iDontLikeStrings(23) 
iDontLikeStrings(true)

And this should NOT compile:

iDontLikeStrings("hello")
Solution

  • Here is my implementation (see gist):

    Step 1: Encoding to capture A is not a subtype of B

    trait NotSubTypeOf[A, B]

    Note: We can use infix notation to write A NotSubTypeOf B instead of NotSubTypeOf[A, B]

    Step 2: Evidence for any two arbitrary types A and B, A is not a subtype of B

    implicit def isSub[A, B]: A NotSubTypeOf B = null

    Step 3: Define ambigious implicits to trigger compile error in case A is a subtype of B (or A =:= B)

    implicit def iSubAmbig1[A, B >: A]: A NotSubTypeOf B = null
implicit def iSubAmbig2[A, B >: A]: A NotSubTypeOf B = null

    Step 4: Define a type-lambda for the negation type: 

    type Not[T] = {
  type L[U] = U NotSubTypeOf T
}

    With kind-projector, this can be made much more readable.

    Step 5: Done!

    def iDontLikeStrings[A: Not[String]#L](a: A) = {
  println(a)
}

iDontLikeStrings(23)   // compiles
iDontLikeStrings(true) // compiles
//iDontLikeStrings("hello") // does not compile

    The compiler error message for the last line can be made better in Scala 2.12 which addresses SI-6806.

    Also, all of this is built into Shapeless.