[Agda] Polymorphism is not (always) naturality

[Andrea Vezzosi]

To clarify on the list:

I also would like a quantifier or modality that allows to enforce some
useful degree of uniformity, which for universes could match what the
quantifiers of System F enjoy, and as Jesper suggests maybe .. can be
that.

And as you point out with your ProdDiagram it has to somehow relate to
the structure of the type in question, like naturality depends on the
structure of the category.

And yeah, I only meant that you can use "." for a dependent function
space ".(A : Set) -> ...", but A is still irrelevant (or at least
shape-irrelevant) in ...

Cheers,
Andrea


On Fri, Oct 9, 2015 at 1:37 AM, Dan Doel <dan.doel at gmail.com> wrote:
> 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