Как доказать принцип взрыва (ex falso sequitur quodlibet) в Scala?

Question

Как мне показать, что что-либо следует из значения типа без конструкторов в Scala? Я хотел бы сделать сопоставление с шаблоном для значения и сделать так, чтобы Scala сообщала мне, что ни один шаблон не может соответствовать, но я открыт для других предложений. Вот краткий пример того, почему это было бы полезно.

Доказательство негативов

В Scala можно определять натуральные числа на уровне типа, например, с помощью кодирования Пеано.

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

Из этого мы можем определить, что значит число быть четным. Ноль является четным, и любое число два больше, чем четное число, также является четным.

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]]]

Из этого мы можем показать, что, например, два является четным:

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

Но я не могу показать, что это даже не так, хотя компилятор не может сказать мне, что ни Base ни Step может обитать по типу.

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

Компилятор с радостью скажет мне, что ни один из приведенных мною случаев невозможен с ошибкой pattern type is incompatible with expected typeно оставив match block empty будет ошибкой компиляции.

Есть ли способ доказать это конструктивно? Если пустое совпадение с образцом - путь, я бы принял любую версию Scala или даже макрос или плагин, если я все еще получаю ошибки для пустых совпадений с образцом, когда тип обитаем. Может быть, я лаю не на том дереве, соответствует ли шаблон неправильной идее - может ли EFQ показываться другим способом?

Примечание. Доказательство того, что один является нечетным, можно сделать с помощью другого (но эквивалентного) определения четности, но это не главное. Краткий пример того, почему может понадобиться EFQ:

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

Answer 1

Ex falso quodlibet означает "из противоречия следует все, что следует". В стандартной кодировке Карри-Ховарда Nothing соответствует лжи, поэтому следующая простая функция реализует принцип взрыва:

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

Компилируется, потому что Nothing настолько всемогущ, что его можно заменить чем угодно (A).

Тем не менее, это ничего не покупает, потому что ваше первоначальное предположение, что из

There is no proof for `X`

это следует из того

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

это неверно. Это неверно не только для интуиционистской / конструктивной логики, но и в целом: как только ваша система может считать, существуют истинные утверждения, которые не могут быть доказаны, поэтому в каждой непротиворечивой системе с натуралами Peano должны быть некоторые утверждения X такой, что X не может быть доказано (Геделем), и их отрицаниеX => _|_ также не может быть доказано (последовательностью).

Кажется, что здесь вам понадобится некая "лемма обращения" (в смысле "Типов и языков программирования" Пирса), ограничивающая способы построения терминов определенных типов, но я не вижу что-нибудь в системе типов Scala, которое предоставит вам кодировку на уровне типа такой леммы.

Answer 2

Это может быть невозможно доказать ex falso для произвольного необитаемого типа в Scala, но все еще можно доказать, что Even[Succ[Zero]] => Nothing, Мое доказательство требует лишь небольшой модификации вашего Nat определение, чтобы обойти отсутствующую функцию в Scala. Вот:

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))