[Agda] Irrelevance and resurrection in type signatures

[Andreas Abel]

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, 
your example is probably ok.

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/