Ghosts of departed proofs in scala (https://github.com/matt-noonan/gdp-paper/releases)

GDP.scala

trait Coercible[A, B] {
  def coerce(a: A): B
}

def coerce[A, B](a: A)(implicit coerceAB: Coercible[A, B]): B = {
  coerceAB.coerce(a)
}

trait Newtype[+T] {
  val value: T
}

implicit def newtypeCoercibleToType[T, NT <: Newtype[T]]: Coercible[NT, T] = new Coercible[NT, T] {
  def coerce(a: NT): T = {
    a.value
  }
}

def deriveCoercionToNewtype[T, NT <: Newtype[T]](ctr: T => NT): Coercible[T, NT] = new Coercible[T, NT] {
  def coerce(a: T): NT = {
    ctr(a)
  }
}

// The Named constructor should not be exported to avoid forging invalid instances
case class Named[Name, A](value: A) extends Newtype[A]
type ~~[A, Name] = Named[Name, A]

implicit def namedCoercible[Name, A]: Coercible[A, Named[Name, A]] = deriveCoercionToNewtype[A, Named[Name, A]](Named[Name, A])

case class name[A, T](x: A) {
  def apply[Name](k: (A ~~ Name) => T): T = {
    k(coerce[A, Named[Name, A]](x))
  }
}

case class Defn()

def defn[F, A](a: A)(implicit proof: Coercible[A, A ~~ F]): A ~~ F = {
  // ???
  proof.coerce(a)
}

trait The[D, A] {
  def the(d: D): A
}

def the[D, A](d: D)(implicit theDA: The[D, A]): A = {
  theDA.the(d)
}

implicit def newtypeTheUnwrap[T, NT <: Newtype[T]]: The[NT, T] = new The[NT, T] {
  def the(d: NT): T = d.value
}

def deriveTheToNewtype[T, NT <: Newtype[T]](ctr: T => NT): The[T, NT] = new The[T, NT] {
  def the(a: T): NT = {
    ctr(a)
  }
}

implicit def namedThe[Name, A]: The[A, Named[Name, A]] = deriveTheToNewtype[A, Named[Name, A]](Named[Name, A])

sealed trait Ordering
case object LT extends Ordering
case object EQ extends Ordering
case object GT extends Ordering

def orderInt(l: Int)(r: Int): Ordering = {
  if (l < r) { LT } else if (l > r) { GT } else { EQ }
}

type Comparator[A] = A => A => Ordering

// Just like Named SortedBy should not be exported either
case class SortedBy[Comp, A](value: A) extends Newtype[A]

implicit def sortedByCoercible[Comp, A]: Coercible[A, SortedBy[Comp, A]] = deriveCoercionToNewtype[A, SortedBy[Comp, A]](SortedBy[Comp, A])
implicit def sortedByThe[Comp, A]: The[A, SortedBy[Comp, A]] = deriveTheToNewtype[A, SortedBy[Comp, A]](SortedBy[Comp, A])

def sortByUnsafe[A](comp: Comparator[A])(xs: List[A]): List[A] = {
  xs.sortWith { (l: A, r: A) =>
    comp(l)(r) match {
      case LT      => true
      case EQ | GT => false
    }
  }
}

def mergeByUnsafe[A](comp: Comparator[A])(l: List[A])(r: List[A]): List[A] = {
  def go(xs: List[A])(ys: List[A]): List[A] = {
    (xs, ys) match {
      case (Nil, ys_) => ys_
      case (xs_, Nil) => xs_
      case (x :: xs_, y :: ys_) =>
        comp(x)(y) match {
          case GT => y :: go(x :: xs_)(ys_)
          case _  => x :: go(xs_)(y :: ys_)
        }
    }
  }
  go(l)(r)
}

def sortBy[A, Comp](comp: Comparator[A] ~~ Comp)(xs: List[A]): SortedBy[Comp, List[A]] = {
  coerce[List[A], SortedBy[Comp, List[A]]](
    sortByUnsafe(the[Comparator[A] ~~ Comp, Comparator[A]](comp))(xs)
  )
}

def mergeBy[A, Comp](comp: Comparator[A] ~~ Comp)(xs: SortedBy[Comp, List[A]])(
  ys:                    SortedBy[Comp, List[A]]): SortedBy[Comp, List[A]] = {
  val theSortedBy = the[SortedBy[Comp, List[A]], List[A]](_)

  coerce[List[A], SortedBy[Comp, List[A]]](
    mergeByUnsafe[A](the[Comparator[A] ~~ Comp, Comparator[A]](comp))(theSortedBy(xs))(theSortedBy(ys)))
}

def minimum_01[Comp, A](xs: SortedBy[Comp, List[A]]): Option[A] = {
  the[SortedBy[Comp, List[A]], List[A]](xs) match {
    case Nil    => None
    case x :: _ => Some(x)
  }
}

def orderingExample[Comp](xs: List[Int])(ys: List[Int])(lt: Comparator[Int] ~~ Comp): List[Int] = {
  val xsSorted = sortBy(lt)(xs)
  val ysSorted = sortBy(lt)(ys)
  println(minimum_01(ysSorted))
  println(minimum_01(xsSorted))
  the[SortedBy[Comp, List[Int]], List[Int]](mergeBy(lt)(xsSorted)(ysSorted))
}

val list1: List[Int] = List[Int](4, 5, 2)
val list2: List[Int] = List[Int](1, 3, 9)

val result: List[Int] = name[Comparator[Int], List[Int]](orderInt)(orderingExample(list1)(list2))

print(result) // = List(1, 2, 3, 4, 5, 9)

Proof.scala

import cats._
import cats.instances._

sealed trait Proof[P]
case class QED[P]() extends Proof[P]

implicit val proofFunctor: Functor[Proof] = new Functor[Proof] {
  def map[A, B](fa: Proof[A])(f: A => B): Proof[B] = QED[B]()
}

implicit val proofApplicative: Applicative[Proof] = new Applicative[Proof] {
  def ap[A, B](ff: Proof[A => B])(fa: Proof[A]): Proof[B] = QED[B]()
  def pure[A](a: A): Proof[A] = QED[A]()
}

implicit val proofMonad: Monad[Proof] = new Monad[Proof] {
  def flatMap[A, B](fa: Proof[A])(f: A => Proof[B]): Proof[B] = QED[B]()
  def pure[A](a: A): Proof[A] = QED[A]()
  def tailRecM[A, B](a: A)(f: A => Proof[Either[A, B]]): Proof[B] = QED[B]()
}

case class :::[A, P](value: A)

sealed trait TRUE
sealed trait FALSE
sealed trait &&&[P, Q]
sealed trait |||[P, Q]
sealed trait -->[P, Q]
sealed trait Not[P]
sealed trait ===[P, Q]

def axiom[P]: Proof[P] = QED[P]()

def and_intro[P, Q](p: P)(q: Q): Proof[P &&& Q] = axiom
def and_elimL[P, Q](p_and_q: P &&& Q): Proof[P] = axiom
def and_elimR[P, Q](p_and_q: P &&& Q): Proof[Q] = axiom
def or_introL[P, Q](p: P): Proof[P ||| Q] = axiom
def or_introR[P, Q](q: Q): Proof[P ||| Q] = axiom
def impl_intro[P, Q](p_proves_q: P => Proof[Q]): Proof[P --> Q] = axiom
def impl_elim[P, Q](p_implies_q: P --> Q)(p: P): Proof[Q] = axiom
def not_intro[P](p_proves_false: P => Proof[FALSE]): Proof[Not[P]] = axiom
def contradicts[P](p: P)(not_p: Not[P]): Proof[FALSE] = axiom
def absurd[P](proof_of_false: FALSE): Proof[P] = axiom
def refl[P]: Proof[P === P] = axiom

type Theorem[P, Q] = (P --> Q) --> (Not[Q] --> Not[P])

def proof1[P, Q]: Proof[Theorem[P, Q]] = {
  impl_intro { p_implies_q => 
    impl_intro { not_q =>
      not_intro { p => 
        implicitly[Monad[Proof]].flatMap(impl_elim(p_implies_q)(p)) { q =>
          contradicts(q)(not_q)
        }
      }
    }
  }
}

println(proof1) // = QED()