Implementing Vector in dhall (or, should we add dependent sums?)


#1

I thought I’d have a go at the new dependent type features and do the first thing everyone does in a dependently-typed language, implement fixed-length vectors.

I wanted to implement Vector n a as a record containing a List a and evidence that the given list has length n. Something like:

{ content  = [ 1, 2 ]
, evidence = assert : List/length Natural [ 1, 2 ] ≡ 2
}

However, this encoding is tricky because the same value appears at the term and type levels. The type of this expression is:

{ content : List Natural
, evidence : 2 ≡ 2
}

but I want something more like

∀(l : List Natural) →
  { content : List Natural
  , evidence : List/length Natural l ≡ 2
  }

Essentially, I think I’m reaching for a dependent sum type but dhall doesn’t have one.

So… two questions. First, am I correct? Is there no way to implement Vector from List with Dhall’s current feature set?

Second, would people consider adding dependent sums to the language?


#2

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

#3

Sorry, I forgot to tie this back to your original question about the more ergonomic encoding you proposed.

So, to do this for the more ergonomic encoding it’s basically the exact same problem. You would need to essentially support type-level operations on Naturals, such as a type-level Natural/fold (in general) along with other useful things like type-level if.

Supporting type-level equivalents of term-level operations usually entails adding something like universe polymorphism to the language, because that means you can have a single function (i.e. Natural/fold) that works at the term level, the type level, the kind level, etc. So universe polymorphism is the real feature you are looking for to power this sort of dependently typed programming.