[Agda] Struggling with irrelevance

[Mathijs Kwik]

I learned a lot by playing around with the pointers you gave me. I think I
hit a bug (reported https://github.com/agda/agda/issues/4398 ) which is
always fun.

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:

```
data Some (f : k → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  some : {@0 t : k} → f t → Some f

data HList3 (f : k → Set ℓ₂) : List k → Set (ℓ₁ ⊔ ℓ₂) where
  []  : HList3 f []
  _∷_ : (sf : Some f) → ∀ {t} {@0 ft : f t} {{p : sf ≡ some ft}} {xs} →
HList3 f xs → HList3 f (t ∷ xs)

t3a : HList3 id (ℕ ∷ Bool ∷ [])
t3a = some 43 ∷ some false ∷ []

t3b : HList3 id (ℕ ∷ Bool ∷ []) → ℕ
t3b (_∷_ (some x) {{p = refl}} hl3) = x
```
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).

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

What an I missing here?

Kind regards,
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/20200125/5348cfde/attachment.html>