Как спросить Scala, существуют ли доказательства для всех экземпляров параметра типа?

Question

Учитывая следующую функцию сложения на уровне типов чисел Пеано

      sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat

type plus[a <: Nat, b <: Nat] = a match
  case O => b
  case S[n] => S[n plus b]

скажем, мы хотим доказать теорему вроде

для всех натуральных чисел n, n + 0 = n

который, возможно, можно указать так

      type plus_n_0 = [n <: Nat] =>> (n plus O) =:= n

тогда, когда дело доходит до доказательства теоремы, мы можем легко попросить компилятор Scala предоставить доказательства в конкретных случаях

      summon[plus_n_O[S[S[O]]]]  // ok, 2 + 0 = 2

но как мы можем спросить Scala, может ли он генерировать доказательства для всех экземпляров [n <: Nat], таким образом обеспечивая доказательство plus_n_0?

Answer 1

Не думаю, что компилятор мог сразу сгенерировать что-то подобное.

Я бы предпочел предположить, что вам придется сформулировать точный тип, для которого вы пытаетесь построить термин свидетельства, затем, возможно, уменьшить проблему до более простых типов, введя какой-то принцип индукции, а затем вручную помочь компилятору доказать все базовые случаи и шаги индукции.

Вот мой взгляд на это:

      sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat

type plus[a <: Nat, b <: Nat] <: Nat = a match
  case O => b
  case S[n] => S[n plus b]

def axiom[T] = (new Object).asInstanceOf[T]

type HoldsForAllNat[P[n <: Nat]] = [n <: Nat] => (() => P[n])

given natInductionPrinciple[P[n <: Nat]](using
  base: P[O],
  step: [i <: Nat] => (P[i] => P[S[i]])
): HoldsForAllNat[P] = axiom
  
given liftCoUpperbounded[U, A <: U, B <: U, S[_ <: U]](using ev: A =:= B):
  (S[A] =:= S[B]) =
    type Surrogate[_] = Any
    ev.liftCo[Surrogate].asInstanceOf[S[A] =:= S[B]]

type NatPlusZeroEqualsNat[n <: Nat] = (n plus O) =:= n

def trivialLemma[i <: Nat]: ((S[i] plus O) =:= S[i plus O]) =
  summon[(S[i] plus O) =:= S[i plus O]]

val inductionBase: NatPlusZeroEqualsNat[O] =
  summon[(O plus O) =:= O]

val inductionStep:
  ([i <: Nat] => NatPlusZeroEqualsNat[i] => NatPlusZeroEqualsNat[S[i]]) = 
    [i <: Nat] => (p: NatPlusZeroEqualsNat[i]) =>
      given previousStep: ((i plus O) =:= i) = p
      given liftPreviousStep: (S[i plus O] =:= S[i]) =
        liftCoUpperbounded[Nat, i plus O, i, S]
      given definitionalEquality: ((S[i] plus O) =:= S[i plus O]) =
        trivialLemma[i]
      definitionalEquality.andThen(liftPreviousStep)

val proof: HoldsForAllNat[NatPlusZeroEqualsNat] =
  natInductionPrinciple(using inductionBase, inductionStep)

Он компилируется. Это не совсем удовлетворительно, потому что axiom-part вызывает исключение приведения к классу, если кто-то на самом деле пытается сгенерировать =:=-экземпляр вне доказательства, т.е. доказательство не совсем конструктивное.

---

Еще немного

1. Возьмем полиморфный тип функции type HoldsForAllNat[P[n <: Nat]] = [n <: Nat] => (() => P[n]) чтобы выразить универсальную количественную оценку.

2. Компилятор не генерирует принцип индукции для Nat. Мы просто постулируем его выполнение, обеспечивая принудительное приведение типа new Object как доказательство следующего принципа индукции:

           If
      P(0) holds, and
      whenever P(i) holds, then also P(i + 1) holds,
   then
      For all `n`, P(n) holds
   

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

3. Мы строим доказательства для базы индукции (простой) и шага индукции (тоже простые, но немного более интересные).

Некоторые замечания:

• В trivialLemma было необходимо, чтобы summonвнутри других givens не генерируют случайно рекурсивные циклы, что немного раздражает.
• Отдельный liftCo-метод для S[_ <: U] был нужен, потому что =:=.liftCo не допускает конструкторов типов с параметрами типа с ограничением сверху.