Axioms.scala

/**
  * Parametric type constructors are either constant or injective.
  * Constant type constructors satisfy `∀ a b. f a = f b`.
  * Injective type constructors satisfy `∀ a b. (f a = f b) => a = b`.
  *
  * Parametricity ≡
  *   `(∀ a b. f a = f b) ∨ (∀ a b. (f a = f b) => a = b)` ≡
  *   `∀ a b x y. (f x = f y) ∨ ¬(f a = f b) ∨ (a = b)`
  *
  * Using `A ∨ B ⊢ ¬A => B`, we get:
  *   1. `∀ a b x y. ¬(f x = f y) ∧ (f a = f b) => (a = b)`
  *   2. `∀ a b x y.  (f a = f b) ∧  ¬(a = b)   => (f x = f y)`
  *   3. `∀ a b x y. ¬(f x = f y) ∧  ¬(a = b)   => ¬(f a = f b)`
  *
  * Another important axis is variance of type constructors.
  * Injective type constructors are strictly covariant,
  * strictly contravariant, or invariant. Notice that constant
  * type constructors are both covariant and contravariant, hence
  * the necessity of explicitly saying "strictly" above.
  *
  * Covariance:     `∀ a b. a ≤ b => (f a ≤ f b)` or `∀ a b. ¬(a ≤ b) ∨ (f a ≤ f b)`
  * Contravariance: `∀ a b. a ≤ b => (f b ≤ f a)` or `∀ a b. ¬(a ≤ b) ∨ (f b ≤ f a)`
  * Strictly covariant: injective and covariant.
  * Strictly contravariant: injective and contravariant.
  * Invariant: injective but neither covariant nor contravariant.
  *
  *  (a ≤ b) <=> (a < b) ∨  (a = b)
  *  (a < b) <=> (a ≤ b) ∧ ¬(a = b)
  * ¬(a ≤ b) <=> (b < a) ∨  (a ≸ b)
  * 
  * NOT TRUE: ¬(a ≤ b) <=> b < a (!!!)
  *
  *
  * A useful statement:
  *   ∀ a b. (a < b) ∧ (f a ≤ f b) => ∀ x y. (x ≤ y) => (f x ≤ f y)
  * Let's unwrap it a bit:
  *    (a < b) ∧  (f a ≤ f b) ∧ (x ≤ y) => (f x ≤ f y)
  *   ¬(a < b) ∨ ¬(f a ≤ f b) ∨ ¬(x ≤ y) ∨ (f x ≤ f y)
  *   ¬(a ≤ b) ∨  (a = b) ∨ ¬(f a ≤ f b) ∨ ¬(x ≤ y) ∨ (f x ≤ f y)
  *    (a = b) ∨ ¬(a ≤ b) ∨ ¬(f a ≤ f b) ∨ (covariant f)
  *
  */
object Axioms {
  /**
    * ∀ a b x y. (f a = f b) ∧ ¬(a = b) => f x = f y
    */
  def tcParametricity1[F[_], A, B, X, Y](fab: F[A] === F[B], ab: (A === B) => Void): F[X] === F[Y] =
    fab.asInstanceOf[F[X] === F[Y]]

  /**
    * ∀ a b x y. (f a = f b) ∧ ¬(f x = f y) => a = b
    */
  def tcInjectivity[F[_], A, B, X, Y](fab: F[A] === F[B], fxy: (F[X] === F[Y]) => Void): A === B =
    fab.asInstanceOf[A === B]

  /**
    * (a < b) ∧ (f a <= f b) => ∀ x y. (x <= y) => (f x <= f y)
    */
  def cotcParametricity[F[_], A, B, X, Y]
  (ab: (A === B) => Void, p: A <~< B, q: F[A] <~< F[B], r: X <~< Y): F[X] <~< F[Y] =
    q.asInstanceOf[F[X] <~< F[Y]]
}