[Agda] Polymorphism is not (always) naturality

[Dan Doel]

I haven't been paying as much attention to Agda lately, so I'm not
really familiar with .. or what it's supposed to be (I found some
slides, is there a paper?). So pardon if I'm just too out of touch.

I'm not really sure why it's the correct modality, or why the vector
example relates to what we were talking about, though. For instance, I
never really expected that `Vec` itself would be irrelevant (in any
sense) in its natural argument, because as you say, it gives different
types for different numbers in general. Rather, I would expect a
declaration like:

    data Vec (A : Set) : Nat -> Set where
      [] : Vec A 0
      _::_ : .(n : Nat) -> A -> Vec A n -> Vec A (suc n)

codifying that Inductive Families Need Not Store Their Indices. Except
you can't write that type, without `Vec` itself being special, because
Agda doesn't have the sort of irrelevant quantification described in
Nathan Mishra-Linger's thesis [1] on the subject. It's the same rule
as you proposed in that bug report, where the variable in an
irrelevant quantifier can be used in ostensibly relevant places in the
body of the quantifier, because it is ultimately just building a type
to be ascribed to the actual computational term.

I understand why Agda (historically) doesn't allow this. It was
causing problems with eta. But I was never clear if those were
fundamental, or due to the implementation too eagerly erasing all
information marked irrelevant. I suppose that could be the point of
the new modality, to keep more information around for the purpose of
type checking, but then it seems more likely that it should have the
improved typing rules.

As it stands, while .. works for my reduced example (because even .
works), it wouldn't work for a somewhat more advanced example I passed
through on the way to it:

     F : Set -> Set1
     F A = Set × A

Naturality for a similar construction on this functor lets you prove
that all inhabited sets are equal to ⊤. But `..(A : Set) -> Set1` is
not allowed as a type for `F` (and I wasn't expecting it to be). So
Agda can't characterize the things that are actually natural for this
functor right now, as far as I know.

1: https://www.pdx.edu/sites/www.pdx.edu.computer-science/files/lingerphdthesis.pdf

On Fri, Oct 9, 2015 at 5:41 AM, Jesper Cockx <Jesper at sikanda.be> wrote:
> The correct modality for parametric things isn't irrelevance (since that
> allows too much, i.e. all irrelevant things are considered equal), but
> rather shape irrelevance / non-strict / isovariance / whatever people call
> it these days. In Agda, it is implemented as the double dot, e.g.
>
>> data Vec (A : Set) : ..(_ : Nat) → Set where
>>   [] : Vec A 0
>>   _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
>
>
> Afaict, this enforces that Vec doesn't depend computationally on its length
> without equating `Vec A m` with `Vec A n`. However, it is unclear what the
> semantics of the double dot are and what you should be allowed to do with
> it, see for example https://github.com/agda/agda/issues/1602. If people are
> interested, we could make it more liberal under --experimental-irrelevance,
> though I'd really rather have a clear semantics first.
>
> Jesper
>
> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>