In programming languages, a list is a collection of values.
The builtin 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 builtin 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 nonhomogenous
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.
hlist
typeHere'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 ith element of the list A
is passed to
B
to get a type corresponding to the ith 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.)
Let's have a look at the arguments needed by the hlist
constructors.
hcons
needs the following arguments:
Argument  Comment 

A : Type 
Type of elements of ls 
B : A > Type 
Mapping from A to Type 
x : A 
Value to pass to B for new element
val 
ls : list A 
Values to be passed to B for xs 
val : B x 
New hlist element. Its type is B x 
xs : hlist 
Remaining elements 
(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. *)
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).
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 *)
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
*)
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 *)
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
*)
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])
*)
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 'nonsimple' 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])
*)
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:
Argument  Comment 

A : Type 
Obtainable from B 
B : A > Type 
Irrelevant as list is empty 
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:
Argument  Comment 

A : Type 
Available from B 
B : A > Type 
Available from hlist type 
x : A 
Available from val 
ls : list A 
Inferable from xs and B 
val : B x 
Element being added 
xs : hlist 
Remaining elements 
(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 nonimplicit 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:
Argument  Comment 

A : Type 
Available from B 
B : A > Type 

list A 
Inferable via B and elements 
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.
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.
Thanks to GaÃ«tan Gilbert for help in setting the indexing function right. ðŸ™‚
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];;
# [type bool but an expression was expected of type Error: This expression has
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)
*)