Proving boolean function properties via type-level logic in Scala

post-lattice.scala

/***         
scalaVersion := "2.12.4"
*/

import scala.language.higherKinds

/**
 * Checking boolean function properties via type-level logic in Scala
 */

/**
 * Type-level booleans
 *
 * Boolean functions are initially defined as methods of boolean objects
 * since this is the easiest way to define them in Scala.
 * Functions are extracted as BoolFun objects later.
 *
 * Only unary functions are defined at the moment.
 */
sealed trait Bool {
  type ConstTrue <: Bool
  type ConstFalse <: Bool
  type Id <: Bool
  type Not <: Bool
}

object True extends Bool {
  type ConstTrue = True.type
  type ConstFalse = False.type
  type Id = True.type
  type Not = False.type
}

object False extends Bool {
  type ConstTrue = True.type
  type ConstFalse = False.type
  type Id = False.type
  type Not = True.type
}

/**
 * This trait allows to represent boolean functions as separate objects.
 * Type-lambdas syntax is not used.
 * Thus to apply a function F to a boolean type B
 * (we work on types and, not on values) is done as F#app[B].
 */
trait BoolFun {
  type app[B <: Bool] <: Bool
}

object ConstTrueBoolFun extends BoolFun {
  type app[B <: Bool] = B#ConstTrue
}

object ConstFalseBoolFun extends BoolFun {
  type app[B <: Bool] = B#ConstFalse
}

object IdBoolFun extends BoolFun {
  type app[B <: Bool] = B#Id
}

object NotBoolFun extends BoolFun {
  type app[B <: Bool] = B#Not
}

/**
 * Type-class formalising that boolean function F preserves false
 *
 * @tparam F A function that preserves false
 */
case class PreservesFalse[F <: BoolFun](
  evidence: F#app[False.type] =:= False.type
)

object PreservesFalse {
  /**
   * The single rule for proving that F preserves false.
   *
   * @param e An evidence that F(false) = false
   * @tparam F The boolean function (corresponding type)
   * @return PreservesFalse[F] value
   */
  implicit def preserves[F <: BoolFun](implicit
    e: F#app[False.type] =:= False.type
  ): PreservesFalse[F] = PreservesFalse[F](e)
}

// test that proofs really work

implicitly[PreservesFalse[ConstFalseBoolFun.type]]
implicitly[PreservesFalse[IdBoolFun.type]]

// this should not compile
// implicitly[PreservesFalse[NotBoolFun.type]]
// implicitly[PreservesFalse[ConstTrueBoolFun.type]]

case class NotPreservesFalse[F <: BoolFun](
  evidence: F#app[False.type] =:= True.type
)

object NotPreservesFalse {
  /**
   * The single rule for proving that F preserves false.
   *
   * @param e An evidence that F(false) = false
   * @tparam F The boolean function (corresponding type)
   * @return PreservesFalse[F] value
   */
  implicit def notPreserves[F <: BoolFun](implicit
    e: F#app[False.type] =:= True.type
  ): NotPreservesFalse[F] = NotPreservesFalse[F](e)
}

// this should not compile
// implicitly[NotPreservesFalse[ConstFalseBoolFun.type]]
// implicitly[NotPreservesFalse[IdBoolFun.type]]

implicitly[NotPreservesFalse[NotBoolFun.type]]
implicitly[NotPreservesFalse[ConstTrueBoolFun.type]]

/**
 * Type-level function composition (not used yet)
 */
trait Compose[F <: BoolFun, G <: BoolFun] extends BoolFun {
  type app[B <: Bool] = F#app[G#app[B]]
}

implicitly[PreservesFalse[Compose[ConstFalseBoolFun.type, IdBoolFun.type]]]

// this should not compile
// implicitly[NotPreservesFalse[Compose[ConstFalseBoolFun.type, IdBoolFun.type]]]

trait ComposeClosed[P[_ <: BoolFun]] {
  def compose[F <: BoolFun, G <: BoolFun](implicit
    pf: P[F],
    pg: P[G]
  ): P[Compose[F, G]]
}

object PreservesFalseComposeClosed extends ComposeClosed[PreservesFalse] {
  def compose[F <: BoolFun, G <: BoolFun](implicit
    pf: PreservesFalse[F],
    pg: PreservesFalse[G]
  ): PreservesFalse[Compose[F, G]] = PreservesFalse[Compose[F, G]](
    // здесь нужно вручную построить экземпляр =:=,
    // см. http://www.scala-lang.org/api/2.12.4/scala/Predef$$$eq$colon$eq.html
    ???
  )
}

// this should not compile
object NotPreservesFalseComposeClosed /*extends ComposeClosed[NotPreservesFalse]*/ {
  def compose[F <: BoolFun, G <: BoolFun](implicit
    pf: NotPreservesFalse[F],
    pg: NotPreservesFalse[G]
  ): NotPreservesFalse[Compose[F, G]] = NotPreservesFalse[Compose[F, G]](
    // здесь нужно вручную построить экземпляр =:=,
    // см. http://www.scala-lang.org/api/2.12.4/scala/Predef$$$eq$colon$eq.html
    ???
  )
}

// def zompose[F <: BoolFun, G <: BoolFun](implicit
//     pf: PreservesFalse[F],
//     pg: PreservesFalse[G]
//   ) =
//   implicitly[PreservesFalse[Compose[F, G]]]

println("the end")