[Agda] Heterogeneous Vectors
Simon Foster
s.foster at dcs.shef.ac.uk
Fri May 28 16:32:50 CEST 2010
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.
More information about the Agda
mailing list