How to prove the principle of explosion (ex falso sequitur quodlibet) in Scala?

Question

How do I show that anything follows from a value of a type with no constructors in Scala? I would like to do a pattern match on the value and have Scala tell me that no patterns can match, but I am open for other suggestions. Here is a short example of why it would be useful.

Proving negatives

In Scala it is possible to define the natural numbers on a type level, e.g. with Peano encoding.

sealed trait Nat
sealed trait Zero extends Nat
sealed trait Succ[N <: Nat] extends Nat

From this we can define what it means for a number to be even. Zero is even, and any number two more than an even number is also even.

sealed trait Even[N <: Nat]
sealed case class Base() extends Even[Zero]
sealed case class Step[N <: Nat](evenN: Even[N]) extends Even[Succ[Succ[N]]]

From this we can show that e.g. two is even:

val `two is even`: Even[Succ[Succ[Zero]]] = Step(Base())

But I am unable to show that one is not even, even though the compiler can tell me that neither Base nor Step can inhabit the type.

def `one is odd`(impossible: Even[Succ[Zero]]): Nothing = impossible match {
  case _: Base => ???
  case _: Step[_] => ???
}

The compiler will happily tell me that none of the cases I've given are possible with the error pattern type is incompatible with expected type, but leaving the match block empty will be a compile error.

Is there any way to prove this constructively? If empty pattern matches is the way to go - I'd accept any version of Scala or even a macro or plugin, as long as I still get errors for empty pattern matches when the type is inhabited. Maybe I am barking up the wrong tree, is a pattern match the wrong idea - could EFQ be shown in some other way?

Note: Proving that one is odd could be done with another (but equivalent) definition of evenness - but that is not the point. A shorter example of why EFQ could be needed:

sealed trait Bottom
def `bottom implies anything`(btm: Bottom): Any = ???

Malvia

In your Step, shouldn't it extend Even[Succ[Succ[N]]]? Otherwise, it's just a proof that 2 is even. – Landman

@BrianMcCutchon You are correct and it should be fixed now. Thank you for your sharp eyes and keen mind! – Malvia

Answer 1

It may be impossible to prove ex falso for an arbitrary uninhabited type in Scala, but it's still possible to prove that Even[Succ[Zero]] => Nothing. My proof requires only a small modification to your Nat definition to work around a missing feature in Scala. Here it is:

import scala.language.higherKinds

case object True
type not[X] = X => Nothing

sealed trait Nat {
  // These dependent types are added because Scala doesn't support type-level
  // pattern matching, so this is a workaround. Nat is otherwise unchanged.
  type IsZero
  type IsOne
  type IsSucc
}
sealed trait Zero extends Nat {
  type IsZero = True.type
  type IsOne = Nothing
  type IsSucc = Nothing
}
sealed trait Succ[N <: Nat] extends Nat {
  type IsZero = Nothing
  type IsOne = N#IsZero
  type IsSucc = True.type
}

type One = Succ[Zero]

// These definitions should look familiar.
sealed trait Even[N <: Nat]
sealed case class Base() extends Even[Zero]
sealed case class Step[N <: Nat](evenN: Even[N]) extends Even[Succ[Succ[N]]]

// A version of scalaz.Leibniz.===, adapted from
// https://typelevel.org/blog/2014/07/02/type_equality_to_leibniz.html.
sealed trait ===[A <: Nat, B <: Nat] {
  def subst[F[_ <: Nat]](fa: F[A]): F[B]
}

implicit def eqRefl[A <: Nat] = new ===[A, A] {
  override def subst[F[_ <: Nat]](fa: F[A]): F[A] = fa
}

// This definition of evenness is easier to work with. We will prove (the
// important part of) its equivalence to Even below.
sealed trait _Even[N <: Nat]
sealed case class _Base[N <: Nat]()(
  implicit val nIsZero: N === Zero) extends _Even[N]
sealed case class _Step[N <: Nat, M <: Nat](evenM: _Even[M])(
  implicit val nIsStep: N === Succ[Succ[M]]) extends _Even[N]

// With this fact, we only need to prove not[_Even[One]] and not[Even[One]]
// will follow.
def `even implies _even`[N <: Nat]: Even[N] => _Even[N] = {
  case b: Base => _Base[Zero]()
  case s: Step[m] =>
    val inductive_hyp = `even implies _even`[m](s.evenN) // Decreasing on s
    _Step[N, m](inductive_hyp)
}

def `one is not zero`: not[One === Zero] = {
  oneIsZero =>
    type F[N <: Nat] = N#IsSucc
    oneIsZero.subst[F](True)
}

def `one is not _even` : not[_Even[One]] = {
  case base: _Base[One] =>
    val oneIsZero: One === Zero = base.nIsZero
    `one is not zero`(oneIsZero)
  case step: _Step[One, m] =>
    val oneIsBig: One === Succ[Succ[m]] = step.nIsStep
    type F[N <: Nat] = N#IsOne
    oneIsBig.subst[F](True)
}

def `one is odd`: not[Even[One]] =
  even1 => `one is not _even`(`even implies _even`(even1))

Landman

This is fascinating. Can you add a proof of even(N)⇒not(even(succ(N)))? What about not(even(N))⇒even(succ(N))? I'm having hard time constructing those. – Grant

@n.m. Maybe I'll try those later. If it helps, I proved it in Coq first, then translated that into Scala, using the Coq Print command to view the generated code for the trickier theorems. ===.subst is roughly equivalent to Coq's eq_ind. The translation was the hardest part. – Landman

Answer 2

Ex falso quodlibet means "from contradiction, anything follows". In the standard Curry-Howard encoding, Nothing corresponds to falsehood, so the following simple function implements the principle of explosion:

def explode[A]: Nothing => A = n => n

It compiles, because Nothing is so omnipotent that it can be substituted for anything (A).

However, this does not buy you anything, because your initial assumption that from

There is no proof for `X`

it follows that

There must be proof for `X => _|_`

is incorrect. It's incorrect not only for intuitionistic/constructive logics, but in general: as soon as your system can count, there are true statements that cannot be proved, so in every consistent system with Peano naturals there must be some statements X such that X cannot be proved (by Goedel), and their negation X => _|_ also cannot be proved (by consistency).

It seems that what you would need here is rather some kind of "inversion lemma" (in the sense of Pierce's "Types and Programming Languages") that limits the ways in which terms of certain types can be constructed, but I don't see anything in Scala's type system that would provide you a type-level encoding of such a lemma.

Incognito

Thank you so much for your answer. It was not my intention to insinuate that the law of excluded middle is true in general. In my attempted proof above, the compiler happily tells me that my cases are impossible - so on some level it already knows that falsehood has happened. The same proof should work in intuitionistic logic, or in e.g. Agda. The type Bottom should be isomorphic to Nothing since they have the same constructors. But Nothing gets magical properties from the compiler by being the subtype of everything, which is the property explode uses. – Malvia

@Malvia You're again mixing up levels of object-language and meta-language. The statement "There is proof of X" is not a negation of *"There is proof of ` X => _|_"*. Those are two meta-theoretic statements about two different types X` and X => _|_ being inhabited or not. That's a completely different realm from where the LEM lives. The LEM (for this particular case) would we a term of type [X].(X \/ (X => _|_)), where \/ is conjunction (corresponds to something roughly like the Either-type constructor), and [X] is universal quantification over type-variable X. – Incognito

@Malvia I hope you can recognize that the statement "Step(Base()) is of type Even[Succ[Succ[Zero]]]" and the statement "Bob is sitting in front of his computer and cannot find a Scala term of type Even[Succ[Zero]] => Nothing" live in completely different realms. – Incognito

@Malvia And another remark: No, a Bottom type is not the same thing as simply a type without any constructors or values. From the point of view of Curry-Howard-Lambek isomorphism, it's exactly the universal property that matters: for the Bottom-type, it has to hold that for every other X there is a unique morphism from Bottom to X, i.e. it must be the initial object. The def explode above proves that Nothing has this universal property. – Incognito

@Malvia And in the second comment, you see what happens if you mix up meta-language with the object language: I forgot a backtick right after _|_, now the markdown is messed up, and an entire sentence is gray... – Incognito