Semantic appeal
Consider the canonical refits we’ve seen so far, and perhaps some others. Loosely speaking, we can characterize such canonical refits
R=R(x,t) as taking the given track
t and placing
t→ and
t← in
just the right places around
x in
order to refit it, all the while doing ‘nothing too crazy’—no case analysis on
t, for instance.
I claim that each ‘placement’ of
t→:a→b or
t←:b→a falls into one of two
categories. Either we
produce a
b but need to
produce an
a (
covariance) or we are
asking for a
b but instead need to
ask for an
a (
contravariance). Let’s look at an example. Consider
χ(a)=a→N
A value
x:χ(a) is a
function accepting an
a and giving back an
N. It is
asking for an
a (and promises an
N in return). And the canonical refit for
χ looks like
Ra,b(x,t)=tb→a ; x
The value
Ra,b(x,t) is of
type b→N. Hence, we want to be
asking for a
b. But
x is
asking for an
a. So we compose with
t← to turn
asking for an
a into
asking for a
b.
Now consider
χ(a)=N→a
Here, a value
x:χ(a) is a
function accepting a
N and producing an
a. It
produces an
a (for each
n∈N). The canonical refit for
χ is
Ra,b(x,t)=x ; ta→b
Here
Ra,b(x,t) needs to have
type N→b. And it ought to be based off of
x, which produces an
a, not a
b. So we
produce an
a but want to
produce a
b. Hence we compose with
t→ to turn the
a into a
b.
Finally consider the example
χ(a)=FinSeq(a)→Maybe(a)
Now a value
x:χ(a) both
asks for and
produces an
a. To turn it into a value
Ra,b(x,t):χ(b) we must transform both an
asking for an
a and a
production of an
a, meaning we will want to use both
t← and
t→. And this is exactly what the canonical refit does:
R:(∀a,b)χ(a)×(a↔b)→χ(b)Ra,b(h,t)=FinSeq[[tb→a]] ; h ; Maybe[[ta→b]]
So very loosely speaking we’
re thinking of refits
R=Ra,b(x,t) as possibly
asking for some
b, and if so turning it into an
a via
t←, and then deferring to the given
x, which may
produce an
a, which gets turned back into a
b with
t→. To put a picture to words:
If you are happy to accept this (very soft) discussion so far, then hopefully you will also be amenable to the conclusion.
The uniformity condition asks that
Ra,b(xa,t)=xb
for
in-preserving tracks
t. Why in-preserving? Well, if we don’t require that
t is in-preserving, then it’s possible that
tb→a ; ta→b wouldn’t be the identity; ie, would
lose information. Certainly for a uniform value
x the instantiations
xa and
xb would have no ‘difference in information’. Hence, if
Ra,b(xa,t) is information-lossy over
xa then there’s no way it’s going to recover all the behaviour of
xb.
As such — the uniformity condition asks specifically for in-preserving tracks.
If you are happy to accept this (very soft) discussion so far, then hopefully you will also be amenable to the conclusion.
The uniformity condition asks that
for in-preserving tracks . Why in-preserving? Well, if we don’t require that is in-preserving, then it’s possible that wouldn’t be the identity; ie, would lose information. Certainly for a uniform value the instantiations and would have no ‘difference in information’. Hence, if is information-lossy over then there’s no way it’s going to recover all the behaviour of .
As such — the uniformity condition asks specifically for in-preserving tracks.
Here the left-hand figure illustrates the situation at the type level, and the right-hand figure at the value level. Each stands for some particular . Dashed lines are bijection inverses. The dots stand for “all the rest of the types ".
Additionally, note that
and so is witness to uniformity of .
