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

Question

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

Проверка отрицательных значений

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

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 пустым, это будет ошибка компиляции.

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

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

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

Answer 1

Может быть невозможно доказать 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))

Answer 2

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 => _|_`

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

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