Heterogeneous lists in Coq

In programming languages, a list is a collection of values.

The built-in lists of some programming languages (like OCaml and C++) are homogeneous lists. ie, lists where all elements should be of the same type.

Whereas the lists that come out of the box in some other programming languages (like Python) can be heterogeneous, where the elements needn't all be of the same type. (I included a sample usage of lists in a few programming languages under the 'Addendum' section at the end of this blog post.)

In Coq, we have built-in lists in the form of list, which is defined as an inductive type:

Inductive list (A : Type) : Set :=
| nil  : list A
| cons : A -> list A -> list A.

Arguments nil {A}.
Arguments cons {A} a l.

As is clear from the definition, this list allows only elements of the same type. ie, it's a homogeneous list.

Examples of using Coq's list:

Require Import List.
Import ListNotations.

Check [1; 2].
(* [1; 2] : list nat *)

Check [true; false].
(* [true; false] : list bool *)

Coq's type checker won't be happy if we try making a non-homogenous list with list:

Check [1; true].
(*
The term "[true]" has type "list bool" while it is expected to have type
 "list nat".
*)

Check [true; 1].
(*
The term "[1]" has type "list nat" while it is expected to have type
 "list bool".
*)

In the list type, the type of the elements of the list is declared as an implicit argument. So Coq looks at the first element of the list and expects every other element to be of the same type.

A way to have heterogeneous lists (hlists) in Coq is described in the book Certified Programming with Dependent Types.

I had found it a bit difficult to understand at first, so I describe the way that helped me understand it in this blog post.

An hlist type

Here's an inductive type representing hlist values:

Inductive hlist (A : Type) (B : A -> Type) : list A -> Type :=
| hnil : hlist A B []
| hcons : forall (x : A) (ls : list A),
    (B x) -> hlist A B ls -> hlist A B (x::ls).

In this definition, the hlist type has a list associated with it (the list A).

We also have B, which is a function that maps the actual type of the elements of the hlist to a common type. It does a 'translation' to make Coq sort of feel that all elements are of the same type so that the type checker will stay happy.

The elements of the list A are passed as arguments to the B function to get the type of the corresponding hlist element. ie, the i-th element of the list A is passed to B to get a type corresponding to the i-th element of the hlist.

The way the hlist will turn out depends on our choice of B. I took (fun x:Set => Type) as the value of B (since Type is the type of all types).

This is just one way of doing this. Coq just needs all elements to appear to be of the same type, one way or the other.

Length of list in hcons's type is same as the number of elements of the hlist to which a new element is being added. Quite like the case of list.

(This often confuses me. I somehow keep thinking that this list is associated with the entire list put together by hcons instead of just its hlist argument to which a new element is being added.)

Parameters

Let's have a look at the arguments needed by the hlist constructors.

hcons needs the following arguments:

(I gave names val and xs for convenience in the above table.)

The 'translation' performed by the B function sort of makes it looks as if all elements of the hlist are of type Type.

A simple hcons constructor usage looks like:

hcons  Set   (fun x => x)   nat   []%list   3   hnil.
       | |   |          |   | |   |     |   |   |  |
       +-+   +----------+   +-+   +-----+   |   +--+
        |          |         |       |      |     |
        |      B:A->Type     |   ls:list A  |    hlist A B _ _
        |                    |              |
     A:Type                 x:A            B x

(Note: Length of the ls here is one less than the length of the resultant hlist itself.)

Compute hcons.
(*
= fun (A : Type) (B : A -> Type) (x : A) (ls : list A)
         (x0 : B x) (x1 : hlist A B ls) => hcons A B x ls x0 x1
     : forall (A : Type) (B : A -> Type) (x : A) (ls : list A),
       B x -> hlist A B ls -> hlist A B (x :: ls)
*)

Compute hcons Set. (* A (hlist) *)
(*
= fun (B : Set -> Type) (x : Set) (ls : list Set)
         (x0 : B x) (x1 : hlist Set B ls) => hcons Set B x ls x0 x1
     : forall (B : Set -> Type) (x : Set) (ls : list Set),
       B x -> hlist Set B ls -> hlist Set B (x :: ls)
*)

Compute hcons Set (fun x => x).  (* B (hlist) *)
(*
= fun (x : Set) (ls : list Set) (x0 : (fun x0 : Set => x0) x)
         (x1 : hlist Set (fun x1 : Set => x1) ls) =>
       hcons Set (fun x2 : Set => x2) x ls x0 x1
     : forall (x : Set) (ls : list Set),
       (fun x0 : Set => x0) x ->
       hlist Set (fun x0 : Set => x0) ls ->
       hlist Set (fun x0 : Set => x0) (x :: ls)
*)

Compute hcons Set (fun x => x) nat. (* x:A *)
(*
= fun (ls : list Set) (x : (fun x : Set => x) nat)
         (x0 : hlist Set (fun x0 : Set => x0) ls) =>
       hcons Set (fun x1 : Set => x1) nat ls x x0
     : forall ls : list Set,
       (fun x : Set => x) nat ->
       hlist Set (fun x : Set => x) ls ->
       hlist Set (fun x : Set => x) (nat :: ls)
*)

Compute hcons Set (fun x => x) nat []%list. (* ls:list A *)
(*
= fun (x : (fun x : Set => x) nat)
         (x0 : hlist Set (fun x0 : Set => x0) []) =>
       hcons Set (fun x1 : Set => x1) nat [] x x0
     : (fun x : Set => x) nat ->
       hlist Set (fun x : Set => x) [] -> hlist Set (fun x : Set => x) [nat]
*)

Compute hcons Set (fun x => x) nat []%list 3. (* B x *)
(*
= fun x : hlist Set (fun x : Set => x) [] =>
       hcons Set (fun x0 : Set => x0) nat [] 3 x
     : hlist Set (fun x : Set => x) [] -> hlist Set (fun x : Set => x) [nat]
*)

Compute hcons Set (fun x => x) nat []%list 3
  (hnil Set (fun x => x)).
(*
= hcons Set (fun x : Set => x) nat [] 3 (hnil Set (fun x : Set => x))
*)

(Well, the output is quite verbose and hence not so readable. We can make this better with notations. We'll do that later.)

hnil takes just the A and B as arguments.

A sample usage of the hnil constructor:

hnil  Set  (fun x => x)
      | |  |          |
      +-+  +----------+
       |         |     
       |     B:A->Type 
       |               
     A:Type             

As evident from:

Compute hnil.
(*
= fun (A : Type) (B : A -> Type) => hnil A B
     : forall (A : Type) (B : A -> Type), hlist A B []
*)
(* Two more arguments needed: A and B. *)

Compute hnil Set.
(*
= fun B : Set -> Type => hnil Set B
     : forall B : Set -> Type, hlist Set B []
*)
(* One more argument remaining: B *)

Compute hnil Set (fun x => x).
(*
= hnil Set (fun x : Set => x)
     : hlist Set (fun x : Set => x) []
*)
(* Okay, that's it. *)

A few functions

Now, let's define a few function for working with hlist values.

But before that, it's good to have a few example hlists that can be used to try out these functions:

(* [[ 3; true ]] *)
Example hls1 : hlist Set (fun x => x) [nat; bool] :=
  hcons Set (fun x=>x) nat [bool] 3
    (hcons Set (fun x=>x) bool [] true (hnil _ _)).


(* [[ false; 3; true ]] *)
Example hls2 : hlist Set (fun x => x) [bool; nat; bool] :=
  hcons Set (fun x=>x) bool[nat;bool] false
    (hcons Set (fun x=>x) nat [bool] 3
      (hcons Set (fun x=>x) bool [] true (hnil _ _))).

While defining functions for hlist, we must bear in mind that Gallina functions need to be total. ie, all possibilities need to be considered.

To satisfy this criterion while still keeping the type checker happy, the functions whose definitions are given below return unit type when a value cannot be returned (denoting an abnormal/error condition).

Length

Calculating the length of an hlist is quite easy as the hlist type itself carries the information needed to find its length.

Definition hlength {A:Type} {B:A->Type}
    {ls : list A} (hls : hlist A B ls) : nat := length ls.

hlength merely takes ls which is part of the hlist type and returns its length.

Sample usage:

Compute hlength hls1.
(* 2 : nat *)

Head

Function to get the first element of an hlist.

Definition hhead {A: Type} {B: A -> Type}
    {ls: list A} (hls : hlist A B ls)
  : match ls with
    | (t::ts)%list => B t
    | _ => (unit:Type)
    end :=
  match hls with
  | hnil _ _ => tt
  | hcons _ _ typ typs x xs => x
  end.

hhead returns tt : unit if the argument hlist is empty.

Sample usage:

Compute hhead hls1.
(*
= 3
     : match [nat; bool]%list with
       | []%list => unit : Type
       | (t :: _)%list => (fun x : Set => x) t
       end
*)

Tail

Function that gets all elements of an hlist except the first element.

Definition htail {A: Type} {B: A -> Type}
    {ls: list A} (hls : hlist A B ls)
  : match ls with
    | (t::ts)%list => hlist A B ts
    | _ => hlist A B []%list
    end :=
  match hls with
  | hnil _ _ => hnil _ _
  | hcons _ _ typ typs x xs => xs
  end.

Sample usage:

Compute htail hls1.
(*
= hcons Set (fun x : Set => x) bool [] true
         (hnil Set (fun x : Set => x))
     : match [nat; bool]%list with
       | []%list => hlist Set (fun x : Set => x) []
       | (_ :: ts)%list => hlist Set (fun x : Set => x) ts
       end
*)
(* ie, an hlist with 'true' as its only element. *)

Compute htail (htail hls1).
(*
= hnil Set (fun x : Set => x)
     : match [bool]%list with
       | []%list => hlist Set (fun x : Set => x) []
       | (_ :: ts)%list => hlist Set (fun x : Set => x) ts
       end
*)
(* ie, an empty hlist *)

Indexing

Function to return the i-th element of an hlist.

Indexing starts from 0.

Fixpoint hidx_helper {A : Type} (B:A->Type)
    (ls : list A) (idx : nat) : Type :=
  match idx, ls with
  | _, []%list => unit
  | O, (x::xs)%list => B x
  | S n', (x::xs)%list => hidx_helper B xs n'
  end.

Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
  (idx : nat) (hls : @hlist A B ls)
  : hidx_helper B ls idx :=
  match idx, hls in (hlist _ _ ls) return
    (hidx_helper B ls idx) with
  | _, @hnil _ _ => tt
  | O, @hcons _ _ _ _ x xs => x
  | S n', @hcons _ _ _ _ x xs => hidx n' xs
  end.

A helper function is used to calculate the return type. Not sure how good a definition this is, as the return type of hidx will contain the hidx_helper. But it does seem to work. 😊

Sample usage:

Compute hidx 0 hls2.
(*
= false
     : hidx_helper (fun x : Set => x) [bool; nat; bool] 0
*)

Compute hidx 1 hls2.
(*
= 3
     : hidx_helper (fun x : Set => x) [bool; nat; bool] 1
*)

Compute hidx 2 hls2.
(*
= true
     : hidx_helper (fun x : Set => x) [bool; nat; bool] 2
*)

Compute hidx 3 hls2.
(*
= tt
     : hidx_helper (fun x : Set => x) [bool; nat; bool] 3
*)

Appending

Function to append two hlist values.

Fixpoint happ {A:Type} {B:A->Type} {ls1 ls2: list A}
    (hls1 : hlist A B ls1) (hls2: hlist A B ls2) :
    hlist A B (ls1++ls2)%list :=
  match hls1 in (hlist _ _ ls1) return
    hlist A B (ls1++ls2)%list with
  | hnil _ _ => hls2
  | hcons _ _ _ _ y ys =>
      hcons A B _ _ y (happ ys hls2)
  end.

The second hlist is added to the end of the first hlist.

Sample usage:

Compute happ hls1 hls2.
(* [[ 3; true; false; 3; true ]] *)
(*
= hcons Set (fun x : Set => x) nat [bool; bool; nat; bool] 3
         (hcons Set (fun x : Set => x) bool [bool; nat; bool] true
            (hcons Set (fun x : Set => x) bool [nat; bool] false
               (hcons Set (fun x : Set => x) nat [bool] 3
                  (hcons Set (fun x : Set => x) bool [] true
                     (hnil Set (fun x : Set => x))))))
     : hlist Set (fun x : Set => x) ([nat; bool] ++ [bool; nat;
bool])
*)

Notations

The output that we saw so far were often too complex or unreadable. In addition we need to write stuff like that to make hlist values as well.

To have a more readable hlist representation, we can use Coq notations.

We can think of these notations as doing simple textual replacement. We can make short notations for bigger definitions.

All right, let's make a few notations.

Module HListNotations.

(* A new scope for the hlist notations. *)
Delimit Scope hlist_scope with hlist.

Notation "[[ ]]" := (hnil _ _) : hlist_scope.

Notation "[[ x ]]" :=
  (hcons Set (fun y=>y) _ _ x (hnil _ _)) : hlist_scope.

Notation "[[ x , y , .. , z ]]" :=
  (hcons Set (fun a=>a) _ _ x
    (hcons Set (fun a=>a) _ _ y ..
      (hcons Set (fun a=>a) _ _ z
        (hnil _ _)) .. )) : hlist_scope.

Infix "::" := (hcons Set (fun x=>x) _ _)
  (at level 60, right associativity, only parsing) : hlist_scope.

Infix "++" := happ
  (at level 60, right associativity, only parsing) : hlist_scope.

End HListNotations.

Placed all these notations into a module named HListNotations (under a new scope with 'hlist' as key).

This module can then be imported with

Import HListNotations.

Example usage of these notations:

Import HListNotations.


(* Empty hlist *)
Compute [[ ]]%hlist.
(*
= [[ ]]%hlist
     : hlist ?A ?B []
*)


(* Single element hlist *)
Compute [[ 3 ]]%hlist.
(*
= [[3]]%hlist
     : hlist Set (fun y : Set => y) [nat]
*)


(* Multiple element hlists *)
Compute [[ 2, 1 ]]%hlist.
(*
= [[2, 1]]%hlist
     : hlist Set (fun a : Set => a) [nat; nat]
*)
Compute [[ 3, 2, 1 ]]%hlist.
(*
= [[3, 2, 1]]%hlist
     : hlist Set (fun a : Set => a) [nat; nat; nat]
*)


(* Few 'non-simple' hlists *)
Compute [[ (1, "hi"%string), 3]]%hlist.
(*
= [[(1, "hi"%string), 3]]%hlist
     : hlist Set (fun a : Set => a) [(nat * string)%type; nat]
*)
Compute [[ (1, true, false), 3]]%hlist.
(*
= [[(1, true, false), 3]]%hlist
     : hlist Set (fun a : Set => a) [(nat * bool * bool)%type; nat]
*)
Compute [[ (1, (2, (3, 4) ), false), 3]]%hlist.
(*
= [[(1, (2, (3, 4)), false), 3]]%hlist
     : hlist Set (fun a : Set => a)
         [(nat * (nat * (nat * nat)) * bool)%type; nat]
*)


(* Add an element to a hlist *)
Compute (3 :: [[]])%hlist.
(*
= [[3]]%hlist
     : hlist Set (fun x : Set => x) [nat]
*)


Compute hhead ([[ 3 ]]%hlist).
(*
= 3
     : match [nat] with
       | [] => unit : Type
       | (t :: _)%list => (fun y : Set => y) t
       end
*)


(* Append two hlists *)
Compute (hls1 ++ hls2)%hlist.
(*
= [[3, true, false, 3, true]]%hlist
     : hlist Set (fun x : Set => x) ([nat; bool] ++ [bool; nat; bool])
*)
Compute ([[1, (2, true)]] ++ [[5]])%hlist.
(*
= [[1, (2, true), 5]]%hlist
     : hlist Set (fun a : Set => a) ([nat; (nat * bool)%type] ++ [nat])
*)
Compute ([[1, true]]++[["hi"%string]])%hlist.
(*
= [[1, true, "hi"%string]]%hlist
     : hlist Set (fun a : Set => a) ([nat; bool] ++ [string])
*)

Implicit arguments

Though we now got notations, we might still need to use the hlist constructors directly.

To make such explicit usages easier, let us make a few of the constructor parameters implicit.

hnil needs the following arguments:

Making both A and B implicit,

Arguments hnil {A B}.

Now hnil can also be used like:

Check @hnil _ _.
Check hnil.
(*
[[ ]]%hlist
     : hlist ?A ?B []
where
?A : [ |- Type]
?B : [ |- ?A -> Type]
*)

In the case of hcons, the following arguments are needed:

(Here, I used xs as the name of the hlist to which an element is added with hcons and val to refer to the new element being added.)

Making A, B, x and ls implicit,

Arguments hcons {A B x ls}.

hcons may now be used like:

Check hcons 3 hnil : hlist Set (fun x=>x) [nat].
Check hcons 3 hnil : hlist _ (fun x=>x) _.
(*
[[3]]%hlist : hlist Set (fun x : Set => x) [nat]
     : hlist Set (fun x : Set => x) [nat]
*)

instead of

Check @hcons Set (fun x=>x) nat []%list 3 hnil
  : hlist Set (fun x=>x) [nat].

Check @hcons Set (fun x=>x) nat []%list 3 hnil.

Observe that while using hcons with implicit arguments, we had to provide the hlist's type as well, whereas we needn't do that for the non-implicit argument version. This is due to the way in which our notation was defined. If the type of hlist is not provided, Coq has no way of figuring out the values of arguments declared as implicit.

We could also make a few arguments of the hlist type implicit as well.

hlist needs the following arguments:

Let's make A and the list A implicit, while keeping B as it is.

Arguments hlist {A} _ {ls}.

Now we can have:

Check hlist (fun x=>x).
(*
hlist (fun x : Type => x)
     : Type
where
?ls : [ |- list Type]
*)

Check hcons 3 hnil : hlist (fun x=>x).
(*
hcons 3 [[ ]]%hlist : hlist (fun x : Type => x)
     : hlist (fun x : Type => x)
*)

Right, that looks much more concise than what we started off with.

As was the case with notations, this is just one way doing things. There could be other (better) ways.

Summary

All the definitions that we made.

Included the functions as well as the notations makes use of some them.

This version of the functions makes some use of the implicit arguments that we had declared.

Require Import List.
Import ListNotations.


(* hlist type *)
Inductive hlist (A : Type) (B : A -> Type) : list A -> Type :=
| hnil : hlist A B []
| hcons : forall (x : A) (ls : list A),
    (B x) -> hlist A B ls -> hlist A B (x::ls).

Arguments hnil {A B}.
Arguments hcons {A B x ls}.
Arguments hlist {A} _ {ls}.


(* Functions *)
Definition hlength {A:Type} {B:A->Type}
    {ls : list A} (hls : @hlist A B ls) : nat := length ls.

Definition hhead {A: Type} {B: A -> Type}
    {ls: list A} (hls : @hlist A B ls)
  : match ls with
    | (t::ts)%list => B t
    | _ => (unit:Type)
    end :=
  match hls with
  | hnil => tt
  | hcons x xs => x
  end.

Definition htail {A: Type} {B: A -> Type}
    {ls: list A} (hls : @hlist A B ls)
  : match ls with
    | (t::ts)%list => hlist B
    | _ => hlist B
    end :=
  match hls with
  | hnil => hnil
  | hcons x xs => xs
  end.

Fixpoint hidx_helper {A : Type} (B:A->Type)
    (ls : list A) (idx : nat) : Type :=
  match idx, ls with
  | _, []%list => unit
  | O, (x::xs)%list => B x
  | S n', (x::xs)%list => hidx_helper B xs n'
  end.
Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
  (idx : nat) (hls : hlist B)
  : hidx_helper B ls idx :=
  match idx, hls in (@hlist _ _ ls) return
    (hidx_helper B ls idx) with
  | _, hnil => tt
  | O, hcons x xs => x
  | S n', hcons x xs => hidx n' xs
  end.

Fixpoint happ {A:Type} {B:A->Type} {ls1 ls2: list A}
    (hls1 : @hlist A B ls1) (hls2: @hlist A B ls2) :
    @hlist A B (ls1++ls2)%list :=
  match hls1 in (@hlist _ _ ls1) return
    @hlist A B (ls1++ls2)%list with
  | hnil => hls2
  | hcons y ys =>
      hcons y (happ ys hls2)
  end.


(* Notations *)
Module HListNotations.
Delimit Scope hlist_scope with hlist.

Notation "[[ ]]" := (@hnil _ _) : hlist_scope.

Notation "[[ x ]]" :=
  (@hcons Set (fun y=>y) _ _ x (@hnil _ _)) : hlist_scope.

Notation "[[ x , y , .. , z ]]" :=
  (@hcons Set (fun a=>a) _ _ x
    (@hcons Set (fun a=>a) _ _ y ..
      (@hcons Set (fun a=>a) _ _ z
        (@hnil _ _)) .. )) : hlist_scope.

Infix "::" := (@hcons Set (fun x=>x) _ _)
  (at level 60, right associativity, only parsing) : hlist_scope.

Infix "++" := happ
  (at level 60, right associativity, only parsing) : hlist_scope.

End HListNotations.

References

• CPDT: Heterogeneous Lists
• Another hlist implementation in Coq
• https://coq.inria.fr/library/Coq.Init.Datatypes.html#list

Thanks to Gaëtan Gilbert for help in setting the indexing function right. 🙂

Addendum

List in different languages

Lists in OCaml:

# (* integer list *)
# [1;2;3];;
- : int list = [1; 2; 3]

# (* boolean list *)
# [true;false];;
- : bool list = [true; false]

# (* mixed type list gives error *)
# [1;true];;
Error: This expression has type bool but an expression was expected of type

There are ways to have hlists in OCaml similar to Coq, though. See here for a discussion on that.

Lists in C++: One way of having lists in C++ is by using list from its standard library.

An example program using list:

// Make an integer list and display its elements
#include<iostream>
#include<list>

int main()
{
    std::list<int> l = {1, 2, 3};
    for (int elem : l )
    {
        std::cout << elem << " ";
    }
    std::cout << "\n";
    return 0;
}

This would give 1 2 3  as output.

Lists in Python: Python lists can be heterogeneous.

# integer list
>>> [1, 2, 3]
[1, 2, 3]

# list with integers and a bool
>>> [1, True, 2]
[1, True, 2]

# list with integer, float, string and bool
>>> [1, 3.1415926, "hi", True]
[1, 3.1415926, 'hi', True]

hlist with 'narrower' B

We had used (fun x:Set => Type) as the value of B throughout the blog post. It's possible to have narrower types as well.

Check @hcons nat (fun x:nat => nat) 0 []%list 3 hnil.
(*
hcons 3 [[ ]]%hlist
     : hlist (fun _ : nat => nat)
*)

Check @hcons bool (fun x:bool => nat) false []%list 3 hnil.
(*
hcons 3 [[ ]]%hlist
     : hlist (fun _ : bool => nat)
*)