<div dir="ltr"><div>The correct modality for parametric things isn&#39;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&#39;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&#39;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">&lt;<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@gmail.com</a>&gt;</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 &lt;<a href="mailto:sanzhiyan@gmail.com">sanzhiyan@gmail.com</a>&gt; wrote:<br>
&gt; If you use the model from this paper and interpret Set as the universe<br>
&gt; of discrete reflexive graphs, then you also know that it sends the<br>
&gt; equality relation to the equality relation. There you can get<br>
&gt; naturality results for functors over that universe.<br>
&gt;<br>
&gt; <a href="http://bentnib.org/dtt-parametricity.html" rel="noreferrer" target="_blank">http://bentnib.org/dtt-parametricity.html</a><br>
<br>
</span>I&#39;ll have to read this in more depth. On skimming, I&#39;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 -&gt; Set1<br>
    F _ = Set<br>
<br>
aren&#39;t clearly well-defined. I don&#39;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>
&gt; I would say that phi and functions Nat -&gt; Nat -&gt; Nat are actually<br>
&gt; parametric, but while we could argue that functions Nat -&gt; Nat -&gt; Nat<br>
&gt; are also natural since Nat is the discrete category, we don&#39;t get the<br>
&gt; same for phi.<br>
<br>
</span>I suppose it depends on what you think &quot;parametric&quot; 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 &quot;parametric polymorphism&quot; 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&#39;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&#39;t match the original intuition about what &quot;parametric&quot;<br>
meant (if that was in fact the original intuition), because things<br>
_aren&#39;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 -&gt; Nat -&gt; Nat` aren&#39;t<br>
required to be parametric, it was in that sense. Functions with type<br>
`Set -&gt; Set -&gt; Set` are a bit harder to call, because you can&#39;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 &quot;parametric&quot; 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>
&gt; The irrelevance modality seems appropriate here because naturality is<br>
&gt; the same as constancy, but it might be too strong in general. It does<br>
&gt; seem like we need a modality though.<br>
<br>
</span>It&#39;s definitely too strong in general. You can see this in GHC if you<br>
try to translate category theory that isn&#39;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 :: &#39;Bool) :: *<br>
    type instance ProdDiagram x y &#39;False = x<br>
    type instance ProdDiagram x y &#39;True = y<br>
<br>
    newtype Prod x y = Prod (forall (b :: &#39;Bool). ProdDiagram x y b)<br>
<br>
However, this doesn&#39;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&#39;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&#39;re used with.<br>
But for things like discrete categories it&#39;s not right at all.<br>
<span class=""><br>
&gt; 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&#39;t work, I thought<br>
maybe my copy of Agda was old, but now I&#39;ve refreshed to the latest<br>
development version, and it still doesn&#39;t seem to work, even with<br>
--experimental-irrelevance. I&#39;ve also asked around and been told that<br>
it isn&#39;t actually implemented. Perhaps it&#39;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&#39;t actually matter, because `F` can be given<br>
type `.Set -&gt; Set1`. But that&#39;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>