Modular calculi

[loewenheim]

I implemented a small strawman proposal for making calculi modular. It works pretty nicely with current dotty (the experimental compiler that will eventually become Scala 3).

import Calculi._

trait Inference


case class Inf1(i: Int) extends Inference
case class Inf2(s: String) extends Inference
case class Inf3(i: Int, j: Int) extends Inference

case class Proof[+C <: Inference](val inf: C, val subProofs: Vector[Proof[C]])

object Calculi {
  type Partial = Inf1 | Inf2
  type Full = Partial | Inf3
  type PartialProof = Proof[Partial]
  type FullProof = Proof[Full]
}

object PartialProof {
  def apply(inf: Partial, subProofs: Vector[Proof[Partial]]): Proof[Partial] = Proof(inf, subProofs)
}

object FullProof {
  def apply(inf: Full, subProofs: Vector[Proof[Full]]): Proof[Full] = Proof(inf, subProofs)
}

object removeInf3 {
  def apply[C <: Inference](proof: Proof[C | Inf3]): Proof[C | Inf1] = proof.inf match {
    case inf: Inf3 =>
      Proof(Inf1(inf.i), proof.subProofs.map(apply))
    case inf: C =>
      Proof(inf, proof.subProofs.map(apply))
  }
}