Heterogeneous Lists

We define HList as a synonym for List (Σ α : Type u, α), namely a list of types together with a value.

We note some other implementations of HList:

• Soup
• Part of Certified Programming with Dependent Types (it's in Coq, but can be translated to Lean)

Our choice of definition is so that we can directly rely on the existing API for List.

@[reducible, inline]

abbrev HList : Type (u + 1)

Heterogeneous list

Equations

• HList = List ((α : Type ?u.4) × α)

def HList.nil : HList

Equations

• HList.nil = []

def HList.cons (x : (α : Type u) × α) (xs : HList) : HList

Equations

• x ::ₕ xs = x :: xs

def HList.hlist : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def HList.«term_::ₕ_» : Lean.TrailingParserDescr

Equations

• HList.«term_::ₕ_» = Lean.ParserDescr.trailingNode `HList.«term_::ₕ_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ₕ ") (Lean.ParserDescr.cat `term 67))

@[simp]

theorem HList.cons_eq_List.cons {x : (α : Type u) × α} {xs : HList} : x ::ₕ xs = x :: xs

@[simp]

theorem HList.length_nil : List.length nil = 0

@[simp]

theorem HList.length_cons (x : (α : Type u) × α) (xs : HList) : List.length (x ::ₕ xs) = List.length xs + 1

def HList.getTypes : HList → List (Type u)

Returns the types of the elements in the HList

Equations

• HList.getTypes = List.map fun (x : (α : Type ?u.9) × α) => x.fst

@[simp]

theorem HList.getTypes_nil : getTypes [] = []

@[simp]

theorem HList.getTypes_cons (x : (α : Type u) × α) (xs : HList) : getTypes (x :: xs) = x.fst :: xs.getTypes

@[simp]

theorem HList.getTypes_hcons (x : (α : Type u) × α) (xs : HList) : (x ::ₕ xs).getTypes = x.fst :: xs.getTypes

@[simp]

theorem HList.length_getTypes (l : HList) : l.getTypes.length = List.length l

@[simp]

theorem HList.getTypes_eq_get_fst (l : HList) (i : Fin (List.length l)) : l.getTypes[i] = l[i].fst

def HList.getValue (l : HList) (i : Fin (List.length l)) : l[i].fst

Get the value of the element at index i, of type l[i].1

Equations

• l.getValue i = l[i].snd

@[simp]

theorem List.get_nil {α : Type u} (i : Fin 0) (a : α) : [].get i = a

def DVec {m : Type v} (α : m → Type u) : Type (max u v)

Dependent vectors

Equations

• DVec α = ((i : m) → α i)

def HList.toDVec (l : HList) : DVec fun (i : Fin (List.length l)) => l[i].fst

Convert a HList to a DVec

Equations

• l.toDVec i = l[i].snd

def HList.ofDVec {n : ℕ} {α : Fin n → Type u} (l : DVec α) : HList

Create an HList from a DVec

Equations

• HList.ofDVec l = List.map (fun (i : Fin n) => ⟨α i, l i⟩) (List.finRange n)

theorem HList.toDVec_eq_getValue (l : HList) (i : Fin (List.length l)) : l.toDVec i = l.getValue i

Equivalent between HList.getValue and HList.toDVec