[Agda] Heterogeneous Vectors

[Thorsten Altenkirch]

Hi Simon,

indeed, Agda's implementation of universe polymorphism is too picky in  
this instance. The only work around seems to be exactly the one you  
suggest. Actually, due to the lack of extensionality it may be better  
to use

HVec : ∀ {n} → Vec Set n → Set
HVec [] = ⊤
HVec (A ∷ As) = A × HVec As

which is extensionally isomorphic to your solution but avoids using  
functions.

Cheers,
Thorsten

On 28 May 2010, at 17:32, Simon Foster wrote:

> Hi,
>
> I'm trying to come up with a flexible implementation of a  
> heterogeneous vector, but I'm encountering some problems with  
> universe levels. At the moment I am using the following  
> representation:
>
> data HVec {a} : (n : ℕ) → (As : Vec (Set a) n) → Set (suc a)  
> where
>  hnil  : HVec zero []
>  hcons : ∀ {A : Set a} {k} {As} → A → HVec k As → HVec (suc  
> k) (A ∷ As)
>
> This works quite well, except when I want to use it in an inductive  
> datatype (such as a typed n-ary expressions), because this leads to  
> a data-type whose universe index increases depending on the data- 
> type depth. My question is, is there another way of representing  
> heterogeneous vectors which doesn't require the type to have a  
> higher set index than its encapsulated types? I can achieve a  
> similar effect using functions, e.g.
>
> HVec : ∀ {a} → (n : ℕ) → (As : Vec (Set a) n) → Set a
> HVec n As = λ (i : Fin n) → lookup i As
>
> But such a representation is very cumbersome to use. Is there a  
> better way using an inductive datatype?
>
> Thanks,
>
> -Si._______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda