type Void <: Nothing
type ¬[-A] = A => Void
type ¬¬[+A] = ¬[¬[A]]
type ⋁[+A, +B] = Either[A, B]
type ⋀[+A, +B] = Tuple2[A, B]
¬¬a
forms a monad.
Types in a language with subtyping form a partially ordered set.
Let's define:
a ~ b
- type equalitya ≤ 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
andb ≤ a
, thena ~ b
(antisymmetry: two distinct elements cannot be related in both directions). - if
a ≤ b
andb ≤ c
, thena ≤ 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 typesa < 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
.
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
a < b
⟺ ¬(a ~ b) ⋀ a ≤ b
¬(a < b)
⟺ ¬(¬(a ~ b) ⋀ a ≤ b)
⟺ a ~ b ⋁ ¬(a ≤ b)
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)
.
At most one of strictly-covariant f
, strictly-contravariant f
, constant f
, invariant f
can be true simultaneously.
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.
All type functions in Scala are either constant or injective.
All injective type functions are either strictly covariant, strictly contravariant, or invariant.
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
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)
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)
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
¬(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)
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
}
}