GeneralizedParametricityForHol

Below we try to interpret Andrei's generalized parametricity tracking
for HOL as an algorithmic rule system, realizing the choice of
predicators and K with (structured) labels. Not tried in silicon yet,
but it looks quite similiar to isotrans.

The K and the predicator of Andrei's judgement are now hidden behind
the label and are semantically lost, because there seems no
easy way to get that. Also we are focussed on the moding that we need
for a transfer functionality.

The basic judgement

l: t to t' by R := R t t'

can be read as

t goes to t' by R, with the label l driving the rule choice

where l,t are inputs and t', R are outputs.
We use this to derive

Fpred vec{P_m} t t'

for a concrete choice (driven by the label)
of vec{P_m} out of the K in (t, t') ::_F K.

To realize the transfer of types we need a judgement to
construct relators R away from types

l: tau to tau' via R := true

(l, tau are inputs, tau', R are outputs)
This seems to correspond to mapper composition.

---

We also have a set-lifted version of this to accumulate derivation
results for the varying elements of K:

l: t to t' by RR := (ALL R:RR. R t t')

It is not clear wether doing all computations for a given input term,
predicator and all elements of K is really necessary or if we are
always just interested in one computation for a given element of K.
Isotrans experience suggests the latter.

And we need the usual function-lifting thing

R #> R' := (% f, f'. ALL x, x'. R x x' --> R' (f x) (f' x'))

(called Funpred R R' in Andreis' writeup).

---

So let's have the rules that are generic in the label:

l : t1 to t2 by R1 #> R2 ; l : t2 to t2' by R1
==> l : (t1 t2) to (t1' t2') by R2

l: tau to tau' via R ; (!! x, x'. l : x to x' by R ==> l : (t x) to (t' x') by R')
==> l : (% x::tau. t x) to (% x'::tau'. t' x') by R #> R'

l : t to t' by R
==> l : t to t' by {R}

l : t to t' by {}

l1 : t to t' by RR1 ; l2 : t to t' by RR2
==> (l1 Un l2) : t to t' by (RR1 Un RR2)

l : tau1 to tau1' via R1 ; l : tau2 to tau2' via R2
==> l : (tau1 => tau2) to (tau1' => tau2') via R1 #> R2

A (1,1)-mapper F (regarding F as a type context) corresponds to the rule
(inverse l) : tau1 to tau1' via R1 ; l : tau2 to tau2' via R2
==> l : ((tau1, tau2) F) to ((tau1', tau2') F) via FPred R1 R2

Note that the union on labels is just a syntactic marker
interpreted by the rule above, so we can set (l1 Un l2) := l1
or something equally boring.

We could also have label-changing rules for the judgement l: t to t' by R,
which was interesting in isotrans to realize ad-hoc choices such as
permutation of products and combination of isomorphisms.
Having a rule like

l : t to t' by RR ; R : RR
==> l : t to t' by R

would kill the syntax-directed nature of the rule system
and seems unnecessary anyway, since if we always know
which relators we are interested in, we can just state
the rules with corresponding premises and specialized labels.

---

So if you have vec{P_m} from K in the definition of generalized parametricity in mind with

P_m :: (vec{beta} G_m, vec{beta'} G'_m) pred

the interpretation of this is a set of rules

P_m_choice : (vec{beta} G_m) to (vec{beta'} G'_m) via P_m.

with fresh labels P_m_choice to selectively activate them if P_m is present in K.
Note that we cannot just use the P_m as labels, because they have different types
in general.

If K is {vec{P_1,m}, ..., vec{P_k,m}} we thus introduce rules
labelled by P_i,j_choice and use the label

Un i:{1,..,k} Un j:{1,..,m} P_i,j_choice

to drive the cumulative computation.

Rules for fully-parametric polymorphic constants c :: vec{alpha_m} F,
i.e with (c, c) :: UNIV, look like this:

vec{ l: alpha_m to alpha'_m via P_m }
==> l: (c :: vec{alpha_m} F) to (c :: vec{alpha'_m} F) by Fpred vec{P_m}

Because of K=UNIV we use a label variable in the rule.

---

An insight about K:
K says what the relation structures on terms of "basic types"
are like, with the functor F saying what is regarded as basic
at the moment. In this interpretation this relation structure
on terms of "basic types" will be realized with rules acting
on just these types. We tag these rules with labels, to
allow for the different choices of vec{P_m} in K.

An insight about the predicators F:
they explain how the type structure is decomposed and how to construct
relator structure from more basic relators.
They are implicitly present in the rules for judgment
l: t to t' by R here, in the form of their relator construction function
Fpred applied to the relators for subterms, giving R.
Which F is to be applied at any given moment?
We infer this from the input terms, also based on the label.

---

How do we ensure that the rules for a label agree with each other?
This is an intensional invariant which can be proven by induction
on derivations ... but how to get this algorithmically?
We soft-type the judgements and check that the rules obey this
soft-typing.
As a basic invariant we want to ensure that R in l: (t::tau) to (t'::tau') by R
is the result of l: tau to tau' via R.

A more precise invariant we can state a softtype is:
given iso: (t::tau) to (t'::tau') by R,
we have that R is a bijection from tau to tau' synthesized by
some rules for bijection formation (cf. isotrans).

---

Andy is still not entirely sure how isomorphic transfer
arises as a parametricity derivation.
Do we use isotrans: t to t' by (P isoto Q via f),
with the custom relator

P isoto Q via f := (% t, t'.
t : dom P, t' : dom Q,
f is a generalized bijection between dom P and dom Q,
Q (f t) t')

????

This would lead to rules like

isotrans: tau1 to tau1' via (P isoto P' via f) ;
isotrans: tau2 to tau2' via (Q isoto Q' via g)
==> isotrans: (tau1 => tau2) to (tau1' => tau2') via ((P #> Q) isoto (P' #> Q') via (f >> g))

with f >> g := (% h. g o h o f^-1).

But do we have that

(P #> Q) isoto (P' #> Q') via (f >> g) = (P isoto P' via f) #> (Q isoto Q' via g)

? Looks pretty good.

Note that dom (P #> Q) = {f | f is P/Q-invariant}

---

simple set-based generalized parametricity

To transfer away from different subsets of a single pseudo-universe
we have to base this tool on sets instead of HOL types.

We only have to consider "simple sets", i.e. no dependent products
and only schematic set variables. (think: we move to the
set-theoretic image of HOL types, using (Union 'a : TyUniv. 'a set)
instead of TyUniv)

Probably we can just get away with reading taus as sets instead
of types and Fs as adapted set constructors instead of functors
in the category of HOL types.