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