proof

gistfile1.scala

object Proof {
  type Not[A] = A => Nothing

  trait All[P[_]] {
    def apply[A]: P[A]
  }

  def DN[A](p: Not[Not[A]]): A =
    p(return (_: A))

  def DeMorgan[P[_]](p: Not[P[A] forSome {type A}]): All[({type X[A]=Not[P[A]]})#X] =
    new All[({type X[A]=Not[P[A]]})#X] {
      def apply[A]: Not[P[A]] = (x: P[A]) => p(x)
    }

  def AllByExist[P[_]](p: Not[Not[P[A]] forSome {type A}]): All[P] =
    new All[P] {
      def apply[A]: P[A] =
        DN(DeMorgan[({type X[A]=Not[P[A]]})#X](p).apply[A])
    }

  def test = {
    val genericNil = AllByExist[List](_(Nil))
    val x: List[Int] = genericNil[Int]
  }
}