If you don’t care about ergonomics you can get pretty close.

Usually the way I reason through these things is to reason about how it would be implemented in pure calculus. In this case, we can define `Vector`

inductively, like this (similar to the trick for defining recursive code in Dhall):

```
let Vector
: Natural → Type → Type
= λ(n : Natural)
→ λ(a : Type)
→ ∀(Vector : Natural → Type)
→ ∀(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ ∀(Nil : Vector 0)
→ Vector n
let Cons
: ∀(n : Natural) → ∀(a : Type) → a → Vector n a → Vector (n + 1) a
= λ(n : Natural)
→ λ(a : Type)
→ λ(x : a)
→ λ(v : Vector n a)
→ λ(Vector : Natural → Type)
→ λ(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ λ(Nil : Vector 0)
→ Cons n x (v Vector Cons Nil)
let Nil
: ∀(a : Type) → Vector 0 a
= λ(a : Type)
→ λ(Vector : Natural → Type)
→ λ(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ λ(Nil : Vector 0)
→ Nil
in Cons 1 Text "ABC" (Cons 0 Text "DEF" (Nil Text))
```

In other words, this is a Boehm-Berarducci encoding of a length-indexed linked list.

That actually type-checks and normalizes just fine. But then if you try to implement a type-safe head, you will get stuck when implementing the case for handling `Nil`

(see the `TODO`

in the code):

```
λ(TODO : ∀(a : Type) → a)
→ let Vector
: Natural → Type → Type
= λ(n : Natural)
→ λ(a : Type)
→ ∀(Vector : Natural → Type)
→ ∀(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ ∀(Nil : Vector 0)
→ Vector n
let Cons
: ∀(n : Natural) → ∀(a : Type) → a → Vector n a → Vector (n + 1) a
= λ(n : Natural)
→ λ(a : Type)
→ λ(x : a)
→ λ(v : Vector n a)
→ λ(Vector : Natural → Type)
→ λ(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ λ(Nil : Vector 0)
→ Cons n x (v Vector Cons Nil)
let Nil
: ∀(a : Type) → Vector 0 a
= λ(a : Type)
→ λ(Vector : Natural → Type)
→ λ(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ λ(Nil : Vector 0)
→ Nil
let Vector/head
: ∀(n : Natural) → ∀(a : Type) → Vector (n + 1) a → a
= λ(n : Natural)
→ λ(a : Type)
→ λ(v : Vector (n + 1) a)
→ v
(λ(_ : Natural) → a)
(λ(m : Natural) → λ(x : a) → λ(v : a) → x)
(TODO a)
in Vector/head 1 Text (Cons 1 Text "ABC" (Cons 0 Text "DEF" (Nil Text)))
```

… buuuuuuuut it actually type-checks and normalizes fine and produces the desired result (albeit under the assumption of the `TODO`

which is logically equivalent to assuming a false axiom):

```
$ dhall --file ./Vector.dhall
λ(TODO : ∀(a : Type) → a) → "ABC"
```

The interesting part is how we get rid of the dependence on `TODO`

.

We can get even closer by doing this:

```
λ(TODO : ∀(a : Type) → a)
→ let Vector
: Natural → Type → Type
= λ(n : Natural)
→ λ(a : Type)
→ ∀(Vector : Natural → Type)
→ ∀(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ ∀(Nil : Vector 0)
→ Vector n
let Cons
: ∀(n : Natural) → ∀(a : Type) → a → Vector n a → Vector (n + 1) a
= λ(n : Natural)
→ λ(a : Type)
→ λ(x : a)
→ λ(v : Vector n a)
→ λ(Vector : Natural → Type)
→ λ(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ λ(Nil : Vector 0)
→ Cons n x (v Vector Cons Nil)
let Nil
: ∀(a : Type) → Vector 0 a
= λ(a : Type)
→ λ(Vector : Natural → Type)
→ λ(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ λ(Nil : Vector 0)
→ Nil
let Vector/head
: ∀(n : Natural) → ∀(a : Type) → Vector (n + 1) a → a
= λ(n : Natural)
→ λ(a : Type)
→ λ(v : Vector (n + 1) a)
→ v
-- The following line is the interesting part!
(λ(m : Natural) → if Natural/isZero m then {} else a)
(λ(m : Natural) → λ(x : a) → λ(v : a) → x)
{=}
in Vector/head 1 Text (Cons 1 Text "ABC" (Cons 0 Text "DEF" (Nil Text)))
```

Here we say that the case for non-empty lists needs to return an `a`

, but the case for empty lists can return anything at all (so we pick `{}`

, which is trivial to return). Here the expected type our fold on `Vector`

s depends on the list index, so we can have the two branches of the fold return different types.

This *almost* works, except that `if`

is restricted to terms so you can’t yet have `if`

expressions on types. We could lift that restriction, but it’s unclear to me if that is sound or not:

```
$ dhall --file ./Vector2.dhall
Use "dhall --explain" for detailed errors
TODO : ∀(a : Type) → a
n : Natural
a : Type
v : ∀(Vector : Natural → Type)
→ ∀(Cons : ∀(m : Natural) → a → Vector m → Vector (m + 1))
→ ∀(Nil : Vector 0)
→ Vector (n + 1)
m : Natural
Error: ❰if❱ branch is not a term
36│ if Natural/isZero m then {} else a
(stdin):36:31
```