[Agda] Struggling with irrelevance

[Mathijs Kwik]

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 :)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200121/afe22831/attachment.html>