[Agda] Polymorphism is not (always) naturality

[Dan Doel]

On Thu, Oct 8, 2015 at 4:53 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> If you use the model from this paper and interpret Set as the universe
> of discrete reflexive graphs, then you also know that it sends the
> equality relation to the equality relation. There you can get
> naturality results for functors over that universe.
>
> http://bentnib.org/dtt-parametricity.html

I'll have to read this in more depth. On skimming, I'm not sure if the
stuff they work through in the paper supports the same example. It has
one universe for instance, so things like:

    F : Set -> Set1
    F _ = Set

aren't clearly well-defined. I don't think Martin-löf type theory even
lets you construct a family `x:U ⊢ F(x) type` such that `F(x) = U` for
all `x` without a universe that contains `U`.

> I would say that phi and functions Nat -> Nat -> Nat are actually
> parametric, but while we could argue that functions Nat -> Nat -> Nat
> are also natural since Nat is the discrete category, we don't get the
> same for phi.

I suppose it depends on what you think "parametric" means, which is
something I might vary on depending on my mood.

I think I recall reading (although I have no references, so I might be
completely wrong) that "parametric polymorphism" was coined by
Streicher, referring to the intuition that even though types were
written as arguments to polymorphic functions (in some presentations,
at least), they didn't affect the computational result of them. I
guess that eventually relational parametricity was formulated to make
the intuition precise. And for something like System F, it matches.

Then relational parametricity can be extended to dependent types so
that all types have an associated true theorem about them, but the
theorem doesn't match the original intuition about what "parametric"
meant (if that was in fact the original intuition), because things
_aren't_ parametric in that sense. But systems for formalizing
computational irrelevance are extending the original sense to new
areas (and presumably the true theorems about those types would look
more like the ones in System F).

So when I said that functions with type `Nat -> Nat -> Nat` aren't
required to be parametric, it was in that sense. Functions with type
`Set -> Set -> Set` are a bit harder to call, because you can't do
something like case analysis on Sets (modulo certain data types). So
they have a greater degree of uniformity, in that they must
essentially be witnessed by a pure lambda term. One might also say
that ordinary inductive data types (and not GADTs, i.e. inductive
families with large indices) are "parametric" in their Set arguments,
because the type family is defined uniformly for every choice of type
parameter. But they are still not exactly parametric in the way that
polymorphic functions in System F are parametric in their type
arguments.

> The irrelevance modality seems appropriate here because naturality is
> the same as constancy, but it might be too strong in general. It does
> seem like we need a modality though.

It's definitely too strong in general. You can see this in GHC if you
try to translate category theory that isn't based on sets with
structure. For instance, we might try to define products by saying
they are limits of diagrams drawn by the discrete category 2. So
something like:

    type family ProdDiagram x y (b :: 'Bool) :: *
    type instance ProdDiagram x y 'False = x
    type instance ProdDiagram x y 'True = y

    newtype Prod x y = Prod (forall (b :: 'Bool). ProdDiagram x y b)

However, this doesn't work, because `forall` ensures computational
irrelevance of the quantified variables, even for things with data
kinds. So things of type `forall b. ProdDiagram x y b` are uniform
definitions that could be instantiated to get something of type `x` or
of type `y`. In practice I think this means `undefined` is your only
real option, even for x = y (because for an abstract b, GHC won't know
that `ProdDiagram x x b` reduces to `x` regardless of choice of `b`).

I think it works out all right for *-like categories, because being
required to commute across arbitrary functions between types is very
similar to not being able to depend on which type you're used with.
But for things like discrete categories it's not right at all.

> By the way, you can actually have dependent irrelevant quantification now.

Are you sure? At first when I tried and it didn't work, I thought
maybe my copy of Agda was old, but now I've refreshed to the latest
development version, and it still doesn't seem to work, even with
--experimental-irrelevance. I've also asked around and been told that
it isn't actually implemented. Perhaps it's only implemented for some
special cases (I think I did see that it will work for Level
arguments).

For this example it doesn't actually matter, because `F` can be given
type `.Set -> Set1`. But that's not true less trivial examples, of
course.

-- Dan