Skip to content

Home

Jump to bottom
Alexander Konovalov edited this page Nov 24, 2017 · 5 revisions

Type Poset

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

Let's define:

  • a ~ b - type equality
  • a < b - strict subtyping relation
  • a ≤ b - subtyping relation
  • a ≸ b - incomparable types

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

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

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. 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 (A1)

All type functions in Scala are either constant or injective. We can write it out as

⊤ ⟺ parametric f
⟺ (∀ 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
Second parametricity axiom (A2)

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

Consequences of the first parametricity axiom

From the first parametricity axiom, we get:

  1. Lemma C: ∀ a b x y. f a ~ f b ⋀ ¬(a ~ b) ⟶ f x ~ f y.
  2. Lemma I1: ∀ a b x y. ¬(f x ~ f y) ⋀ f a ~ f b ⟶ a ~ b.
  3. Lemma I2: ∀ a b x y. ¬(f x ~ f y) ⋀ ¬(a ~ b) ⟶ ¬(f a ~ f b).

They can be declared in Scala as follows:

def lemmaC[F[_], A, B, X, Y](x: F[A] === F[B], y: (A === B) => Void): F[X] === F[Y]
def lemmaI1[F[_], A, B, X, Y](x: (F[X] === F[Y]) => Void, y: F[A] === F[B]): A === B
def lemmaI2[F[_], A, B, X, Y](x: (F[X] === F[Y]) => Void, y: (A === B) => Void): (F[A] === F[B]) => Void

Close examination shows that Lemma I2 can be constructively proven from Lemma I1.

Consequences of the second parametricity axiom

We can show that covariant f ⟺ constant f ⋁ strictly-covariant f. Due to A1/A2, there are four cases to consider.

  • f is constant, both sides are true.
  • f is strictly covariant, both sides are true.
  • f is strictly contravariant, then by L2 f is not covariant, both sides are false.
  • f is invariant, both sides are false.

From the second parametricity axiom, we get:

⊤ ⟺ constant f ⋁ invariant f
   ⋁ strictly-covariant f ⋁ strictly-contravariant f
⟺ strictly-contravariant f ⋁ invariant f ⋁ (constant f ⋁ strictly-covariant f)
⟺ (∀ a b. ¬(a < b) ⋁ (f b < f a)) ⋁ (∀ a b. f a ≸ f b) ⋁ covariant f
⟹ ∀ a b. ¬(a < b) ⋁ (f b < f a) ⋁ (f c ≸ f d) ⋁ covariant f
⟺ ∀ a b. ¬(a < b) ⋁ ¬(f a ≤ f b) ⋁ covariant f
⟺ ∀ a b. ¬(a < b) ⋁ ¬(f a ≤ f b) ⋁ covariant f
⟺ ∀ a b. a < b ⋀ f a ≤ f b ⋀ covariant f
⟺ ∀ a b. a < b ⋀ f a ≤ f b ⟶ (∀ x y. x ≤ y ⟶ f x ≤ f y)

⟺ ∀ a b. ¬(a < b) ⋁ ¬(f a ≤ f b) ⋁ covariant f
⟺ ∀ a b x y. ¬(a < b) ⋁ ¬(f a ≤ f b) ⋁ ¬(x ≤ y) ⋁ f x ≤ f y
⟺ ∀ a b x y. a < b ⋀ f a ≤ f b ⋀ x ≤ y ⟶ f x ≤ f y

We will call this result Lemma S. It can be declared in Scala as:

def lemmaS[F[_], A, B, X, Y](ab: (A === B) => Void, p: A <~< B, q: F[A] <~< F[B], r: X <~< Y): F[X] <~< F[Y]

Putting it all together

trait Is[A, B] { def subst[F[_]](fa: F[A]): F[B] }
trait As[-A, +B] { def subst[F[+_]](fa: F[A]): F[B] }
type Void <: Nothing
type ¬[-A] = A => Void
type ⋁[+A, +B] = Either[A, B]

type ~[ A,  B] = Is[A, B]
type ≤[-A, +B] = As[A, B]
type <[ A,  B] = (¬[A ~ B], A ≤ B)
type ≸[ A,  B] = (¬[A ≤ B], ¬[B ≤ A])

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]
}

def axiom1[F[_]]: ¬[¬[Constant[F] ⋁ Injective[F]]]
def axiom2[F[_]]: ¬[¬[Constant[F] ⋁ Invariant[F] ⋁ StrictlyCovariant[F] ⋁ StrictlyContravariant[F]]]

def axiom3[A, B](ev: ¬[¬[A ~ B]]): A ~ B
def axiom4[A, B](ev: ¬[¬[A ≤ B]]): A ≤ B
Clone this wiki locally