Search code examples
scalatype-theorysubtyping

Subtype relation of Option type


I recently learned a bit about scala's subtype system, and I got curious about Option type and its subtypes' relationship. I learned that following statement is true.

if A <: B, then (A => C) >: (B => C)

Also, I understood that A <: B means that there exists some instance of B that cannot be an instance of A. If I apply these to Option type, then I get following results. I'll skip ⱯA. notation for convenience.

  1. Nothing <: Option[A], so Option[A] => string <: Nothing => string
  2. I cannot think of any instance of Nothing => string that is not an instance of Option[A] => string, so Nothing => string <: Option[A] => string
  3. Nothing => string (<: and >:) Option[A] => string, so Nothing => string is effectively equal to Option[A] => string in subtyping
  4. Option[A] => string <: Some[A] => string, so Nothing => string <: Some[A] => string
  5. Some[A] <: Nothing

Since I strongly doubt the result is correct, I think something went wrong in the middle. Can anybody explain what's happening here?


Solution

  • I think you are mixing up some things. I take it that A -> B should mean A => B, a function from A to B. Next, Nothing[A] doesn't exist, only Nothing which is a bottom type in Scala (sub-type of all types). But probably you mean the object None (with type None.type) which is a sub-type of Option.

    Then your first assumption would be true:

    implicitly[None.type <:< Option[_]]   // ok
    implicitly[(Option[_] => String) <:< (None.type => String)]  // ok
    

    I rephrase your second assumption:

    I cannot think of any instance of None.type => String that is not an instance of Option[A] => String, so (None.type => String) <: (Option[A] => String)

    This assumption is wrong:

    implicitly[(None.type => String) <:< (Option[_] => String)]
    
    error: Cannot prove that None.type => String <:< Option[_] => String.
           implicitly[(None.type => String) <:< (Option[_] => String)]
                     ^
    

    It might be difficult to imagine, because None does not add any methods that are not part of the interface of Option. But take the typical example of general animal (as Option) and particular animal (as None).

    trait Animal  // aka Option
    object Dog extends Animal { def bark() = "bark!" }
    object Cat extends Animal { def purr() = "purr!" } // aka None
    

    Your second assumption would mean that (Cat => String) <: (Animal => String). If this was true, the following would be possible:

    val fun: Animal => String = { c: Cat.type => c.purr }  // doesn't compile
    

    let's force that:

    val fun: Animal => String = { c: Cat.type => c.purr } .asInstanceOf[Animal => String]
    fun(Dog)  // try run this
    
    java.lang.ClassCastException: Dog$ cannot be cast to Cat$
      ... 64 elided