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?

`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`

).

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?

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

Thanks! Had trouble getting that right.

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`

?

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)

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?

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: May 24 2024 at 23:01 UTC