<div dir="ltr"><div>I learned a lot by playing around with the pointers you gave me. I think I hit a bug (reported <a href="https://github.com/agda/agda/issues/4398">https://github.com/agda/agda/issues/4398</a> ) which is always fun.</div><div><br></div><div>I have the feeling I still don't really grasp irrelevance itself (as opposed to runtime irrelevance). Have a look at this contrived heterogenous list alternative:</div><div><br></div><div>```</div>data Some (f : k → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where<br>  some : {@0 t : k} → f t → Some f<br><br>data HList3 (f : k → Set ℓ₂) : List k → Set (ℓ₁ ⊔ ℓ₂) where<br>  []  : HList3 f []<br>  _∷_ : (sf : Some f) → ∀ {t} {@0 ft : f t} {{p : sf ≡ some ft}} {xs} → HList3 f xs → HList3 f (t ∷ xs)<br><div><br></div><div>t3a : HList3 id (ℕ ∷ Bool ∷ [])<br>t3a = some 43 ∷ some false ∷ []<br><br>t3b : HList3 id (ℕ ∷ Bool ∷ []) → ℕ<br>t3b (_∷_ (some x) {{p = refl}} hl3) = x<br></div><div>```<br></div><div>It's clunky, but it works. Equality proofs disappear from runtime anyway (taking care or {{p}}) and @0 removes {ft} as well, leaving HList3 without any runtime overhead (apart from the "some" constructor).</div><div><br></div><div>However, I would expect to be able to mark {ft} and {{p}} as irrelevant as well (not just runtime irrelevant), but I run into 2 separate issues:</div><div>a) when marking them both irrelevant, agda complains p is using ft, which I would expect should be allowed if p itself is irrelevant as well.</div><div>b) I can no longer match p as refl, which matches the documented rules, but I don't understand it. I see why matching on irrelevant arguments kind of show they *are* relevant, but in the case of refl, it is the only valid constructor for ≡, so I'm only showing agda how I know x is the right type and not really using the proof for any type of (relevant) computation.</div><div><br></div><div>What an I missing here? <br></div><div><br></div><div>Kind regards,<br></div><div>Mathijs<br></div><div><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">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>