## Stream: Coq users

### Topic: A 'head' function for 'Vector.t'

#### Julin S (Aug 09 2021 at 10:06):

I have been trying make a function that accepts a `Vector.t` and returns its first element.

But couldn't understand how to handle `Vector.cons` while doing pattern matching.

``````Require Import Vector.
Import VectorNotations.
Definition head {A n} (v : Vector.t A n) : nat :=
match v with
| Vector.nil _ => []
| @Vector.cons _ _ _ n => 0
end.
``````
``````Print Vector.cons.
``````

gives

``````Inductive t (A : Type) : nat -> Type :=
nil : t A 0 | cons : A -> forall n : nat, t A n -> t A (S n)
``````

Does `A -> forall n : nat, t A n -> t A (S n)` mean that it takes:

• a type `A` (implicit?)
• a `Vector.t` of size `n`

and gives a `Vector.t` of size `n+1`?

If so, where does the contents of the vector come in?

I mean, how can we access the elements of the vector?

#### Andrej Dudenhefner (Aug 09 2021 at 11:00):

`A -> forall n : nat, t A n -> t A (S n)` means that given an element of type `A` (the head, let's call it `x`), a natural number `n` (the length) and a vector of length `n` (lets call it `v`) over the type `A` you construct a longer vector (here `x,v`).

#### Julin S (Aug 09 2021 at 11:15):

How can we construct a `Vector.t nat 2` element?

Suppose we need to make `[10; 20]` using the constructors of `Vector.t`? How do we do that?

#### Gaëtan Gilbert (Aug 09 2021 at 11:16):

`@cons nat 10 1 (@cons nat 20 0 (@nil nat))`

#### Julin S (Aug 09 2021 at 12:11):

Thanks! Had trouble getting that right.

#### Julin S (Aug 10 2021 at 04:26):

How would we able to make the actual `head` function though?

I tried

``````Definition head {A n} (v : Vector.t A n) :
match v with
| Vector.nil _ => unit
| Vector.cons _ _ _ _ => A
end
:=
match v with
| Vector.nil _ => tt
| Vector.cons _ x n xs => x
end.
``````

But am getting an error saying

``````term "A" has type "Type" while it is expected to have type "Set"
``````

because of the return type.

I did a `match` for the return type to handle cases where `v` is an empty vector. Isn't that needed?

What could we place in the return type instead of `A`?

#### Gaëtan Gilbert (Aug 10 2021 at 09:00):

that's a stupid issue when the first branch of the match returns Set
you need to explicitly use `match v return Type with ...`
(btw matching on `n` for the type should work too)

#### Julin S (Aug 10 2021 at 12:20):

That did the trick!

What does `return Type` do here?

I looked here: https://coq.inria.fr/refman/language/extensions/match.html
but didn't really understood.

It is not like type-casting in programming languages like C, right?

#### Kenji Maillard (Aug 13 2021 at 08:03):

The `return Type` provides explicitely the required type annotation for the result of the `match` construct: in presence of dependent types this return type can depend on the scrutinee (`v` here) and cannot be inferred in general (in the sense that the general type inference problem is undecidable). Coq has some heuristics to try to infer a reasonable return type in most simply typed matches (where the return type does not depend on the scrutinee) but plays badly with the inference of `Set vs Type`.

Last updated: Oct 04 2023 at 21:01 UTC