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.
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 = ???
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))