<div dir="ltr"><div>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.<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">data Vec (A : Set) : ..(_ : Nat) → Set where<br> [] : Vec A 0<br> _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)<br></blockquote><div><br></div><div>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 <a href="https://github.com/agda/agda/issues/1602">https://github.com/agda/agda/issues/1602</a>. If people are interested, we could make it more liberal under --experimental-irrelevance, though I'd really rather have a clear semantics first.<br><br></div><div>Jesper<br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Oct 9, 2015 at 1:37 AM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Thu, Oct 8, 2015 at 4:53 AM, Andrea Vezzosi <<a href="mailto:sanzhiyan@gmail.com">sanzhiyan@gmail.com</a>> wrote:<br>
> If you use the model from this paper and interpret Set as the universe<br>
> of discrete reflexive graphs, then you also know that it sends the<br>
> equality relation to the equality relation. There you can get<br>
> naturality results for functors over that universe.<br>
><br>
> <a href="http://bentnib.org/dtt-parametricity.html" rel="noreferrer" target="_blank">http://bentnib.org/dtt-parametricity.html</a><br>
<br>
</span>I'll have to read this in more depth. On skimming, I'm not sure if the<br>
stuff they work through in the paper supports the same example. It has<br>
one universe for instance, so things like:<br>
<br>
F : Set -> Set1<br>
F _ = Set<br>
<br>
aren't clearly well-defined. I don't think Martin-löf type theory even<br>
lets you construct a family `x:U ⊢ F(x) type` such that `F(x) = U` for<br>
all `x` without a universe that contains `U`.<br>
<span class=""><br>
> I would say that phi and functions Nat -> Nat -> Nat are actually<br>
> parametric, but while we could argue that functions Nat -> Nat -> Nat<br>
> are also natural since Nat is the discrete category, we don't get the<br>
> same for phi.<br>
<br>
</span>I suppose it depends on what you think "parametric" means, which is<br>
something I might vary on depending on my mood.<br>
<br>
I think I recall reading (although I have no references, so I might be<br>
completely wrong) that "parametric polymorphism" was coined by<br>
Streicher, referring to the intuition that even though types were<br>
written as arguments to polymorphic functions (in some presentations,<br>
at least), they didn't affect the computational result of them. I<br>
guess that eventually relational parametricity was formulated to make<br>
the intuition precise. And for something like System F, it matches.<br>
<br>
Then relational parametricity can be extended to dependent types so<br>
that all types have an associated true theorem about them, but the<br>
theorem doesn't match the original intuition about what "parametric"<br>
meant (if that was in fact the original intuition), because things<br>
_aren't_ parametric in that sense. But systems for formalizing<br>
computational irrelevance are extending the original sense to new<br>
areas (and presumably the true theorems about those types would look<br>
more like the ones in System F).<br>
<br>
So when I said that functions with type `Nat -> Nat -> Nat` aren't<br>
required to be parametric, it was in that sense. Functions with type<br>
`Set -> Set -> Set` are a bit harder to call, because you can't do<br>
something like case analysis on Sets (modulo certain data types). So<br>
they have a greater degree of uniformity, in that they must<br>
essentially be witnessed by a pure lambda term. One might also say<br>
that ordinary inductive data types (and not GADTs, i.e. inductive<br>
families with large indices) are "parametric" in their Set arguments,<br>
because the type family is defined uniformly for every choice of type<br>
parameter. But they are still not exactly parametric in the way that<br>
polymorphic functions in System F are parametric in their type<br>
arguments.<br>
<span class=""><br>
> The irrelevance modality seems appropriate here because naturality is<br>
> the same as constancy, but it might be too strong in general. It does<br>
> seem like we need a modality though.<br>
<br>
</span>It's definitely too strong in general. You can see this in GHC if you<br>
try to translate category theory that isn't based on sets with<br>
structure. For instance, we might try to define products by saying<br>
they are limits of diagrams drawn by the discrete category 2. So<br>
something like:<br>
<br>
type family ProdDiagram x y (b :: 'Bool) :: *<br>
type instance ProdDiagram x y 'False = x<br>
type instance ProdDiagram x y 'True = y<br>
<br>
newtype Prod x y = Prod (forall (b :: 'Bool). ProdDiagram x y b)<br>
<br>
However, this doesn't work, because `forall` ensures computational<br>
irrelevance of the quantified variables, even for things with data<br>
kinds. So things of type `forall b. ProdDiagram x y b` are uniform<br>
definitions that could be instantiated to get something of type `x` or<br>
of type `y`. In practice I think this means `undefined` is your only<br>
real option, even for x = y (because for an abstract b, GHC won't know<br>
that `ProdDiagram x x b` reduces to `x` regardless of choice of `b`).<br>
<br>
I think it works out all right for *-like categories, because being<br>
required to commute across arbitrary functions between types is very<br>
similar to not being able to depend on which type you're used with.<br>
But for things like discrete categories it's not right at all.<br>
<span class=""><br>
> By the way, you can actually have dependent irrelevant quantification now.<br>
<br>
</span>Are you sure? At first when I tried and it didn't work, I thought<br>
maybe my copy of Agda was old, but now I've refreshed to the latest<br>
development version, and it still doesn't seem to work, even with<br>
--experimental-irrelevance. I've also asked around and been told that<br>
it isn't actually implemented. Perhaps it's only implemented for some<br>
special cases (I think I did see that it will work for Level<br>
arguments).<br>
<br>
For this example it doesn't actually matter, because `F` can be given<br>
type `.Set -> Set1`. But that's not true less trivial examples, of<br>
course.<br>
<span class="HOEnZb"><font color="#888888"><br>
-- Dan<br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>