[Agda] Polymorphism is not (always) naturality

[Jesper Cockx]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151009/ffc1d9d2/attachment.html