The Coq mailing list

[flicky frans <flickyfrans AT gmail.com>]

I don't know Coq much, so my answer will be in Agda.

Vilhelm Sjöberg, this ``tt'' at the end looks confusing. Agda has
non-empty vectors (the _^_ operator), which are handy in this case:

    HList : ∀ {α} n -> Set α ^ n -> Set α
    HList  0             _       = Lift ⊤
    HList  1             X       = X
    HList (suc (suc n)) (X , Xs) = X × HList (ℕ.suc n) Xs

    lookup-^ : ∀ {n α} {A : Set α} -> (i : Fin n) -> A ^ n -> A
    lookup-^ {1}            zero    x       = x
    lookup-^ {suc (suc n)}  zero   (x , xs) = x
    lookup-^ {1}           (suc ())
    lookup-^ {suc (suc n)} (suc i) (x , xs) = lookup-^ i xs

    get : ∀ n {Xs : Set ^ n} -> (i : Fin n) -> HList n Xs -> lookup-^ i Xs
    get  1             zero    x       = x
    get (suc (suc n))  zero   (x , xs) = x
    get  1            (suc ())
    get (suc (suc n)) (suc i) (x , xs) = get _ i xs

    test : get 4 (Fin.suc (Fin.suc Fin.zero)) (1 , tt , 42 , true) ≡ 42
    test = refl

Agda can infer all types automatically. To get rid of this
``Fin.suc``s we can define a generic combinator

    Default : ∀ {n} -> Set -> (Fin n -> Set) -> ℕ -> Set
    Default {0}     A F  m      = A
    Default {suc n} A F  0      = F Fin.zero
    Default {suc n} A F (suc m) = Default A (F ∘ Fin.suc) m

    default : ∀ {n} {A : Set} {C : Fin n -> Set}
            -> A -> ((i : Fin n) -> C i) -> ∀ m -> Default A C m
    default {0}     x f  m      = x
    default {suc n} x f  0      = f Fin.zero
    default {suc n} x f (suc m) = default x (f ∘ Fin.suc) m

and use it:

    _≢0 : ℕ -> Set
    0 ≢0 = ⊥
    _ ≢0 = ⊤

    getᴺ : ∀ n {Xs : Set ^ n}
         -> ∀ m {_ : m ≢0} -> HList n Xs -> Default {n} ⊤ (λ i ->
lookup-^ i Xs) (m ∸ 1)
    getᴺ n m hs = default tt (λ i -> get n i hs) (m ∸ 1)

``getᴺ'' receives the length of a tuple and the index of an element.
If the index is bigger than the length, then ``getᴺ'' returns ``tt''.

    test-2 : getᴺ 4 3 (1 , true , 42 , tt) ≡ 42
    test-2 = refl

    test-3 : getᴺ 4 5 (1 , true , 42 , 42) ≡ tt
    test-3 = refl

It's also possible to write fully universe polymorphic ``HList'', so
you can write stuff like (1 , List Set , Set₁ , 42), but that's more
involved.

It's also possible to replace n-ary tuples with a datatype, that
represents heterogeneous vectors, so you can write something like

    test : vgetᴺ 3 (1 ∷ true ∷ 42 ∷ tt ∷ []) ≡ 42
    test = refl

but datatypes have more problems with universe polymorphism than functions.

The whole code: http://lpaste.net/118537