lambda_bool.sc

import Bool._
import Equality._

sealed trait Bool {
  type V <: Bool
  type ACT[T <: Up, F <: Up, Up]
}

trait True extends Bool {
  type V = True
  // lambda x.lambda y.x
  type ACT[T <: Up, F <: Up, Up] = T
}

trait False extends Bool {
  type V = False
  // lambda x.lambda y.y
  type ACT[T <: Up, F <: Up, Up] = F
}

case class Equality[A]() {
  def =+=(a: A)(implicit t: True): True = t
  def =+=[B](b: B)(implicit f: False): False = f
}

object Equality {
  def dummy[T] = null.asInstanceOf[T]

  implicit val t: True = null
  implicit val f: False = null

}

object Bool {
  type &&[A <: Bool, B <: Bool] = A# ACT[B, False, Bool]
  type ||[A <: Bool, B <: Bool] = A# ACT[True, B, Bool]
  type Not[A <: Bool] = A# ACT[False, True, Bool]
}



class BoolRep[B <: Bool](val value: Boolean)
implicit val falseRep: BoolRep[False] =
  new BoolRep[False](false)
implicit val trueRep: BoolRep[True] =
  new BoolRep[True](true)
def toBoolean[B <: Bool](implicit b: BoolRep[B]) = b.value

toBoolean[True && False || Not[False]]
type Num = True# ACT[Int, Double, Any]

val eq1 = Equality[List[Int]] =+= dummy[List[Double]]
val v1: eq1.V#ACT[Double, Int, Any] = 13
// val v2: eq1.V#ACT[Double, Int, Any] = 13.3