[Agda] Struggling with irrelevance

[Ulf Norell]

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/210ac5c9/attachment.html>