Skip to content

Instantly share code, notes, and snippets.

@gvolpe

gvolpe/Leibniz-theory.md

Forked from hobwekiva/Leibniz-theory.md
Created December 29, 2018 01:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gvolpe/4740c3cefdd28e6958a10bc1d971f3f4 to your computer and use it in GitHub Desktop.
Save gvolpe/4740c3cefdd28e6958a10bc1d971f3f4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Leibniz-theory.md

Preliminaries

type Void <: Nothing
type ¬[-A] = A => Void
type ¬¬[+A] = ¬[¬[A]]
type ⋁[+A, +B] = Either[A, B]
type ⋀[+A, +B] = Tuple2[A, B]

Inhabitance

¬¬a forms a monad.

Type Poset

Types in a language with subtyping form a partially ordered set.

Let's define:

  • a ~ b - type equality
  • a ≤ b - subtyping relation

We can declare them in Scala as follows:

trait ~[ A,  B] { def subst[F[_]] (fa: F[A]): F[B] }
trait ≤[-A, +B] { def subst[F[+_]](fa: F[A]): F[B] }

Since they are inhabited by at most a single value, they are mere propositions and we can assert:

def provedIs[A, B](f: ¬¬[A === B]): A === B = ...
def provedAs[A, B](f: ¬¬[A <~< B]): A <~< B = ...

Axioms for posets:

  • a ≤ a (reflexivity: every element is related to itself).
  • if a ≤ b and b ≤ a, then a ~ b (antisymmetry: two distinct elements cannot be related in both directions).
  • if a ≤ b and b ≤ c, then a ≤ c (transitivity: if a first element is related to a second element, and, in turn, that element is related to a third element, then the first element is related to the third element).

We hit our first stumbling block, anti-symmetry is not provable (at least in Scala2)! We will have to assert it:

def bracket[A, B](below: A <~< B, above: B <~< A): A === B = ...

Later on we will need:

  • a ≸ b - incomparable types
  • a < b - strict subtyping relation
type <[ A,  B] = (¬[A ~ B], A ≤ B)
type ≸[ A,  B] = (¬[A ≤ B], ¬[B ≤ A])

They satisfy a number of poset axioms & consequences of those axioms:

  • a < b ⟺ a ≤ b ⋀ ¬(a ~ b) (by definition in Scala).

  • a ≸ b ⟺ ¬(a ≤ b) ⋀ ¬(b ≤ a) (by definition in Scala).

  • a ≤ b ⟺ a < b ⋁ a ~ b

  • ¬(a ≤ b) ⟺ a ≸ b ⋁ b < a

  • ¬(a ~ b) ⟺ a ≸ b ⋁ b < a ⋁ a < b

  • ...

Only one of a ~ b, a < b, a > b, a ≸ b can be true for any given a and b.

Incomparability witnesses

a ≸ b
⟺ ¬(a ~ b) ⋀ ¬(a < b) ⋀ ¬(b < a)
⟺ ¬(a ~ b ⋁ a < b ⋁ b < a)
⟺ ¬(a ≤ b ⋁ b ≤ a)
⟺ ¬(a ≤ b) ⋀ ¬(b ≤ a)

¬(a ≸ b)
⟺ ¬(¬(a ~ b) ⋀ ¬(a < b) ⋀ ¬(b < a))
⟺ a ~ b ⋁ a < b ⋁ b < a
⟺ a ≤ b ⋁ b ≤ b

Strict Subtyping witnesses

a < b
⟺ ¬(a ~ b) ⋀ a ≤ b

¬(a < b)
⟺ ¬(¬(a ~ b) ⋀ a ≤ b)
⟺ a ~ b ⋁ ¬(a ≤ b)

Type functions

Define "type functions" as type constructors and type lambdas and write f a to mean type function f applied to type a.

Define:

  • constant f to mean ∀ a b. f a ~ f b (constant function).
  • injective f to mean ∀ a b. f a ~ f b ⟶ a ~ b (injective function).
  • covariant f to mean ∀ a b. a ≤ b ⟶ f a ≤ f b (monotonically increasing function).
  • contravariant f to mean ∀ a b. a ≤ b ⟶ f b ≤ f a (monotonically decreasing function).
  • strictly-covariant f to mean ∀ a b. a < b ⟶ f a < f b (strictly increasing function).
  • strictly-contravariant f to mean ∀ a b. a < b ⟶ f b < f a (strictly decreasing function).
  • invariant f to mean ∀ a b. ¬(a ~ b) ⟶ f b ≸ f a.

It is obvious that constant f ⟹ covariant f and strictly-covariant f ⟹ covariant f (analogously for contravariance). It is not obvious at all whether strictly-covariant f ⟹ covariant f ⋀ ¬(constant f).

Lemma 1 (L1)

At most one of strictly-covariant f, strictly-contravariant f, constant f, invariant f can be true simultaneously.

Lemma 2 (L2)

strictly-covariant f ⟹ ¬(contravariant f) and strictly-contravariant f ⟹ ¬(covariant f)

Proof: WLOG we will only prove the first part. Suppose f is both strictly covariant and contravariant. Then for any a and b such that a < b, f a < f b and f b ≤ f a ⟺ f b < f a ⋁ f b ~ f a. Contradiction.

Parametricity Axioms

First parametricity axiom (P1)

All type functions in Scala are either constant or injective.

Second parametricity axiom (P2)

All injective type functions are either strictly covariant, strictly contravariant, or invariant.

Consequences of Parametricity

Injectivity & Constantness witnesses

injective f ⟺ ¬(constant f)
⟺ ¬(∀ a b. f a ~ f b)
⟺ ∃ a b. ¬(f a ~ f b)

¬(injective f) ⟺ constant f
⟺ ¬(∀ a b. f a ~ f b ⟶ a ~ b)
⟺ ¬(∀ a b. ¬(f a ~ f b) ⋁ a ~ b)
⟺ ∃ a b. f a ~ f b ⋀ ¬(a ~ b)
⟺ ∃ a b. ¬(a ~ b) ⋀ f a ~ f b

Variance bracket theorems

covariant f ⋀ contravariant f 
⟺ (∀ a b. a ≤ b ⟶ f a ≤ f b) ⋀ (∀ a b. a ≤ b ⟶ f b ≤ f a)
⟺ ¬(0 ~ 1) ⋀ (f 0 ≤ f 1) ⋀ (f 1 ≤ f 0)
⟺ ¬(0 ~ 1) ⋀ (f 0 ~ f 1)
⟺ constant f

covariant f ⋁ contravariant f
⟺ ¬(¬(covariant f) ⋀ ¬(contravariant f))
⟺ ¬(invariant f)

Invariance witness

invariant f
⟺ ¬(constant f) ⋀ ¬(strictly-covariant f) ⋀ ¬(strictly-contravariant f)
⟺ ¬(covariant f) ⋀ ¬(contravariant f)
⟺ ¬(∀ a b. a ≤ b ⟶ f a ≤ f b) ⋀ ¬(∀ a b. a ≤ b ⟶ f b ≤ f a)
⟺ ¬(∀ a b. ¬(a ≤ b) ⋁ f a ≤ f b) ⋀ ¬(∀ a b. ¬(a ≤ b) ⋁ f b ≤ f a)
⟺ (∃ a b. a ≤ b ⋀ ¬(f a ≤ f b)) ⋀ (∃ a b. a ≤ b ⋀ ¬(f b ≤ f a))
⟺ ∃ a b x y. a ≤ b ⋀ ¬(f a ≤ f b) ⋀ x ≤ y ⋀ ¬(f b ≤ f a)

¬(invariant f)
⟺ ¬(∀ a b. ¬(a ~ b) ⟶ f b ≸ f a)
⟺ ¬(∀ a b. a ~ b ⋁ f b ≸ f a)
⟺ ∃ a b. a ~ b ⋀ ¬(f b ≸ f a)

Covariance & Contravariance witnesses

covariant f
⟺ ¬(strictly-contravariant f) ⋀ ¬(invariant f)
⟺ ¬(∀ a b. a < b ⟶ f b < f a) ⋀ ¬(∀ a b. ¬(a ~ b) ⟶ f a ≸ f b)
⟺ ¬(∀ a b. ¬(a < b) ⋁ f b < f a) ⋀ ¬(∀ a b. a ~ b ⋁ f a ≸ f b)
⟺ (∃ a b. a < b ⋀ ¬(f b < f a)) ⋀ (∃ a b. ¬(a ~ b) ⋀ ¬(f a ≸ f b))
⟸ ∃ a b. a < b ⋀ ¬(f b < f a) ⋀ ¬(a ~ b) ⋀ ¬(f a ≸ f b)
⟺ ∃ a b. a < b ⋀ ¬(f b < f a) ⋀ ¬(f a ≸ f b)
⟺ ∃ a b. a < b ⋀ (f a ≤ f b ⋁ f a ≸ f b) ⋀ ¬(f a ≸ f b)
⟺ ∃ a b. a < b ⋀ f a ≤ f b

W.L.O.G.

contravariant f
⟺ ∃ a b. a < b ⋀ f b ≤ f a

Strict Covariance & Contravariance witnesses

¬(strictly-covariant f)
⟺ ¬(∀ a b. a < b ⟶ f a < f b)
⟺ ¬(∀ a b. ¬(a < b) ⋁ f a < f b)
⟺ ∃ a b. a < b ⋀ ¬(f a < f b)

Putting it all together

trait Constant[F[_]] { 
	def apply[A, B]: F[A] ~ F[B]
}
trait Injective[F[_]] { 
	def apply[A, B](ev: F[A] ~ F[B]): A ~ B
}
trait Invariant[F[_]] {
	def apply[A, B]: F[A] ≸ F[B]
}
trait Covariant[F[_]] { 
	def apply[A, B](ev: A ≤ B): F[A] ≤ F[B]
}
trait Contravariant[F[_]] {
	def apply[A, B](ev: A ≤ B): F[B] ≤ F[A]
}
trait StrictlyCovariant[F[_]] { 
	def apply[A, B](ev: A < B): F[A] < F[B]
}
trait StrictlyContravariant[F[_]] {
	def apply[A, B](ev: A < B): F[B] < F[A]
}

object Axioms {
  /**
    * Subtyping is antisymmetric.
    *
    * a ~ b ⟷ a ≤ b ⋀ b ≤ a
    */
  def bracket[A, B](below: A <~< B, above: B <~< A): A === B =
    Inhabited.unsafeForce[A === B].proved

  def subtyping[A, B](ev: A =!= B): ¬¬[(B </< A) \/ (A </< B) \/ (A >!< B)] =
    Inhabited.unsafeForce

  def parametricity[F[_]]: ¬¬[IsConstant[F] \/ IsInjective[F]] =
    Inhabited.unsafeForce

  def subtypeParametricity[F[_]](ev: IsInjective[F]): ¬¬[IsStrictlyContravariant[F] \/ IsStrictlyCovariant[F] \/ IsInvariant[F]] = {
    val _ = ev
    Inhabited.unsafeForce
  }
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment