<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>