# [Agda] Irrelevance and resurrection in type signatures

Andreas Abel abela at chalmers.se
Sat Jul 29 02:32:59 CEST 2017

```Hi Matus,

ICC* is based on untyped equality rather than Agda's typed equality of
Martin-Löf Type Theory.  In particular, ICC* does not have eta-equality
for record types like Agda, which is type-directed.

In the particular case, Vec A n is not a large elimination of n, thus,

Agda has the undocumented and slightly buggy ..-modality to mark indices
in types which are not large eliminations.  This makes your example go
through:

{-# OPTIONS --experimental-irrelevance #-}

open import Data.Nat

data Vec (A : Set) : ..(n : ℕ) → Set where
Nil : Vec A zero
Cons : (n : ℕ) → (x : A) → (xs : Vec A n) → Vec A (suc n)

vlen : ∀ {A} → .(n : ℕ) → Vec A n → ℕ
vlen .(zero)   Nil = zero
vlen .(suc n) (Cons n x xs) = suc (vlen n xs)

Alternatively, .. can be used as "run-time irrelevance":

open import Data.Nat

data Vec (A : Set) : (n : ℕ) → Set where
Nil : Vec A zero
Cons : (n : ℕ) → (x : A) → (xs : Vec A n) → Vec A (suc n)

vlen : ∀ {A} → ..(n : ℕ) → Vec A n → ℕ
vlen .(zero)   Nil = zero
vlen .(suc n) (Cons n x xs) = suc (vlen n xs)

Both lead to the erasure of parameter n in vlen at runtime.

Cheers,
Andreas

On 28.07.2017 23:24, Matus Tejiscak wrote:
> Dear all,
>
> I have the following program.
>
>> open import Data.Nat
>>
>> data Vec (A : Set) : ℕ → Set where
>>    Nil : Vec A zero
>>    Cons : (n : ℕ) → (x : A) → (xs : Vec A n) → Vec A (suc n)
>>
>> vlen : ∀ {A} → .(n : ℕ) → Vec A n → ℕ
>> vlen .(zero)   Nil = zero
>> vlen .(suc n) (Cons n x xs) = suc (vlen n xs)
>
> Agda complains in the type signature of `vlen` that `n` is declared irrelevant
> so it cannot be used in the expression `Vec A n`.
>
> PDF page 12 of http://www2.tcs.ifi.lmu.de/~abel/talkFoSSaCS11.pdf mentions
> that "Could not reconcile this with typed equality and large eliminations."
>
> Could anyone shed some light on what the problem is there (and why does ICC*
> not suffer from it)? Why cannot we resurrect the context in type signatures?
>
> Thanks!
> Matus
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/
```