Unboxed recursive union types via the Curry Howard Correspondence

unboxed.scala

object UnionTypes {
  private type ¬[A] = A => Nothing
  private type ¬¬[A] = ¬[¬[A]]

  private type ∈[S, T <: Disjunction] = ¬¬[S] <:< ¬[T#D]
  private type ∉[S, T <: Disjunction] = ¬¬[S] <:!< ¬[T#D]

  /** `S` is `T`. */
  type Is[S, T] = ∈[S, OneOf[T]#Or[Nothing]]

  /** `S` must be in `T`. */
  type In[S, T <: Disjunction] = ∈[S, T]

  /** `S` must not be in `T`. */
  type NotIn[S, T <: Disjunction] = ∉[S, T]

  /** `T`. */
  type OneOf[T] = { type Or[S] = (Disjunction {type D = ¬[T]})#Or[S] }

  /** Defines alternative vaues for `T`. */
  trait Disjunction {
    self =>
    type D
    type Or[S] = Disjunction {
      type D = self.D with ¬[S]
    }
  }
  type TP[T] = T In OneOf[Int]#Or[Double]#Or[String] 
  def foo[T : TP](t: T) = t
  val i: Int = foo(42)
  val s: String = foo("foo")
  val d: Double = foo(42.4)
  //val err: Boolean = foo(true) // doesn't compile
}