[Agda] Struggling with irrelevance

[Ulf Norell]

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 https://github.com/agda/agda/issues/3855

/ Ulf

On Wed, Jan 22, 2020 at 4:34 PM Mathijs Kwik <mathijs at bluescreen303.nl>
wrote:

> Interesting.
>
> 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 :)
>
> 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?
>
> Thanks,
> Mathijs
>
> On Wed, Jan 22, 2020 at 9:52 AM Ulf Norell <ulf.norell at gmail.com> wrote:
>
>> Hi Mathijs,
>>
>> I the first example you can use run-time irrelevance (written `@0` or
>> `@erased`):
>>
>> ```
>> data Any {ℓ₁ ℓ₂ : Level} {k : Set ℓ₁} (f : k → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂)
>> where
>>   any : {@0 t : k} → f t → Any f
>> ```
>> This gets compiled to
>> ```
>> name10 = "Any"
>> d10 a0 a1 a2 a3 = ()
>> newtype T10 = C22 AgdaAny
>> ```
>>
>> 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,
>> ```
>> t5b (sucList (zero ∷ xs) (zero ∷ ys) {p}) = ⊥-elim (case p of λ { (() ∷
>> _) })
>> ```
>>
>> Similarly, when you need to deconstruct the proof for the recursive
>> cases, the pattern matching must happen inside the irrelevant argument:
>> ```
>> t5b (sucList (zero ∷ xs) (suc y ∷ ys) {p}) = t5b (sucList xs ys {case p
>> of λ { (_ ∷ p) → p }})
>> ```
>>
>> Hope this helps with your struggles.
>>
>> / Ulf
>>
>>
>> On Tue, Jan 21, 2020 at 11:41 PM Mathijs Kwik <mathijs at bluescreen303.nl>
>> wrote:
>>
>>> Hi all,
>>>
>>> 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.
>>>
>>> I observed that while in haskell it's quite easy to purposefully lose
>>> reference to a type variable through this construct:
>>>
>>> ```
>>> data Any (f : k -> Type) where
>>>   Any :: f t -> Any f
>>> ```
>>>
>>> The agda equivalent
>>>
>>> ```
>>>   data Any {ℓ₁ ℓ₂ : Level} {k : Set ℓ₁} (f : k → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂)
>>> where
>>>     any : {t : k} → f t → Any f
>>> ```
>>>
>>> leads to this runtime representation:
>>>
>>> ```
>>> name42 = "Any"
>>> d42 a0 a1 a2 a3 = ()
>>> data T42 = C48 AgdaAny AgdaAny
>>> ```
>>>
>>> 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`.
>>>
>>> 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).
>>>
>>> I tried adding an irrelevance annotation: .{t :k} -> f t -> Any f
>>> But this is rejected because `t` gets used in `f t`.
>>>
>>> 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.
>>>
>>>
>>> ---
>>>
>>> My other case where irrelevance doesn't really help me the way I expect
>>> it would:
>>>
>>> ```
>>> data OneMore : Rel ℕ 0ℓ where
>>>   onemore : {n : ℕ} → OneMore n (suc n)
>>>
>>> data SucList : Set where
>>>   sucList : (xs : List ℕ) (ys : List ℕ) .{p : Pointwise OneMore xs ys} →
>>> SucList
>>>
>>> t5a : SucList
>>> t5a = sucList (42 ∷ 43 ∷ []) (43 ∷ 44 ∷ []) {onemore ∷ (onemore ∷ [])}
>>>
>>> t5b : SucList → Bool
>>> t5b (sucList [] []) = true
>>> t5b (sucList (zero ∷ xs) (zero ∷ ys) {p}) = {!!}
>>> t5b (sucList (zero ∷ xs) (suc y ∷ ys) {p}) = {!!}
>>> t5b (sucList (suc x ∷ xs) (zero ∷ ys) {p}) = {!!}
>>> t5b (sucList (suc x ∷ xs) (suc y ∷ ys) {p}) = {!!}
>>> ```
>>>
>>> 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.
>>>
>>> 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.
>>>
>>> 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.
>>>
>>> Or did I misunderstand these concepts and opt for other means to get
>>> things erased at run time?
>>> Or are there workarounds or additional things to learn/add to make these
>>> cases work the way I would like them to work?
>>>
>>>
>>> Kind regards,
>>> Mathijs
>>>
>>> PS: I couldn't resist the subject-line although this might get
>>> advertisers to label me as entering an early midlife crisis :)
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200122/9650e821/attachment.html>