scalaunit-typecurry-howard

Is there a Scala function of type `Nothing => A`? Or how to construct one?

Through Curry-Howard isomorphism Scala's Unit corresponds to logical true and Nothing to logical false. The fact that logical true is implied by anything is witnessed by a simple function that just discards the argument:

def toUnit[A](x: A): Unit = { }

Is there a function that witnesses the fact that logical false implies anything, that is a function of type Nothing => A? Or is there an idiomatic way how to construct one?

One can always do something like

def fromNothing[A](n: Nothing): A = throw new RuntimeException();

but this is just ugly - it doesn't use the fact that Nothing has no values. There should be a way how to do it without exceptions.

Solution

  • You may do that 

    def emptyFunction[A]: Nothing => A = {n => n}

    or

    def emptyFunction[A](n: Nothing): A = n