jcreed blog > A Postulate for Internalized Parametricity

A Postulate for Internalized Parametricity

Update! Everything Below Is Perhaps Bunk! Evan Cavallo shrewdly sniffed out the fact that the below idea runs into a gap if you try to show free theorems for any nontrivial polymorphic type where the type variable occurs negatively. Maybe it can be repaired somehow? Or quite possibly I'm stumbling down the path towards reinventing the POPL'24 paper cited below. I'm having fun either way.
I had the follow-up thought about the previous post, and though I have no particular confidence that it is consistent and/or novel, I thought I'd write it down anyways.

Suppose we postulate first of all that there is a "bridge interval" (to borrow a term of this paper, which I have not fully digested, and which may for all I know do everything I'm doing here but better) type I\I that has two known points i0,i1:Ii_0, i_1 : \I. From any type family V:ISetV : \I \to \rset we can derive a (binary, proof-relevant) relation. I'm going to use record notation and say the type of relations is Rel:={A0:Set,A1:Set,R:Set,π0:RA0,π1:RA1}\rrel := \{ A_0 : \rset, A_1 :\rset, R : \rset, \pi_0 : R \to A_0, \pi_1 : R \to A_1 \} Then we can make some definitions

A0:(V:ISet)SetA_0 : (V : \I \to \rset) \to \rsetA0 V=V i0 A_0\ V = V\ i_0
A1:(V:ISet)SetA_1 : (V : \I \to \rset) \to \rsetA1 V=V i1 A_1\ V = V\ i_1
R:(V:ISet)SetR : (V : \I \to \rset) \to \rsetR V=(i:I)V i R\ V = (i:\I)\to V\ i
π0:(V:ISet)R VA0 V\pi_0 : (V : \I \to \rset) \to R\ V \to A_0\ Vπ0 V r=r i0 \pi_0\ V\ r = r\ i_0
π1:(V:ISet)R VA1 V\pi_1 : (V : \I \to \rset) \to R\ V \to A_1\ Vπ1 V r=r i1 \pi_1\ V\ r = r\ i_1

And bundle all this up as

mkr:(ISet)Relmkr : (\I \to \rset) \to \rrel
mkr V={ mkr\ V = \{
A0=A0 V, A1=A1 V,R=R V,π0=π0 V, π1=π1 V\qquad A_0 = A_0\ V,\ A_1 = A_1\ V,R = R\ V, \pi_0 = \pi_0\ V,\ \pi_1 = \pi_1\ V
}\}
The set A0A_0 is the fiber over i0i_0, the set A1A_1 is the fiber over i1i_1, and the RR consists of the global elements of the indexed set VV. Each global element can be instantiated to give an element of A0A_0 or A1A_1, so we really do have a span across A0,A1A_0, A_1.

The Postulate

Now consider what happens if we postulate that
mkrmkr is an equivalence
That is, mkrmkr has some inverse mkr1:RelISetmkr^{-1} : \rrel \to \I \to \rset and so every relation arises as the mkrmkr of some ISet\I \to \rset.

Preserving Relations

Next we we want to observe that whenever we have V,W:ISetV, W : \I \to \rset, every map of the form h:(i:I)V iW i h : (i:\I) \to V\ i \to W\ i induces a relation-preserving map. Namely, the map λm.λi.h i (m i):((i:I)V I)((i:I)W I)\lambda m.\lambda i. h\ i\ (m\ i) : ((i:\I)\to V\ I) \to ((i:\I)\to W\ I) goes by definition also R VR WR\ V \to R\ W, and can be seen to commute with the maps h i0:V i0W i0=A0 VA0 Wh\ i_0 : V\ i_0 \to W\ i_0 = A_0\ V \to A_0\ W h i1:V i1W i1=A1 VA1 Wh\ i_1 : V\ i_1 \to W\ i_1 = A_1\ V \to A_1\ W In other words, we have a commutative diagram
or equivalently by definition,

Parametricity

Suppose we'd like to show the canonical example free theorem that j:(A:Set)AAj : (A : \rset) \to A \to A must be the identity function. We can do this by showing that jj appropriately commutes with any function f:ABf : A \to B, i.e. by showing (f:AB)fj A=j Bf(*)(f : A \to B) \to f \o j\ A = j\ B \o f \tag{*} because if that were true, then for any a:Aa : A we could set ff to K aK\ a, the constantly-aa function AAA \to A, and find that (a:A)Kaj A=j AK a(a : A) \to K a \o j\ A = j\ A \o K\ a and therefore (a:A)a=j A a(a : A) \to a = j\ A\ a so jj would be the identity function.

Now to show (*), define ρ:Rel\rho : \rrel to be the underyling relation of the function ff, i.e. ρ={A0=A, A1=B, R=(a:A)(b:B)×f ab,\rho = \{ A_0 = A,\ A_1 = B,\ R = (a : A) (b : B) \x f\ a \equiv b, π0a,b,q=a, π1a,b,q=b}\pi_0\langle a, b, q \rangle = a,\ \pi_1\langle a,b,q\rangle = b \} What happens when we apply jj to the type mkr1 ρ imkr^{-1}\ \rho \ i for various i:Ii:\I? We obtain h=λi.j (mkr1 ρ i):(i:I)mkr1 ρ imkr1 ρ i h = \lambda i . j\ (mkr^{-1}\ \rho \ i) : (i:\I) \to mkr^{-1}\ \rho \ i \to mkr^{-1}\ \rho \ i This is an example of an hh from the previous section about preserving relations! So we obtain a commutative diagram, where the top and bottom horizontal maps are h i0h\ i_0 and h i1h\ i_1. But in particular our h i0h\ i_0 is equal to j (mkr1 ρ i0)=j (A0 (mkr1 ρ)) j\ (mkr^{-1}\ \rho \ i_0) = j\ (A_0\ (mkr^{-1}\ \rho)) =j ((mkr(mkr1 ρ)).A0)= j\ ((mkr (mkr^{-1}\ \rho)).A_0) =j (ρ.A0)= j\ (\rho.A_0) =j A= j\ A and likewise h i1=j Bh\ i_1 = j\ B So what we have is a commutative diagram

which can be massaged into
as required.