<div dir="ltr"><div>Run-time irrelevance is a relatively new feature, which is only officially supported in the upcoming 2.6.1 release. It hasn't been properly documented yet. See <a href="https://github.com/agda/agda/issues/3855">https://github.com/agda/agda/issues/3855</a></div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jan 22, 2020 at 4:34 PM Mathijs Kwik <<a href="mailto:mathijs@bluescreen303.nl">mathijs@bluescreen303.nl</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Interesting.</div><div><br></div><div>The @0 annotation works fine, thanks. Only thing I'm wondering is how I could have found this myself. Neither the manual nor the release notes make note of this facility. Grepping the sources, I found there are other annotations, such as @erased, which makes me wonder what other nice gems I'm missing out on :)</div><div><br></div><div>Your second suggestion seems to works fine! I'm wondering though why Data.Empty.Irrelevant exists at all. Why not just make the default version in Data.Empty use irrelevance? Or even: shouldn't all \bot occurrences be treated as irrelevant automatically?</div><div><br></div><div>Thanks,<br></div><div>Mathijs<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jan 22, 2020 at 9:52 AM Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi Mathijs,</div><div><br></div><div>I the first example you can use run-time irrelevance (written `@0` or `@erased`):</div><div><br></div><div>```</div><div>data Any {ℓ₁ ℓ₂ : Level} {k : Set ℓ₁} (f : k → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where<br>  any : {@0 t : k} → f t → Any f</div><div>```</div><div>This gets compiled to</div><div>```</div><div>name10 = "Any"<br>d10 a0 a1 a2 a3 = ()<br>newtype T10 = C22 AgdaAny</div><div>```</div><div><br></div><div>In the second case you need to take care to only pattern match on the proof in irrelevant contexts. To rule out the impossible cases you can use `Data.Empty.Irrelevant.⊥-elim`. For instance,<br></div><div>```</div><div>t5b (sucList (zero ∷ xs) (zero ∷ ys) {p}) = ⊥-elim (case p of λ { (() ∷ _) })</div><div>```</div><div><br></div><div>Similarly, when you need to deconstruct the proof for the recursive cases, the pattern matching must happen inside the irrelevant argument:</div><div>```</div><div>t5b (sucList (zero ∷ xs) (suc y ∷ ys) {p}) = t5b (sucList xs ys {case p of λ { (_ ∷ p) → p }})<br>```</div><div><br></div><div>Hope this helps with your struggles.<br></div><div><br></div><div>/ Ulf<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Jan 21, 2020 at 11:41 PM Mathijs Kwik <<a href="mailto:mathijs@bluescreen303.nl" target="_blank">mathijs@bluescreen303.nl</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi all,</div><div><br></div><div>I recently played around a bit with irrelevance annotations and with compile time vs runtime presence of certain elements by looking at the generated Haskell code via MAlonzo.</div><div><br></div><div>I observed that while in haskell it's quite easy to purposefully lose reference to a type variable through this construct:</div><div><br></div><div>```</div><div>data Any (f : k -> Type) where</div><div>  Any :: f t -> Any f</div><div>```</div><div><br></div><div>The agda equivalent</div><div><br></div><div>```</div><div>  data Any {ℓ₁ ℓ₂ : Level} {k : Set ℓ₁} (f : k → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where<br>    any : {t : k} → f t → Any f</div><div>```</div><div><br></div><div>leads to this runtime representation:</div><div><br></div><div>```</div><div>name42 = "Any"<br>d42 a0 a1 a2 a3 = ()<br>data T42 = C48 AgdaAny AgdaAny</div><div>```</div><div><br></div><div>so the {t : k} actually sticks around at runtime. Of course by instantiating `f` to `id` k turns into Set, erasing t at runtime (but still wasting a "space" in the constructor), but for other `f` choices (like `Vec String`) t becomes a natural number and is passed around at runtime constantly and I can even match on it to regain knowledge about the full type of `f t`.<br></div><div><br></div><div>This effectively turns the `Any` construct into a sigma / dependent product, albeit one that doesn't advertise the type that completes the incomplete `f` in its type (but in many cases, this can be known because of `f` anyway).</div><div><br></div><div>I tried adding an irrelevance annotation: .{t :k} -> f t -> Any f</div><div>But this is rejected because `t` gets used in `f t`.</div><div><br></div><div>I would expect "some vector with unknown length" to be something we would want to be able to express. And to regain knowledge of its length, we would have to traverse the entire spine (as with lists). So is there no way to get the haskell-like behaviour where we actually lose that piece of type information and can no longer depend/match on it? And most importantly: not move around the information at runtime.</div><div><br></div><div><br></div><div>---</div><div><br></div><div>My other case where irrelevance doesn't really help me the way I expect it would:</div><div><br></div><div>```</div><div>data OneMore : Rel ℕ 0ℓ where<br>  onemore : {n : ℕ} → OneMore n (suc n) <br><br>data SucList : Set where<br>  sucList : (xs : List ℕ) (ys : List ℕ) .{p : Pointwise OneMore xs ys} → SucList<br><br>t5a : SucList<br>t5a = sucList (42 ∷ 43 ∷ []) (43 ∷ 44 ∷ []) {onemore ∷ (onemore ∷ [])}<br><br>t5b : SucList → Bool<br>t5b (sucList [] []) = true<br>t5b (sucList (zero ∷ xs) (zero ∷ ys) {p}) = {!!}<br>t5b (sucList (zero ∷ xs) (suc y ∷ ys) {p}) = {!!}<br>t5b (sucList (suc x ∷ xs) (zero ∷ ys) {p}) = {!!}<br>t5b (sucList (suc x ∷ xs) (suc y ∷ ys) {p}) = {!!}<br></div><div>```</div><div><br></div><div>Here, I want to mandate that a SucList contains 2 lists of the same length, where members of the second list are always the member of the first list plus one (yes, a bit contrived). Of course I don't want any of that to exist at run time, so I mark the proof irrelevant, but the typechecker still enforces the invariant everywhere I want to create or modify a SucList. I also managed to turn this into instance arguments by creating an instance-arguments-and-implicits-only version of Pointwise, so generating the proof by hand is no longer needed, but left that out of this example.</div><div><br></div><div>But now, I run into problems then I want to match a SucList. Agda thinks all these cases at t5b are fine, which of course shouldn't be the case. Luckily, it does pick up on the fact that both lists need to be equal length, but the "one more" invariant seems unknown. Of course I can mark the proof relevant again and start matching on that, to have the type checker see which cases are impossible, but I'd rather not do that, as these Pointwise proof chains then end up being passed around at run time. <br></div><div><br></div><div>I was hoping that these irrelevant arguments (like this proof type) would still be useable by the type checker to rule out faulty cases and see shapes or other arguments. Otherwise, there really isn't much use for irrelevance for me.</div><div><br></div><div>Or did I misunderstand these concepts and opt for other means to get things erased at run time?<br></div><div>Or are there workarounds or additional things to learn/add to make these cases work the way I would like them to work?</div><div><br></div><div><br></div><div>Kind regards,</div><div>Mathijs</div><div><br></div><div>PS: I couldn't resist the subject-line although this might get advertisers to label me as entering an early midlife crisis :)<br></div><div><br></div><div><br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
</blockquote></div>
</blockquote></div>
</blockquote></div>